A type theory for defining logics and proofs

DOI10.5555/3470152.3470181MaRDI QIDQ6654495zbMATH OpenFDO

Authors Brigitte Pientka, David Thibodeau, Andreas Abel, Francisco Ferreira, Rebecca Zucchini

Publication date 19 December 2024

Mathematics Subject Classification ID

Type theory (03B38)

Recommendations

• A framework for defining logics
• scientific article; zbMATH DE number 516994
• Reasoning with higher-order abstract syntax in a logical framework
• Some normalization properties of Martin-Löf's type theory, and applications
• A modular construction of type theories

Cited in

(2)

• For the metatheory of type theory, internal sconing is enough
• Semantical analysis of contextual types

This page was built for publication: A type theory for defining logics and proofs

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