Showing cs.PLShow all
2 papers · 1 filter
cs.PL2021
Touring the MetaCoq Project (Invited Paper)
Matthieu Sozeau
Proof assistants are getting more widespread use in research and industry to provide certified and independently checkable guarantees about theories, designs, systems and implement…
cs.PL2019
The Marriage of Univalence and Parametricity
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, equality is appallingly syntactic and, as…