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]

Authors

Gaëtan Gilbert

This author has not been identified. Look up 'Gaëtan Gilbert' in Google