MOLA: A Runtime Verification Engine Factory by (Meta-)interpreting Embedded DSLs
summary
Mola implements a meta-interpreter factory for stream runtime verification: HLoLA specs become stringly-typed trees, a theory engineer role binds symbols to Haskell values and annotated types, then GHC + the reflection package compile a specialized interpreter for that domain. It adds type inference and unification, uses Read to decode constants, and keeps Haskell type safety. Example theories (booleans, integers, UAV, blockchain) compile into engines that run thousands–hundreds of thousands events/sec and give tool-level error messages.
AI-written summary · about
chapters (7)
- 0:00MOLA runtime verification intro
- 1:28Stream runtime verification background
- 3:16Lola EDSL limitations
- 5:04MOLA meta-interpreter intro
- 8:17Decoding expressions with theory tables
- 11:46MOLA approach summary
- 13:49Q&A: Specializing meta-interpreter
related talks
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
31mHigh Assurance Software for Financial Regulation and Business Platforms
01h 05mVerifying Infinitely Many Programs at Once
01h 02mMelocoton: A Program Logic for Verified Interoperability Between OCaml and C (I...
22mVerification Modulo Tested Library Contracts
30mTrustworthy Runtime Verification via Bisimulation
31mVerified Software at Scale
12mTowards Self-Adaptable Languages