Abstract

During my summer stay in Poland I spent the time studying the Coq system, the French proof assistant, widely popular in Europe. Coq is based on Curry-Howard isomorphism as well as Nuprl. There are significant differences from Nuprl's type theory, however.

I am going to present the main features of the type system of Coq, compare it to Nuprl, discuss similarities and differences. I am also going to compare two systems from user-based point of view.