Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
The Principia Rewrite
🧊 An indexed construction of semi-simplicial and semi-cubical sets
A LaTeX package to make theorem names link to coqdoc webpages. Works with ntheorem, amsthm and the LLNCS and LIPIcs classes.
Logical relation for predicative CC omega with booleans and an intensional identity type
Papers We Love. Mad. Talk on fold: slides, Coq file, and links for further reading
A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
Principia Fractalis: Fractal Resonance Ontology. A 1000+ page work exploring how mathematics, consciousness, and physical reality connect through a unified structure. Formally triple-verified in Lean 4, Coq, and L4L
my PhD dissertation: Foreign Function Verification Through Metaprogramming
(Terminating) hylomorphisms in Coq
repo for all notes, programmes etc I made for LambdaConf17
LaTeX sources for my undergraduate thesis
Report for "A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
4th Year Honours Thesis on Programming Language Semantics
Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
Un ejemplo de uso de Coq y Agda para lemas triviales sobre árboles binarios.
Calvin Talks Types
∇⎕ coloring
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989