Comparing higher-order encodings in logical frameworks and tile logic

DOI10.1016/S1571-0661(04)00324-XMaRDI QIDQ2841275zbMATH OpenOpenAlexFDO

Authors Roberto Bruni, Furio Honsell, Marina Lenisa, Marino Miculan

Publication date 24 July 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s1571-0661(04)00324-x

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• Encoding modal logics in logical frameworks
• Expressibility of higher order logics
• scientific article; zbMATH DE number 1089034
• Higher-order representation of substructural logics
• scientific article; zbMATH DE number 4047723
• Reasoning with higher-order abstract syntax in a logical framework
• scientific article; zbMATH DE number 1926604
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF

Cites work

• -calculus in (Co)inductive-type theory
• A calculus of mobile processes. II
• A framework for defining logics
• A natural extension of natural deduction
• A theory of bisimulation for the -calculus
• An interactive semantics of logic programming
• Comparing cospan-spans and tiles via a Hoare-style process calculus
• Compositional SOS and beyond: A coalgebraic view of open systems
• Conditional rewriting logic as a unified model of concurrency
• Full abstraction in the lazy lambda calculus
• scientific article; zbMATH DE number 1189279 (Why is no real title available?)
• scientific article; zbMATH DE number 1231660 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 1754648 (Why is no real title available?)
• scientific article; zbMATH DE number 1759616 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Using typed lambda calculus to implement formal systems on a machine

Cited in

(3)

• Comparing logics for rewriting: Rewriting logic, action calculi and tile logic
• A third-order representation of the -calculus
• Tiling transactions in rewriting logic

Describes a project that uses

Uses Software

• Coq
• LEGO

This page was built for publication: Comparing higher-order encodings in logical frameworks and tile logic

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