8
$\begingroup$

The history of dependent data types spans decades and is a bit confusing. I have seen some implausible claims about which documents present what. I would like to get it right for my own work without making misleading citations.

Currently,

Now going back to the 90s

  • the earliest citation I could find (from 1994) to CIC points to the 1991 "The Coq proof assistant version 5.6, user's guide"

  • Calculus of Constructions with Inductive Definitions (CCID) looks like a restricted version of CIC presented in "Inductive definitions in the system Coq rules and properties" from 1992-3

There are several other papers from around this time that try to work out dependent data types, but as best as I can tell they do not describe CIC.

Ideally I would like to know

  1. What should be cited as the first formalization of "the Calculus of inductive Constructions"?
  2. What was the first peer reviewed presentation of CiC?
  3. When where claims about its meta theory conjectured/proven, specifically subject reduction/type soundness/normalization?
Improve this question
$\endgroup$
2
  • $\begingroup$ Bruno Baras' thesis may be involved $\endgroup$
    – user833970
    Commented Apr 14, 2022 at 23:23
  • $\begingroup$ "This led to the Calculus of Inductive Constructions, logical formalism implemented in Versions 5 upward of the system, and documented in: C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and Properties [PM93b]."from coq.inria.fr/distrib/current/refman/… seems to indicate "inductive definitions in the system Coq rules and properties" should be cited $\endgroup$
    – user833970
    Commented Apr 22, 2022 at 17:03

1 Answer 1

Reset to default
2
$\begingroup$

It depends on what you're willing to accept, right? It could be:

  • Th. Coquand and C. Paulin-Mohring, "Inductively defined types". In P. Martin-Lof and G. Mints, editors, Proceedings of Colog’88, volume 417. Springer-Verlag, 1990.
  • Z. Luo, "An extended calculus of constructions". PhD Thesis, U. of Edinburgh, 1990 (eprint).
  • Frank Pfenning and Christine Paulin-Mohring, "Inductively Defined Types in the Calculus of Constructions". Tech. Report, CMU-CS-89-209, dated December 8, 1989.

It sounds like Luo's thesis is what you want.

Improve this answer
$\endgroup$
3
  • $\begingroup$ I am aware of these alternative ways to deal with dependent inductive data, but my impression was that they are distinct form CIC in some important ways. I did not cite them in the question for that reason. I'll review and see if I missed something. $\endgroup$
    – user833970
    Commented Apr 12, 2022 at 15:08
  • $\begingroup$ Re: "Inductively defined types" The paper define an “open system” with a scheme for encoding data. “a proposition for an extension of the Calculus of Constructions with inductive definitions as first-class objects. The rules for these definitions follow the point of view of Martin-Lof 's type theory. From a specification of the introduction rules for a new inductive definition, we generate a dependent elimination with new computational rules... Our extension of the Calculus of Constructions with Inductive Definitions... preserve the property for the system to be closed.” from the CCID paper $\endgroup$
    – user833970
    Commented Apr 12, 2022 at 16:02
  • $\begingroup$ Re "Inductively defined types" There are some notable CIC like conventions such as "arities", but the grammar and typing rules are not explicit and while the set theoretic model may imply normalization I don't think anything is said for S.R. or type soundness. Unrelatedly, I have never been able to find a non-“preliminary version” of this paper. It has also been hard for me to nail down in time. You have the usual citation of '88, my pdf cites work from 1989, and the proceedings were apparently published in 1990. $\endgroup$
    – user833970
    Commented Apr 12, 2022 at 16:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.