Verified Interpreters for Dynamic Languages with Applications to the Nix Expression(…)

on YouTube ↗21m

" summary

Paper presents a substitution-based operational semantics using deferred substitutions for dynamic name binding, extends call-by-name lambda calculus to model Nix features, and develops corresponding environment interpreters proven sound and complete for terminating, faulty, and diverging programs (including open terms). All proofs and a verified interpreter are mechanized in Rocq using rocq-std++ maps, the Rocq extraction produces executable OCaml, and the interpreter runs against the official Nix language tests (artifacts available; some tests differ due to call-by-name vs Nix laziness).

AI-written summary · about

" chapters (21)

1. 0:00Formal semantics for Nix
2. 1:05Nix needs formal semantics
3. 2:08Nix expression language
4. 3:11Nix expression features
5. 4:13Dynamic binding in Nix
6. 5:59Evaluation strategies in Nix
7. 7:01Limitations of Nix semantics
8. 8:03Substitution-based semantics challenges
9. 9:30Deferred substitutions for open programs
10. 10:53Core calculus with deferred substitutions
11. 12:11Shadowing in Nix with deferred substitutions
12. 13:14Extending deferred substitutions
13. 14:15Nix language grammar
14. 14:57Verified interpreters and tests
15. 15:38Contributions and evaluation
16. 16:05Q&A: Program logic
17. 16:49Q&A: Laziness and semantics
18. 17:54Q&A: 'with' feature necessity
19. 18:35Q&A: Completeness of verification
20. 19:39Q&A: Verifying build systems
21. 20:43Q&A: Future work