Popular repositories Loading

1. PhD-thesis PhD-thesis Public

   My PhD thesis.

   TeX 13

2. observational-coq observational-coq Public

   Forked from Yann-Leray/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 develo…

   OCaml 2

3. cwf-strictification cwf-strictification Public

   Accompanying formalisation for the paper "Type theory in type theory using a strictified syntax"

   HTML 2

4. cubical cubical Public

   Forked from agda/cubical

   Agda

5. logrel-mltt logrel-mltt Public

   Forked from CoqHott/logrel-mltt

   A Logical Relation for Martin-Löf Type Theory using Indexed Inductive Types

   Agda

6. Juna Juna Public

   A compiler that supports wobbly types, does CPS and defunctionalization (school project)

   OCaml