tabareau

InriaFrance

Pinned Repositories

AJoCaml
Implementation of the aspect join calculus based on JoCaml
Language:OCaml1 2 00
Cocasse
A library for Gradual Certified Programming in Coq
Language:Coq9 4 12
Coq-Equations
A plugin for Coq to add dependent pattern-matching.
Language:OCaml0 2 00
coq-forcing
Tentative implementation of call-by-name forcing in Coq
Language:OCaml0 2 00
coq-malfunction
Language:Coq0 0 00
Forcing
Forcing layer on top of Coq
Language:Coq1 2 00
HoTT
Homotopy type theory
Language:Coq0 2 00
lmfi_hott
Course on HoTT at LMFI Master
Language:Coq1 4 00
omega_categories
Formalisation of strict omega categories and the homotopy hypothesis in type theory, using coinduction
Language:Coq0 2 01
sheafification
Language:TeX00

tabareau's Repositories

tabareau/Cocasse
A library for Gradual Certified Programming in Coq
Language:Coq9 4 12
tabareau/AJoCaml
Implementation of the aspect join calculus based on JoCaml
Language:OCaml1 2 00
tabareau/Forcing
Forcing layer on top of Coq
Language:Coq1 2 00
tabareau/lmfi_hott
Course on HoTT at LMFI Master
Language:Coq1 4 00
tabareau/Coq-Equations
A plugin for Coq to add dependent pattern-matching.
Language:OCaml0 2 00
tabareau/coq-forcing
Tentative implementation of call-by-name forcing in Coq
Language:OCaml0 2 00
tabareau/coq-malfunction
Language:Coq0 0 00
tabareau/HoTT
Homotopy type theory
Language:Coq0 2 00
tabareau/omega_categories
Formalisation of strict omega categories and the homotopy hypothesis in type theory, using coinduction
Language:Coq0 2 01
tabareau/sheafification
Language:TeX00