Pinned Repositories
coq-effects
A program translation implementing self-algebraic effects in Coq.
coq-forcing
A plugin for Coq that implements the call-by-name forcing translation
cubical_forcing
forcing on the cube category to realize univalence
DICoq
Dependent Interoperability for Coq
exceptional-tt
A Coq plugin that implements exceptions in Coq
logrel-coq
Logical Relation for MLTT in Coq
logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda
parametricity-a-la-carte
mixing CoqEAL and univalent parametricity
Program-translations-CC-omega
univalent_parametricity
Univalent Parametricity for Effective Transport
The CoqHott project's Repositories
CoqHott/logrel-coq
Logical Relation for MLTT in Coq
CoqHott/exceptional-tt
A Coq plugin that implements exceptions in Coq
CoqHott/Program-translations-CC-omega
CoqHott/coq-forcing
A plugin for Coq that implements the call-by-name forcing translation
CoqHott/DICoq
Dependent Interoperability for Coq
CoqHott/univalent_parametricity
Univalent Parametricity for Effective Transport
CoqHott/coq-effects
A program translation implementing self-algebraic effects in Coq.
CoqHott/logrel-mltt
A Logical Relation for Martin-Löf Type Theory in Agda
CoqHott/parametricity-a-la-carte
mixing CoqEAL and univalent parametricity
CoqHott/cubical_forcing
forcing on the cube category to realize univalence
CoqHott/model-structures-Coq
Formalization of a model structure on the universe of Types in Coq
CoqHott/sProp
repository containing the examples of the POPL paper
CoqHott/coq-2ltt
Two-level type theory in Coq
CoqHott/ceps
Coq Enhancement Proposals
CoqHott/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.
CoqHott/coq-partialfun
Dependent composable partial functions for free in Coq
CoqHott/coqdocjs
Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]
CoqHott/inductive-families-extraction
CoqHott/logrel-coq-cpp24
CoqHott/reedy
A formalisation of some results on theory of Reedy fibrant diagrams in two-level type theory
CoqHott/seminar-setoid
Toy implementation of TT^obs for the Gallinette Seminar
CoqHott/template-coq-forcing
A call-by-name forcing translation implemented in Meta Coq