loic-p

Pinned Repositories

cellular
Cellular cohomology in cubical Agda
Language:TeX00
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.
Language:OCaml00
cubical
Language:Agda00
cubical_forcing
Implementation of cubical forcing in Coq
Language:Coq20
Juna
A compiler that supports wobbly types, does CPS and defunctionalization (school project)
Language:OCaml00
logrel-coq
Logical relation for MLTT in Coq
Language:Coq00
logrel-impred
Language:Coq00
logrel-mltt
A Logical Relation for Martin-Löf Type Theory using Indexed Inductive Types
Language:Agda0 0 00
PhD-thesis
My PhD thesis.
Language:TeX12 2 00
template-coq
Reflection library for Coq
Language:Coq10

loic-p's Repositories

loic-p/PhD-thesis
My PhD thesis.
Language:TeX12 2 00
loic-p/Setoid-Universe
A universe for proof-relevant setoids
Language:Coq7 1 0
loic-p/cubical_forcing
Implementation of cubical forcing in Coq
Language:Coq20
loic-p/template-coq
Reflection library for Coq
Language:Coq10
loic-p/cellular
Cellular cohomology in cubical Agda
Language:TeX00
loic-p/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.
Language:OCaml00
loic-p/cubical
Language:Agda00
loic-p/Juna
A compiler that supports wobbly types, does CPS and defunctionalization (school project)
Language:OCaml00
loic-p/logrel-coq
Logical relation for MLTT in Coq
Language:Coq00
loic-p/logrel-impred
Language:Coq00
loic-p/logrel-mltt
A Logical Relation for Martin-Löf Type Theory using Indexed Inductive Types
Language:Agda0 0 00