Metaprogramming, Synthesis & Verification • Nada Amin • YOW! 2025

From the creator

This presentation was recorded at YOW! Australia 2025. #GOTOcon #YOW https://yowcon.com Nada Amin - Assistant Professor of Computer Science at Harvard SEAS RESOURCES https://github.com/namin https://www.linkedin.com/in/mitnamin https://cv.namin.org Links https://namin.seas.harvard.edu https://github.com/namin/dafny-sketcher https://github.com/namin/staged-miniKanren https://github.com/namin/llm-verified-with-monte-carlo-tree-search https://github.com/namin/holey https://github.com/metareflection/dafny-annotator https://github.com/namin/eurisclo https://io.livecode.ch/learn/gregr/icfp2017-artifact-auas7pp ABSTRACT 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,

Published 2026-06-02 · Watch on YouTube ↗
Availability and playback restrictions are controlled by the original channel.