KnowledgeBase » 
SEMINAR
» ID = 602
Coq and Nuprl
by Wojciech Moczydlowski
2004 Summ
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.