The Coq mailing list

[Brian Milnes <briangmilnes AT gmail.com>]

Frederic,

 It's not so much citing, it's finding a clear definition, differences and implications for my understanding. 

 Is there a bit less I can read that will do that?

 Thanks, Brian

On Tue, Mar 21, 2017 at 4:36 AM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Le 03/20/2017 à 04:03 PM, Brian Milnes a écrit :

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.

I don't think that Thierry's PhD includes inductive types. You should rather cite:

@INPROCEEDINGS{coquand88colog,
BOOKTITLE    = {Proceedings of the  International Conference on Computer Logic\em, Lecture Notes in Computer Science 417}, YEAR = 1988,
TITLE    = {\href{http://doi.org/10.1007/3-540-52335-9_47}{Inductively defined types}},
AUTHOR    = {T. Coquand and C. Paulin-Mohring}}

@INPROCEEDINGS{paulin93tlca,
BOOKTITLE    = {Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications\em, Lecture Notes in Computer Science 664}, YEAR = 1993,
TITLE    = {\href{http://doi.org/10.1007/BFb0037116}{Inductive definitions in the system {Coq} - rules and properties}},
AUTHOR    = {C. Paulin-Mohring}}

@PHDTHESIS{altenkirch93phd,
AUTHOR    = {T. Altenkirch},
TITLE    = {Constructions, inductive types and strong normalization},
SCHOOL    = {University of Edinburgh, UK},
YEAR    = {1993}}

@PHDTHESIS{werner94phd,
YEAR    = {1994},
SCHOOL    = {Universit\'e Paris 7, France},
TITLE    = {\href{https://tel.archives-ouvertes.fr/tel-00196524}{Une th\'eorie des constructions inductives}},
AUTHOR    = {B. Werner}}

But none of these works consider an infinite hierarchy of universes...

For this, you can cite:

@PHDTHESIS{luo90phd,
YEAR    = {1990},
SCHOOL    = {University of Edinburgh, UK},
TITLE    = {\href{http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-118/}{An extended calculus of constructions}},
AUTHOR    = {Z. Luo}}

but it only includes pairs and no arbitrary inductive types.

pCiC

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

if so, where is it formalized?

 Thanks, Brian 

  

@INPROCEEDINGS{luo92lfcs,
AUTHOR    = {Z. Luo},
TITLE    = {A Unifying Theory of Dependent Types: the Schematic Approach},
BOOKTITLE    = {Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science\em, Lecture Notes in Computer Science 620}, YEAR = 1992,
YEAR    = {10.1007/BFb0023883}}

@TECHREPORT{luo92tr2,
AUTHOR    = {Z. Luo},
TITLE    = {A Unifying Theory of Dependent Types: the Schematic Approach},
INSTITUTION    = {University of Edinburgh, UK},
YEAR    = {1992},
NUMBER    = {ECS-LFCS-92-202}}

@PHDTHESIS{goguen94phd,
YEAR    = {1994},
SCHOOL    = {Edinburgh University, UK},
TITLE    = {\href{http://www.lfcs.inf.ed.ac.uk/reports/94/ECS-LFCS-94-304/}{A typed operational semantics for type theory}},
AUTHOR    = {H. Goguen}}

But these works do not include the impredicative sort Prop of Coq.