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 (15)

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

This page was built for publication: Primitive recursion for higher-order abstract syntax