scientific article; zbMATH DE number 2185713

MaRDI QIDQ3024905zbMATH OpenFDO

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

Publication date 4 July 2005

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Primitive recursion for higher-order abstract syntax
• 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

Cited in

(22)

• A recursive second order initial algebra specification of primitive recursion
• Nominal logic, a first order theory of names and binding
• Recursion over objects of functional type
• scientific article; zbMATH DE number 1722696 (Why is no real title available?)
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• A representation of \(F_{\omega}\) in LF
• 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
• Programming inductive proofs. A new approach based on contextual types
• Focusing and higher-order abstract syntax
• scientific article; zbMATH DE number 2079037 (Why is no real title available?)
• scientific article; zbMATH DE number 1927423 (Why is no real title available?)
• Stratified polymorphism and primitive recursion
• scientific article; zbMATH DE number 1841845 (Why is no real title available?)
• Formalizing type operations using the ``image type constructor
• scientific article; zbMATH DE number 1420785 (Why is no real title available?)
• scientific article; zbMATH DE number 5033764 (Why is no real title available?)
• Typed Lambda Calculi and Applications
• Primitive recursion for higher-order abstract syntax
• Closed nominal rewriting and efficiently computable nominal algebra equality
• Cut-free Gentzen calculus for multimodal CK

Describes a project that uses

Uses Software

• ALF
• Elf
• Coq

This page was built for publication:

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