§ Lean internals Cheat Sheet

• 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.