A type and scope safe universe of syntaxes with binding: their semantics and proofs

Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna

Research output: Contribution to journalConference Contributionpeer-review

71 Downloads (Pure)

Abstract

Almost every programming language’s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs.

We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material.
Original languageEnglish
Article number90
Pages (from-to)1-30
Number of pages30
JournalProceedings of the ACM on Programming Languages (PACMPL)
Volume2
Issue numberICFP
Early online date31 Jul 2018
DOIs
Publication statusPublished - 23 Sep 2018
EventInternational Conference on Functional Programming 2018 - St. Louis, United States
Duration: 23 Sep 201829 Sep 2018

Keywords

  • generic programming
  • syntax with binding
  • semantics
  • logical relations
  • simulation
  • fusion
  • agda

Fingerprint

Dive into the research topics of 'A type and scope safe universe of syntaxes with binding: their semantics and proofs'. Together they form a unique fingerprint.

Cite this