Definitional proof-irrelevance without K

Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, Nicolas Tabareau. Definitional proof-irrelevance without K. Proceedings of the ACM on Programming Languages, 3, 2019. [doi]

Authors

Gaëtan Gilbert

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

Jesper Cockx

Identified as Jesper Cockx

Matthieu Sozeau

This author has not been identified. Look up 'Matthieu Sozeau' in Google

Nicolas Tabareau

This author has not been identified. Look up 'Nicolas Tabareau' in Google