Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic

DOI10.1016/S1571-0661(04)00324-XzbMath1268.68047OpenAlexW1544527987MaRDI QIDQ2841275

Furio Honsell, Roberto Bruni, Marino Miculan, Marina Lenisa

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

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

Uses Software

• Coq
• LEGO

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Using typed lambda calculus to implement formal systems on a machine
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Conditional rewriting logic as a unified model of concurrency
• A calculus of mobile processes. II
• Full abstraction in the lazy lambda calculus
• \(\pi\)-calculus in (Co)inductive-type theory
• Compositional SOS and beyond: A coalgebraic view of open systems
• A theory of bisimulation for the \(\pi\)-calculus
• Comparing cospan-spans and tiles via a Hoare-style process calculus
• A natural extension of natural deduction
• A framework for defining logics
• An interactive semantics of logic programming

This page was built for publication: Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic