αProlog: A Logic Programming Language with Names, Binding and α-Equivalence

James Cheney, Christian Urban

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

Abstract / Description of output

There are two well-known approaches to programming with names, binding, and equivalence up to consistent renaming: representing names and bindings as concrete identifiers in a first-order language (such as Prolog), or encoding names and bindings as variables and abstractions in a higher-order language (such as λProlog). However, both approaches have drawbacks: the former often involves stateful name-generation and requires manual definitions for α-equivalence and capture-avoiding substitution, and the latter is semantically very complicated, so reasoning about programs written using either approach can be very difficult. Gabbay and Pitts have developed a new approach to encoding abstract syntax with binding based on primitive operations of name-swapping and freshness. This paper presents αProlog, a logic programming language that uses this approach, along with several illustrative example programs and an operational semantics.
Original languageEnglish
Title of host publicationLogic Programming
EditorsBart Demoen, Vladimir Lifschitz
PublisherSpringer Berlin Heidelberg
Pages269-283
Number of pages15
Volume3132
ISBN (Electronic)978-3-540-27775-0
ISBN (Print)978-3-540-22671-0
DOIs
Publication statusPublished - 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume3132

Fingerprint

Dive into the research topics of 'αProlog: A Logic Programming Language with Names, Binding and α-Equivalence'. Together they form a unique fingerprint.

Cite this