Pinned Loading

1. ghost-reflection ghost-reflection Public

   A formalisation of a dependent type theory with ghost types

   Coq 2 1

2. MetaCoq/metacoq MetaCoq/metacoq Public

   Metaprogramming, verified meta-theory and implementation of Coq in Coq

   Coq 390 82

3. coq-partialfun coq-partialfun Public

   Dependent composable partial functions for free in Coq

   Coq 6 2

4. phd-thesis phd-thesis Public

   Phd Thesis of Théo Winterhalter. Look at releases to get the latest PDF.

   TeX 33 3

5. ett-to-wtt ett-to-wtt Public

   Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory

   Coq 6

6. SSProve/ssprove SSProve/ssprove Public

   A foundational framework for modular cryptographic proofs in Coq

   Coq 56 9