Speaker:

   Thomas van Binsbergen (Royal Holloway)

Title: 

   Formal, executable and reusable components for syntax specification

Abstract: 

   Developing a programming language formally is cumbersome and
   maintaining the language definition as it evolves is tedious and
   error-prone. But programming languages have syntactic and semantic
   commonalities that can be captured once and for all, potentially
   easing the task of developing and maintaining language
   definitions. Languages often share features, even across paradigms,
   such as scoping rules, function calls, and control
   operators. Moreover, some concrete syntaxes share patterns such as
   repetition with a separator, delimiters around blocks, and the
   application of prefix and infix operators.

   In this talk we contrast two possible routes for capturing
   syntactic features of languages in a library of reusable
   components. The components should be executable, so that a syntax
   definition can be tested as it is being developed, and formal, so
   that mathematical claims can be made about specifications and the
   languages being defined.

   In the first route, the well-known BNF formalism is extended with a
   mechanism for abstraction, borrowed from modern programming
   languages. With the abstraction mechanism, it is possible to define
   syntactic templates in which certain elements are variable and can
   be instantiated as needed. Complete syntax specifications are
   mechanically translated into conventional BNF. The formalism thus
   inherits all the advantages of conventional BNF: a rich formal
   theory and generalised parsing technology. An example
   implementation is found in Happy, the standard parser generator for
   Haskell.

   In the second route, we demonstrate the expressive power of parser
   combinators. We define parser combinators that satisfy certain
   combinator laws, allowing us to reason formally about the parsers
   defined with these combinators. However, care must be taken to
   avoid non-terminating and inefficient parsers. Several authors have
   made suggestions to overcome these issues. However, these
   suggestions significantly complicate the combinator definitions,
   making it hard to maintain the combinator laws.

   We have taken a third route, which is to define *grammar*
   combinators, simultaneously generating grammars and parsers,
   effectively implementing the BNF formalism as an embedded
   DSL. Implemented in Haskell, the the grammar combinators piggyback
   on Haskell's abstraction mechanism and on Haskell's strong
   type-system to integrate semantic actions in grammar
   specifications. The grammar combinators are at the heart of a
   library of formal, executable and reusable components. With this
   library, it is possible to apply software design principles like
   "reuse via abstraction" and "test-driven development" to the
   development of programming languages.