A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.
We currently model the following parts of the CIC spec:
- CC; Caveats:
(@ e e)instead of juxtaposition for application syntax.
- Missing global assumptions and definitions.
- βιδζη conversion
- Infinite hierarchy of Type
- Predicative Set
- Impredicative Prop
- Parameterized indexed inductive families;
- Missing mutually inductive families, since they can be encoded via indexed families; see, e.g., The Rooster and the Syntactic Bracket for the construction.
- Strict positivity checking
- Dependent pattern matching
- Allowed elimination sorts, including "Prop-extended" (elimination to any sort from empty and singleton Prop)
- Recursive functions;
- Missing mutually recursive functions.
- Expects recursive functions to be well-defined on their first argument.
- Termination checking
We do not plan to model:
- Coinductive families