The Theory of Contexts for First Order and Higher Order Abstract Syntax

DOI10.1016/S1571-0661(04)00323-8zbMath1268.68048OpenAlexW1600588339MaRDI QIDQ2841274

Furio Honsell, Marino Miculan, Ivan Scagnetto

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)00323-8

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

A canonical locally named representation of binding, Mechanizing type environments in weak HOAS, \(\mathrm{HO}\pi\) in Coq

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• The lambda calculus. Its syntax and semantics. Rev. ed.
• \(\pi\)-calculus in (Co)inductive-type theory
• Some lambda calculus and type theory formalized
• Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types.
• A framework for defining logics
• Automating inversion of inductive predicates in Coq