T
TheoWinterhalter
Researcher, proof assistants and dependent types
22 repositories
98 followers
Saclay
Repositories
Select a repository to view its commits, contributors, and more.public
formal-type-theory
Formalising Type Theory in a modular way for translations between type theories
Coq
90
4
0
Updated 2 years ago
public
phd-thesis
Phd Thesis of Théo Winterhalter. Look at releases to get the latest PDF.
TeX
33
3
0
Updated 2 months ago
public
sirtt
Shape-Irrelevant Reflection Type Theory
Coq
6
0
0
Updated a year ago
public
ett-to-itt
Coq formalisation and plugin of a translation from ETT to ITT
Coq
6
0
0
Updated a month ago
public
ett-to-wtt
Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory
Coq
6
0
0
Updated 8 months ago
public
coq-partialfun
Dependent composable partial functions for free in Coq
Coq
6
2
0
Updated 2 months ago
public
ghost-reflection
A formalisation of a dependent type theory with ghost types
Coq
2
1
1
Updated 5 months ago
public
resizing-reflection
Master Thesis with Nicolas Tabareau on Resizing Rules and Reflection
Coq
1
0
0
Updated 7 years ago
public
selection-count
Add character count for atom editor
CoffeeScript
0
0
1
Updated 11 years ago
public
galliblog
Implementing the Gallinette website and its blog
OCaml
0
0
0
Updated 5 years ago
public
pdm4all
Partial Dijkstra monads for all
Coq
0
0
0
Updated 5 months ago
public
ocawb
Write HTML with ocaml (just fun with continuations)
OCaml
0
0
1
Updated 8 years ago