- CIC page in Coq
-
bollu/cubicaltt: an annotated version of the cubicaltt sources. - CPDT (certified programming with dependent types) chapter on equality to learn about the various reduction rules.
- Data structures to verify acyclicity of a graph on updates : A New Approach to Incremental Cycle Detection and Related Problems
- Coq Coq correct : Paper on formally verifying the type checker for Coq, contains information about data structures used in the kernel.