Higher-order substitutions

DOI10.1006/inco.2000.2887zbMath1003.68024OpenAlexW2086668518MaRDI QIDQ1854398

Dominic Duggan

Publication date: 14 January 2003

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/af077063343bf186a69e225ce205923fba20f6a0

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items

Unification with extended patterns

Uses Software

• Haskell
• Nuprl
• Automath
• ALF
• ALGOL 60

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A theory of binding structures and applications to rewriting
• The calculus of constructions
• Higher-order rewrite systems and their confluence
• An efficient interpreter for the lambda-calculus
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Conditional lambda-theories and the verification of static properties of programs
• Uniform proofs as a foundation for logic programming
• On theories with a combinatorial definition of 'equivalence'
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Explicit substitutions
• Correspondence between ALGOL 60 and Church's Lambda-notation
• The Calculi of Lambda Conversion. (AM-6)
• Correctness of procedure representations in higher-order assembly language