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

inductionhigher-order abstract syntaxlogical frameworks

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Nominal logic, a first order theory of names and binding, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts, The Theory of Contexts for First Order and Higher Order Abstract Syntax

Uses Software

• Coq
• Isabelle/HOL
• Twelf

Cites Work

• Using typed lambda calculus to implement formal systems on a machine
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Full abstraction in the lazy lambda calculus
• \(\pi\)-calculus in (Co)inductive-type theory
• A framework for defining logics
• Automating inversion of inductive predicates in Coq
• Consistency of the theory of contexts
• Primitive recursion for higher-order abstract syntax
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item