A modular construction of type theories

DOI10.46298/LMCS-19(1:12)2023MaRDI QIDQ5883738zbMATH OpenOpenAlexFDO

Authors Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger

Publication date 22 March 2023

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

\(\lambda\Pi\)-calculus modulo rewritingDeduktilogiclogical frameworktype theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 7204561
• scientific article; zbMATH DE number 1678369
• The calculus of constructions
• Coquand's calculus of constructions: A mathematical foundation for a proof development system

Cites work

• A framework for defining logics
• Combinatory reduction systems: Introduction and survey
• Dependency pairs termination in dependent type theory modulo rewriting
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 2185666 (Why is no real title available?)
• scientific article; zbMATH DE number 7034416 (Why is no real title available?)
• scientific article; zbMATH DE number 7034428 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 7204561 (Why is no real title available?)
• scientific article; zbMATH DE number 963644 (Why is no real title available?)
• Proof normalization modulo
• Semantic A-translations and super-consistency entail classical cut elimination
• Some Axioms for Mathematics
• Term Rewriting and Applications
• The calculus of constructions
• Theorem proving modulo

Cited in

(31)

• Construction of tame types
• Modularity of proof-nets. Generating the type of a module.
• A modern perspective on type theory. From its origins until today
• A type system for higher-order modules
• scientific article; zbMATH DE number 2185711 (Why is no real title available?)
• Automorphisms of types in certain type theories and representation of finite groups
• A minimalistic many-valued theory of types
• A very modal model of a modern, major, general type system
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• A module calculus for Pure Type Systems
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• scientific article; zbMATH DE number 65526 (Why is no real title available?)
• scientific article; zbMATH DE number 1301730 (Why is no real title available?)
• scientific article; zbMATH DE number 1070622 (Why is no real title available?)
• Modular types in some supersimple theories
• PAL⁺: a lambda-free logical framework
• A Modular Type Reconstruction Algorithm
• On the Structure of Mizar Types
• A Formal System for the Universal Quantification of Schematic Variables
• Dialectica models of type theory
• Modeling abstract types in modules with open existential types
• Principal Type Schemes for Modular Programs
• The metatheory of UTT
• Native type theory
• Encoding type universes without using matching modulo associativity and commutativity
• From rewrite rules to axioms in the \(\lambda \varPi \)-calculus modulo theory
• Sharing proofs with predicative theories through universe-polymorphic elaboration
• A type theory for defining logics and proofs
• Lean4Less: eliminating definitional equalities from Lean via an extensional-to-intensional translation
• Impredicativity, cumulativity and product covariance in the logical framework dedukti
• Translating HOL-Light proofs to Coq

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A modular construction of type theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5883738)