Implementing the meta-theory of deductive systems

DOI10.1007/3-540-55602-8_190MaRDI QIDQ4264727zbMATH OpenFDO

Authors Ekkehard Rohwedder, Frank Pfenning

Publication date 10 October 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-55602-8_190

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Abstract deductive systems (03B22) Mechanization of proofs and logical operations (03B35) Relative consistency and interpretations (03F25)

Recommendations

• Mechanizing metatheory in a logical framework
• scientific article; zbMATH DE number 4180832
• Logical frameworks
• scientific article; zbMATH DE number 2110615

Cited in

(11)

• Proof-search in type-theoretic languages: An introduction
• Mechanized metatheory revisited
• A metatheory of a mechanized object theory
• Adding metatheoretic facilities to first-order theories
• Explicit contexts in LF (extended abstract)
• scientific article; zbMATH DE number 4155932 (Why is no real title available?)
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• Structuring metatheory on inductive definitions
• Representing proof transformations for program optimization
• The practice of logical frameworks
• On extensibility of proof checkers

Describes a project that uses

Uses Software

• Elf

This page was built for publication: Implementing the meta-theory of deductive systems

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