A5033071564- Logic, programming, and type systems
- Logic, Reasoning, and Knowledge
- Semantic Web and Ontologies
- Formal Methods in Verification
- Advanced Algebra and Logic
- Gender, Labor, and Family Dynamics
- Homotopy and Cohomology in Algebraic Topology
- Multi-Agent Systems and Negotiation
- Natural Language Processing Techniques
Stockholm University
2024-2025
Institut national de recherche en informatique et en automatique
2020-2023
We present an extensive mechanization of the metatheory Martin-Löf Type Theory (MLTT) in Coq proof assistant. Our development builds on pre-existing work Agda to show not only decidability conversion, but also type checking, using approach guided by bidirectional checking. From our decidability, we obtain a certified and executable checker for full-fledged version MLTT with support Π, Σ, ℕ, Id types, one universe. does rely impredicativity, induction-recursion or any axiom beyond extended...
The notion of equality is at the heart dependent type theory, as it plays a fundamental role in program specifications and mathematical reasoning. In mainstream proof assistants such Agda , Lean Coq usually defined using Martin-Löf’s identity type, an elegant simple approach that has stood test time since 1970s. However, this definition also comes with serious downsides: intensional nature means impractical for reasoning about functions predicates, impossible to define quotient types....
Building on the recent extension of dependent type theory with a universe definitionally proof-irrelevant types, we introduce TTobs, new based setoidal interpretation theory. TTobs equips every an identity relation that satisfies function extensionality, propositional and definitional uniqueness proofs (UIP). Compared to other existing proposals enrich these principles, our features notion reduction is normalizing provides algorithmic canonicity result, which formally prove in Agda using...
In dependent type theory, impredicativity is a powerful logical principle that allows the definition of propositions quantify over arbitrarily large types, potentially resulting in self-referential propositions. Impredicativity can provide system with increased strength and flexibility, but counterpart it comes multiple incompatibility results. particular, Abel Coquand showed adding definitional uniqueness identity proofs (UIP) to main proof assistants support impredicative (Coq Lean) breaks...
Homotopy type theory is an extension of that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations multiple classical results from However, many proofs are still surprisingly complicated formalize. One reason for this the axiomatic treatment univalence higher inductive types which complicates as intermediate steps, could hold simply by computation, require explicit arguments. Cubical offers a solution in form new with native support...
We present an extensive mechanization of the meta-theory Martin-L\"of Type Theory (MLTT) in Coq proof assistant. Our development builds on pre-existing work Agda to show not only decidability conversion, but also type checking, using approach guided by bidirectional checking. From our decidability, we obtain a certified and executable checker for full-fledged version MLTT with support $\Pi$, $\Sigma$, $\mathbb{N}$, identity types, one universe. Furthermore, does rely impredicativity,...