A type theory with definitional proof-irrelevance. (Une théorie des types avec insignifiance des preuves définitionnelle)

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},
}