coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Brian Milnes <briangmilnes AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] CoC vs Cic vs pCiC
Date: Mon, 20 Mar 2017 11:03:40 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=briangmilnes AT gmail.com; spf=Pass smtp.mailfrom=briangmilnes AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f181.google.com
Ironport-phdr: 9a23:wAxwjhNISruihr4I0Mwl6mtUPXoX/o7sNwtQ0KIMzox0Lfj+rarrMEGX3/hxlliBBdydsKMZzbSJ+P+4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT69bL9oLRi7rwrdu8sKjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktZwgqJVrhyiuhJx3ZLbbZqPO/ZiZK7QZ88WSXZDU8tXSidPApm8b4wKD+cZIOtYtYj9qEEIrRCjAgesBefvyjlWiX/twKY31P8uERvH3AM6GdIOv3HUrNTxNKcUT++117LFzTrGb/xM2Df97JLEfQwmofGJRL99d9fax0o3Fw7dkFmctYjoMymW2+kNqWSX8vRsWOG1h2I6qAx9vz6izdo2hIbTnIIa0FXE+D15wIkrId24T1Z2Ydu+H5tRsyGWLoV3Qtk+T21xtiY2174LtYOhcCgFz5QnwBHfa/iZfISS/h3jU+ORLS95hHJjZr2/mw6//Va8xuD4TMW501ZHojBYntXStX0BzQHf58uaRvdl+0euwzeP1wTd6uFeJkA0kLLWJIU7wr4xjJUTt0vDHir3mEXyiq+ZaF4k9/On6+TieLrmp5ucO5VohQH5N6Qigta/DvggMggSQ2ib/vyx26Hk/U3gWblFkvk2krTCv53BPsQapqu5AxdP3Yo56ha/CS2m0NUCknUdIlJFYkHPs4+8MFbXZfv8EP2XglK2kT4tyeqVBLD5BoTxKS3Jirboe7l46kpaxREbwtVW5pYSAbYEc9zpXUqknsbZBxlxFg2wxev8QIF3zIIXX22KA6ufPbj6vlqB5+ZpKO6JMtxG8A3hIuQosqa9xUQynkUQKPGk

Folks,

I'm wondering what the right papers are that define the Calculus of Constructions, the Calculus of Inductive Constructions and the newest

predicative Calculus of Constructrions.

CoC

Coquand, Thierry, and Gérard Huet. "The calculus of constructions." Information and computation 76.2-3 (1988): 95-120.

CiC

Is it Coquands thesis? 'Une theories des constuctions', 1985.

pCiC

Is Coq >= 8 based upon a change called the predicative CiC? And

if so, where is it formalized?

Thanks, Brian

[Coq-Club] CoC vs Cic vs pCiC, Brian Milnes, 03/20/2017
- Re: [Coq-Club] CoC vs Cic vs pCiC, Frédéric Blanqui, 03/21/2017
  - Re: [Coq-Club] CoC vs Cic vs pCiC, Brian Milnes, 03/21/2017