Implementing λ-calculus reduction strategies in extended logic programming languages

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


We study the implementation of four reduction strategies for the untyped λ-calculus in the logic programming language λProlog and restricted sublanguages. The higher-order features of these languages provide very natural methods for manipulating and substituting bound variables. Starting from clear and concise specifications of reduction in the full language we demonstrate how to make certain details in the implementations explicit as we restrict ourselves to the weaker sublanguages. We also show how to translate specifications in a higher-order language to a first-order one, such as Prolog, introducing closures as a replacement for substitutions. This process illustrates how a very high-level description of an implementation can be translated to lower-level ones by reasoning about the logic in which the descriptions are given. It also illustrates some basic methods for manipulating functional languages represented in a higher-order abstract syntax.

Original languageEnglish (US)
Title of host publicationExtensions of Logic Programming - 2nd International Workshop, ELP 1991, Proceedings
EditorsLars-Henrik Eriksson, Lars Hallnas, Peter Schroeder-Heister
PublisherSpringer Verlag
Number of pages27
ISBN (Print)9783540554981
StatePublished - 1992
Event2nd International Workshop on Extensions of Logic Programming, ELP 1991 - Stockholm, Sweden
Duration: Jan 27 1991Jan 29 1991

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume596 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other2nd International Workshop on Extensions of Logic Programming, ELP 1991

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Implementing λ-calculus reduction strategies in extended logic programming languages'. Together they form a unique fingerprint.

Cite this