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 types
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
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.
Papers We Love. Mad. Talk on fold: slides, Coq file, and links for further reading
my PhD dissertation: Foreign Function Verification Through Metaprogramming
repo for all notes, programmes etc I made for LambdaConf17
Report for "A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
LaTeX sources for my undergraduate thesis
Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
(Terminating) hylomorphisms in Coq
Un ejemplo de uso de Coq y Agda para lemas triviales sobre árboles binarios.
4th Year Honours Thesis on Programming Language Semantics
Calvin Talks Types
∇⎕ coloring
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 2 months ago