Metaprogramming, Synthesis, and Verification
You need to be signed in to add a collection
With live examples Nada will demonstrate: * **Dafny and verification-aware programming**, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics). * **Multi-stage programming**, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis. * **Monte Carlo Tree Search**, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems. The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).
Transcript
With live examples Nada will demonstrate:
- Dafny and verification-aware programming, including proof by induction to verify properties of programs (for example, that an optimizer preserves semantics).
- Multi-stage programming, a principled approach to writing programs that write programs, and its incarnation in multi-stage relational programming for faster synthesis of programs with holes—with the theoretical insight that a staged interpreter is a compiler, and a staged relational interpreter for a functional language can turn functions into relations running backwards for synthesis.
- Monte Carlo Tree Search, specifically the VerMCTS variant, and when this exploration-exploitation sweet spot is a good match for synthesis problems.
The ideas will be demonstrated with live examples and open-source artifacts spanning verified programming, relational programming, and LLM-guided synthesis, including Dafny Sketcher (https://github.com/namin/dafny-sketcher), multi-stage miniKanren (https://github.com/namin/staged-miniKanren), VerMCTS (https://github.com/namin/llm-verified-with-monte-carlo-tree-search), and Holey (https://github.com/namin/holey).
About the speakers
Assistant Professor of Computer Science at Harvard SEAS