Gaëtan Gilbert. A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle). PhD thesis, Mines ParisTech, France, 2019. [doi]
@phdthesis{hal-15988,
title = {A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle)},
author = {Gaëtan Gilbert},
year = {2019},
url = {https://tel.archives-ouvertes.fr/tel-03236271},
researchr = {https://researchr.org/publication/hal-15988},
cites = {0},
citedby = {0},
school = {Mines ParisTech, France},
}