Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types.

DOI10.1016/S1571-0661(04)00278-6zbMath1268.68050MaRDI QIDQ2841233

Marino Miculan

Publication date: 24 July 2013

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

zbMATH Keywords

induction; higher-order abstract syntax; logical frameworks

Mathematics Subject Classification ID

DB lookup for MSC labels failed

Uses Software

• Coq
• Isabelle/HOL
• Twelf