×

Binding structures as an abstract data type. (English) Zbl 1335.68153

Vitek, Jan (ed.), Programming languages and systems. 24th 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. Berlin: Springer (ISBN 978-3-662-46668-1/pbk; 978-3-662-46669-8/ebook). Lecture Notes in Computer Science 9032, 762-786 (2015).
Summary: 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.
For the entire collection see [Zbl 1333.68020].

MSC:

68Q65 Abstract data types; algebraic specification
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI Link