Building 59, Room 1257
Speaker: Wojciech Różowski, University College London
Title: Well-behaved (Co)algebraic semantics of regular expressions in Dafny
Abstract:
This is a joint seminar with the Agents, Interaction and Complexity' group.
Regular expressions are commonly understood in terms of their denotational semantics, that is, through formal languages – the regular languages. This view is inductive in nature: two primitives are equivalent if they are constructed in the same way. Alternatively, regular expressions can be understood in terms of their operational semantics, that is, through deterministic finite automata. This view is coinductive in nature: two primitives are equivalent if they are deconstructed in the same way. It is implied by Kleene’s famous theorem that both views are equivalent: regular languages are precisely the formal languages accepted by deterministic finite automata.
In this talk, I describe a formally verified proof of what has been previously established only through proofs by hand: that the two semantics of regular expressions are well-behaved, in the sense that they are, in fact, one and the same, up to pointwise bisimilarity. To do so, I use Dafny, a verification-aware programming language relying on an SMT solver to discharge verification conditions. It turns out that Dafny is particularly well suited for the task due to its support for inductive and coinductive reasoning.
This is a joint work with Stefan Zetzsche (Amazon Web Services).
Bio:
Wojciech Różowski is a PhD candidate in the Programming Principles, Logic and Verification Group at University College London supervised by Alexandra Silva and Samson Abramsky. His research interests are centred around formal semantics of programming languages, logic and formal verification. At the same time, Wojciech works part-time as a Research Software Engineer at Lean FRO, contributing to the development of Lean theorem prover.