Logic representation in LF

DOI10.1007/BFB0018356MaRDI QIDQ5096264zbMATH OpenFDO

Authors Robert Harper, Donald Sannella, Andrzej Tarlecki

Publication date 16 August 2022

Published in Category Theory and Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0018356

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Type theory (03B38) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 3841852
• The rewriting logic semantics project: a progress report
• The rewriting logic semantics project: a progress report
• scientific article; zbMATH DE number 1231527
• Logic and Theory of Representation
• scientific article; zbMATH DE number 781332
• The Representation of Intensional Logics
• scientific article; zbMATH DE number 4028939
• On complete representations of algebras of logic
• scientific article; zbMATH DE number 1500177

Cites work

• A framework for defining logics
• Axioms for abstract model theory
• Generalized algebraic theories and contextual categories
• scientific article; zbMATH DE number 4130339 (Why is no real title available?)
• scientific article; zbMATH DE number 3837407 (Why is no real title available?)
• scientific article; zbMATH DE number 4180831 (Why is no real title available?)
• scientific article; zbMATH DE number 3864486 (Why is no real title available?)
• scientific article; zbMATH DE number 4097351 (Why is no real title available?)
• scientific article; zbMATH DE number 3657156 (Why is no real title available?)
• scientific article; zbMATH DE number 3714904 (Why is no real title available?)
• Quasi-varieties in abstract algebraic institutions
• Some fundamental algebraic tools for the semantics of computation. III: Indexed categories
• Specifications in an arbitrary institution
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(13)

• Structured theory presentations and logic representations
• May I borrow your logic? (Transporting logical structures along maps)
• An open logical framework
• Hybridizing a logical framework
• A proof theoretic interpretation of model theoretic hiding
• Towards logical frameworks in the heterogeneous tool set Hets
• scientific article; zbMATH DE number 2086323 (Why is no real title available?)
• scientific article; zbMATH DE number 4180831 (Why is no real title available?)
• scientific article; zbMATH DE number 516994 (Why is no real title available?)
• scientific article; zbMATH DE number 1948185 (Why is no real title available?)
• Equivalences between logics and their representing type theories
• scientific article; zbMATH DE number 1418814 (Why is no real title available?)
• A categorical study on the finiteness of specifications

This page was built for publication: Logic representation in LF

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