17 citations · 20 across the 5 of their papers we have counts for
7 papers
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau +2
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class…
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…
Types are Internal -Groupoids
Antoine Allioux, Eric Finster, Matthieu Sozeau
By extending type theory with a universe of definitionally associative and unital polynomial monads, we show how to arrive at a definition of opetopic type which is able to encode…
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…
Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)
Amin Timany, Matthieu Sozeau
In order to avoid well-know paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of…
The HoTT Library: A formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine +3
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including un…
Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study
Cyprien Mangin, Matthieu Sozeau
This paper presents a case study of formalizing a normalization proof for Leivant's Predicative System F using the Equations package. Leivant's Predicative System F is a stratified…