Join 10350+ others. No spamming.
I promise!

Follow us at github.



wilbowma/cic-redex

14

wilbowma / cic-redex

Racket

A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.


READ ME

CIC

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:
    • Use (@ e e) instead of juxtaposition for application syntax.
    • Missing global assumptions and definitions.
  • βιδζη conversion
  • Subtyping
  • Infinite hierarchy of Type
  • Predicative Set
  • Impredicative Prop
  • Parameterized indexed inductive families; Caveats:
  • Strict positivity checking
  • Dependent pattern matching
  • Allowed elimination sorts, including "Prop-extended" (elimination to any sort from empty and singleton Prop)
  • Recursive functions; Caveats:
    • 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