scientific article; zbMATH DE number 4180831

MaRDI QIDQ3204067zbMATH OpenFDO

Authors Robert Harper, Donald Sannella, Andrzej Tarlecki

Publication date 1989

zbMATH Keywords

logical frameworktype theoriestyped \(\lambda \) -calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic programming (68N17) Logic in artificial intelligence (68T27) Artificial intelligence (68T99)

Recommendations

• Logic representation in LF
• Structured theory presentations and logic representations
• An open logical framework
• scientific article; zbMATH DE number 65531
• Towards logical frameworks in the heterogeneous tool set Hets

Cited in

(18)

• Structured theory presentations and logic representations
• Proof systems for structured specifications with observability operators
• Logical frameworks. Why not just classical logic?
• Explicit contexts in LF (extended abstract)
• A proof theoretic interpretation of model theoretic hiding
• Towards logical frameworks in the heterogeneous tool set Hets
• The Twelf Proof Assistant
• scientific article; zbMATH DE number 1231543 (Why is no real title available?)
• scientific article; zbMATH DE number 516994 (Why is no real title available?)
• An axiomatic approach to structuring specifications
• scientific article; zbMATH DE number 1542840 (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?)
• Proof systems for structured algebraic specifications: An overview
• Logic representation in LF
• Toward formal development of programs from algebraic specifications: model-theoretic foundations
• Types for Proofs and Programs
• Grothendieck inclusion systems

This page was built for publication:

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