Binding Structures as an Abstract Data Type

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


A long line of research has been dealing with the representation, in a formal tool such as an interactive theorem prover, of languages with binding structures (e.g. the lambda calculus). Several concrete encodings of binding have been proposed, including de Bruijn dummies, the locally nameless representation, and others. Each of these encodings has its strong and weak points, with no clear winner emerging. One common drawback to such techniques is that reasoning on them discloses too much information about what we could call “implementation details”: often, in a formal proof, an unbound index will appear out of nowhere, only to be substituted immediately after; such details are never seen in an informal proof. To hide this unnecessary complexity, we propose to represent binding structures by means of an abstract data type, equipped with high level operations allowing to manipulate terms with binding with a degree of abstraction comparable to that of informal proofs. We also prove that our abstract representation is sound by providing a de Bruijn model.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages5
ISBN (Electronic)978-3-662-46669-8
ISBN (Print)978-3-662-46668-1
Publication statusPublished - 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Binding Structures as an Abstract Data Type'. Together they form a unique fingerprint.

Cite this