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.
the specification for CiC is maintained at in the Coq reference manual https://coq.github.io/doc/v8.9/refman/language/cic.html, the credits page has a summery of the history https://coq.github.io/doc/v8.9/refman/credits.html
The meta Coq project has formalized CiC, and formally proven some of its properties
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
- What should be cited as the first formalization of "the Calculus of inductive Constructions"?
- What was the first peer reviewed presentation of CiC?
- When where claims about its meta theory conjectured/proven, specifically subject reduction/type soundness/normalization?