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]

Abstract

Abstract is missing.