Primitive recursion for higher-order abstract syntax

DOI10.1016/S0304-3975(00)00418-7MaRDI QIDQ5958752zbMATH OpenFDO

Authors Carsten Schürmann, J. Despeyroux, Frank Pfenning

Publication date 3 March 2002

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

Full work available at URL https://doi.org/10.1016/S0304-3975(00)00418-7

zbMATH Keywords

higher-order abstract syntaxmodal logicprimitive recursiontyped lambda calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 2185713
• Primitive recursion in the abstract
• scientific article; zbMATH DE number 1390021
• Recursion principles for syntax with bindings and substitution
• scientific article; zbMATH DE number 445161
• Programming Languages and Systems
• Term rewriting theory for the primitive recursive functions

Cites work

• A framework for defining logics
• A modal analysis of staged computation
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 2185713 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 65531 (Why is no real title available?)
• scientific article; zbMATH DE number 1231474 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 559219 (Why is no real title available?)

Cited in

(31)

• A recursive second order initial algebra specification of primitive recursion
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• Higher-order unification revisited: Complete sets of transformations
• A formalized general theory of syntax with bindings: extended version
• Rensets and renaming-based recursion for syntax with bindings
• Self-quotation in a typed, intensional lambda-calculus
• Recursion over objects of functional type
• scientific article; zbMATH DE number 1722696 (Why is no real title available?)
• A simple nominal type theory
• Developing (meta)theory of -calculus in the theory of contexts
• A third-order representation of the -calculus
• Functional programming with higher-order abstract syntax and explicit substitutions
• A type-theoretic approach to induction with higher-order encodings
• Structural recursion with locally scoped names
• scientific article; zbMATH DE number 2185713 (Why is no real title available?)
• scientific article; zbMATH DE number 445161 (Why is no real title available?)
• Focusing and higher-order abstract syntax
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• scientific article; zbMATH DE number 2079037 (Why is no real title available?)
• Stratified polymorphism and primitive recursion
• scientific article; zbMATH DE number 1841845 (Why is no real title available?)
• scientific article; zbMATH DE number 1420785 (Why is no real title available?)
• Dual-context calculi for modal logic
• The calculus of dependent lambda eliminations
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
• scientific article; zbMATH DE number 5033764 (Why is no real title available?)
• Typed Lambda Calculi and Applications
• Normalization by evaluation for modal dependent type theory
• Rensets and renaming-based recursion for syntax with bindings extended version
• A weakly initial algebra for higher-order abstract syntax in Cedille
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions

Describes a project that uses

Uses Software

• MiniML
• ALF
• Elf
• Nuprl
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5958752)