Collaborated with:
J.Cockx M.Sozeau N.Tabareau
Talks about:
without (1) irrelev (1) definit (1) proof (1)
Person: Gaëtan Gilbert
DBLP: Gilbert:Ga=euml=tan
Contributed to:
Wrote 1 papers:
- POPL-2019-GilbertCST
- Definitional proof-irrelevance without K (GG, JC, MS, NT), p. 28.