Executable Formal Specification of Programming Languages with Reusable Components

L. Thomas van Binsbergen

Research output: ThesisDoctoral Thesis

128 Downloads (Pure)


Writing a formal definition of a programming language is cumbersome and maintaining the definition as the language evolves is tedious and error-prone.
But programming languages have commonalities that can be captured once and for all and used in the formal definition of multiple languages, potentially easing the task of developing and maintaining 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 prefix and infix operators.

The PLanCompS project has established a formal and component-based approach to semantics intended to reduce development and maintenance costs by employing the software engineering practices of reuse and testing.
This thesis contributes further, taking advantage of the advanced features of the Haskell programming language to define *executable* and *reusable* components for specifying both syntax and semantics.

The main theoretical contributions of this thesis are:
* a data structure for representing the possibly many derivations found by a generalised parser which significantly simplifies the specification of generalised parsing algorithms,
* a purely functional description of GLL parsing based on this data structure,
* a novel approach to combinator parsing that incorporates generalised parsing algorithms such as GLL in their implementation,
* and a novel and lightweight framework for developing modular rule-based semantic specifications (MRBS).

The main practical contributions of this thesis are:
* a combinator library for component-based descriptions of context-free grammars from which GLL parsers are generated,
* a compiler and interpreter for executing operational semantic specifications written in CBS (the meta-language developed by the PLanCompS project),
* an interpreter for an intermediate meta-language (IML) based on MRBS,
* and a translation from CBS specifications into IML that gives an operational semantics to CBS.

The practicality of the presented tools is evaluated through case studies.
Original languageEnglish
Awarding Institution
  • Royal Holloway, University of London
  • Johnstone, Adrian, Supervisor
  • Scott, Elizabeth, Supervisor
Award date1 Apr 2019
Publication statusUnpublished - 2019


  • syntax analysis
  • top-down parsing
  • generalised parsing
  • parser combinators
  • operational semantics
  • structural operational semantics
  • MSOS
  • reusable semantics
  • reusable components
  • component-based semantics
  • caml light

Cite this