🧊 An indexed construction of semi-simplicial and semi-cubical sets
-
Updated
Dec 16, 2025 - TeX
#
Coq
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.
Here are 22 public repositories matching this topic...
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
coq mathematics fractal ontology proof-assistant coq-formalization turing-machine theoretical-physics formal-verification complexity-theory millennium-problems consciousness-and-neuroscience lean4 spectral-theory
-
Updated
Dec 2, 2025 - TeX
The Principia Rewrite
latex coq logic latex-packages formal-mathematics coq-ecosystem formal-proofs formal-logic history-of-philosophy
-
Updated
Nov 24, 2025 - TeX
Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
-
Updated
Nov 17, 2025 - TeX
LaTeX sources for my undergraduate thesis
-
Updated
Aug 22, 2025 - TeX
(Terminating) hylomorphisms in Coq
-
Updated
Jul 8, 2025 - TeX
Logical relation for predicative CC omega with booleans and an intensional identity type
-
Updated
Apr 22, 2025 - TeX
my PhD dissertation: Foreign Function Verification Through Metaprogramming
-
Updated
Oct 11, 2024 - TeX
∇⎕ coloring
-
Updated
Jul 2, 2022 - TeX
Report for "A Basis for Event-Driven Programming" based on Linear Temporal Type Theory
-
Updated
May 25, 2021 - TeX
-
Updated
Dec 4, 2020 - TeX
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.
-
Updated
Jul 23, 2020 - TeX
A LaTeX package to make theorem names link to coqdoc webpages. Works with ntheorem, amsthm and the LLNCS and LIPIcs classes.
-
Updated
May 22, 2019 - TeX
Papers We Love. Mad. Talk on fold: slides, Coq file, and links for further reading
-
Updated
May 22, 2018 - TeX
Appunti ed esercizi del corso "Teoria dei tipi" - università degli studi di Padova, corso di laurea in Informatica
math coq proof-assistant type-theory exercises unipd esercizi matematica logica martin-lof teoria-dei-tipi
-
Updated
Mar 19, 2018 - TeX
repo for all notes, programmes etc I made for LambdaConf17
-
Updated
May 30, 2017 - TeX
Calvin Talks Types
-
Updated
Apr 10, 2017 - TeX
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
- Followers
- 64 followers
- Repository
- coq/coq
- Website
- github.com/topics/coq
- Wikipedia
- Wikipedia