Logic representation in LF

DOI10.1007/BFb0018356zbMath1496.03055MaRDI QIDQ5096264

Andrzej Tarlecki, Robert Harper, Donald Sannella

Publication date: 16 August 2022

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

Mathematics Subject Classification ID

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

Related Items (3)

Structured theory presentations and logic representations ⋮ May I borrow your logic? (Transporting logical structures along maps) ⋮ A categorical study on the finiteness of specifications

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• Quasi-varieties in abstract algebraic institutions
• Generalized algebraic theories and contextual categories
• Specifications in an arbitrary institution
• Some fundamental algebraic tools for the semantics of computation. III: Indexed categories
• A framework for defining logics
• Axioms for abstract model theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Logic representation in LF