InBound : Simple yet powerful Specification of Syntax with Binders [pdf] [bib]

Abstract

Nearly all meta-programming tools need to deal with binders in abstract syntax trees. Unfortunately, ubiquitous boilerplate functions for computing free variables and variable substitution are remarkably intricate and hard to get right. Moreover, the complexity quickly increases with larger languages and non-trivial binding forms. On top of that, the underlying scoping rules are only implicitly encoded in these function definitions. Because their logic has to be repeated across functions, this leaves ample space for inconsistencies. In short, programming with binders is a pain!

Our new specification language InBound brings much needed relief: it allows programmers to explicitly state the scoping rules of syntax with binders in a concise and intuitive manner. From such a specification the InBound compiler automatically generates the boilerplate functions, and takes care of all the intricacies as well as mutual consistency.

We illustrate InBound with a number of examples and two larger case studies, including a simple type checker for Haskell. These show that InBound easily scales to larger languages and complex binding situations.

BibTeX

@unpublished{infragen,
  author = "Keuchel, Steven and Schrijvers, Tom",
  title =  "{InBound : Simple yet powerful Specification of
             Syntax with Binders}",
  year =   "2015",
  note =   "Unpublished Draft",
  url =
  "https://skeuchel.me/publication/2015-draft-inbound-simple-yet-powerful-specification-of-syntax-with-binders"
}