Full Workshop
summary
A fast tour of research tools and case studies from ML 2021: a running effect-handler Unix model that composes write/exit/su/fork/interrupt handlers and reproduces interleaved outputs; Camellia that translates Gospel-annotated OCaml to Why3 and discharges VCs with Alt-Ergo; Hobbit for contextual equivalence using up-to techniques that cuts proofs from thousands to seconds; Coq→OCaml/Tezos/Elm extraction with Metacoq; a verified lexer generator, GADT formalization, datatype-unfolding algorithm, frozen-constraint disambiguation, F# history plus domain-modelling patterns and a symbolic-math toolkit—most prototypes compile or run, and several case studies report full automatic proofs or dramatic speedups.
AI-written summary · about
related talks
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
27mTry-Mopsa: Relational Static Analysis in Your Pocket
01h 10mMedium-scale automation for proof assistants
35mLightning Talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
27mParsing, Compiling, and Static Metaprogramming
43mOCaml at LexiFi
01h 00mIntro to FP in Scala: Exploring a Toolbox for Solving Problems - Part 2 of 6