Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny
summary
Formalises that the denotational (language) and operational (deterministic automaton) semantics of regular expressions coincide, proving the inductive algebra homomorphism and the coalgebraic automaton-to-language map are unique and equal up to pointwise bisimilarity. Development uses Dafny’s inductive and coinductive features, encodes constructions as final coalgebra and initial algebra, and proves preservation of concatenation, union and star while working around lack of functional extensionality.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:44Motivation
- 1:28Regular expressions basics
- 3:17Semantics perspectives
- 5:47Algebraic semantics in Dafny
- 9:46Automata semantics in Dafny
- 11:15Equivalence of both semantic approaches
- 13:41Related work
- 15:29Conclusion & Q&A
related talks
30mRecognizing regular patterns in mixed type sequences using Symbolic Finite Automata
21mVerified VCG and Verified Compiler for Dafny
20mAlgebras for Deterministic Computation are Inherently Incomplete
58mCoalgebra for the working programming languages researcher
14mAdequacy for Algebraic Effects Revisited
14mEmbedding Quantum Program Verification into Dafny
18mCertified Semantics for Disequality
03mAttempts to design hardware using dafny