Primitive recursion for higher-order abstract syntax

DOI10.1016/S0304-3975(00)00418-7zbMath0994.68028MaRDI QIDQ5958752

Joëlle Despeyroux, Frank Pfenning, Carsten Schuermann

Publication date: 3 March 2002

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

zbMATH Keywords

modal logichigher-order abstract syntaxprimitive recursiontyped lambda calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Self-quotation in a typed, intensional lambda-calculus, Normalization by evaluation for modal dependent type theory, Rensets and renaming-based recursion for syntax with bindings extended version, A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names., Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, The calculus of dependent lambda eliminations, A formalized general theory of syntax with bindings: extended version, Structural recursion with locally scoped names, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, A Simple Nominal Type Theory, Unnamed Item, Higher-order unification revisited: Complete sets of transformations, Developing (Meta)Theory of λ-calculus in the Theory of Contexts1 1Work partially supported by Italian MURST project tosca and EC-WG types., Rensets and renaming-based recursion for syntax with bindings

Uses Software

• Coq
• Nuprl
• ALF
• Elf
• MiniML

Cites Work

• A modal analysis of staged computation
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item