Finitary type theories with and without contexts

DOI10.1007/s10817-023-09678-yarXiv2112.00539OpenAlexW3216376486MaRDI QIDQ6053849

Andrej Bauer, Philipp G. Haselwarter

Publication date: 24 October 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2112.00539

zbMATH Keywords

proof assistantscontext-free-type theorydependent-type theoryformal meta-theory

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Generalized algebraic theories and contextual categories
• Type checking with universes
• A linear logical framework
• The locally nameless representation
• A lattice-theoretical fixpoint theorem and its applications
• Type theory in type theory using quotient inductive types
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• A framework for defining logics
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
• An extensible equality checking algorithm for dependent type theories
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Types for Proofs and Programs
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Unifying Cubical Models of Univalent Type Theory