Pinned Repositories
automata
Beginning of formal language theory
coq-in-coq
A formalisation of the Calculus of Constructions
graph-basics
a Coq toolkit for graph theory
group-theory
Elements of Group Theory
lin-alg
Linear Algebra
ltl
Linear Temporal Logic
paradoxes
Paradoxes in Set Theory and Type Theory
pi-calc
Pi-calculus in Coq
pts
A formalisation of Pure Type Systems
zfc
An encoding of Zermelo-Fraenkel Set Theory in Coq
coq-contribs's Repositories
coq-contribs/coq-in-coq
A formalisation of the Calculus of Constructions
coq-contribs/zfc
An encoding of Zermelo-Fraenkel Set Theory in Coq
coq-contribs/ltl
Linear Temporal Logic
coq-contribs/paradoxes
Paradoxes in Set Theory and Type Theory
coq-contribs/pi-calc
Pi-calculus in Coq
coq-contribs/coq-contribs
coq-contribs/lambek
A Coq Toolkit for Lambek Calculus
coq-contribs/ipc
Intuitionistic Propositional Checker
coq-contribs/miniml
Correctness of the compilation of Mini-ML into the Categorical Abstract Machine
coq-contribs/rsa
Correctness of RSA algorithm
coq-contribs/weak-up-to
New Up-to Techniques for Weak Bisimulation
coq-contribs/param-pi
Coding of a typed monadic pi-calculus using parameters for free names
coq-contribs/ptsatr
Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.
coq-contribs/ramsey
Ramsey Theory
coq-contribs/tarski-geometry
Tarski's geometry
coq-contribs/mutual-exclusion
A certification of Peterson's algorithm for managing mutual exclusion
coq-contribs/zchinese
A proof of the Chinese Remainder Lemma
coq-contribs/mini-compiler
Correctness of a tiny compiler for arithmetic expressions
coq-contribs/otway-rees
Otway-Rees cryptographic protocol
coq-contribs/prfx
Proof Reflection in Coq
coq-contribs/reflexive-first-order
Reflexive first-order proof interpreter
coq-contribs/rem
Rem Theorem in Baire space
coq-contribs/schroeder
The Theorem of Schroeder-Bernstein
coq-contribs/search-trees
Binary Search Trees
coq-contribs/shuffle
Gilbreath's card trick
coq-contribs/streams
Specification of Eratosthene Sieve
coq-contribs/subst
The confluence of Hardin-Lévy lambda-sigma-lift-calcul
coq-contribs/traversable-fincontainer
Traversable Functors are Finitary Containers
coq-contribs/zf
An axiomatisation of intuitionistic Zermelo-Fraenkel set theory
coq-contribs/zsearch-trees
Binary Search Trees