Combining predicate transformer semantics for effects: a case study in parsing regular languages

Anne Baanen
(Vrije Universiteit Amsterdam)
Wouter Swierstra
(Utrecht Univeristy)

This paper describes how to verify a parser for regular expressions in a functional programming language using predicate transformer semantics for a variety of effects. Where our previous work in this area focused on the semantics for a single effect, parsing requires a combination of effects: non-determinism, general recursion and mutable state. Reasoning about such combinations of effects is notoriously difficult, yet our approach using predicate transformers enables the careful separation of program syntax, correctness proofs and termination proofs.

In Max S. New and Sam Lindley: Proceedings Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020), Dublin, Ireland, 25th April 2020, Electronic Proceedings in Theoretical Computer Science 317, pp. 39–56.
Published: 1st May 2020.

ArXived at: bibtex PDF

Comments and questions to:
For website issues: