Readings shared March 1, 2026
The readings shared in Bluesky on 1 March 2026 are:
- Lean for science formalization. ~ Przemyslaw Chojecki. #LeanProver #ITP
- Vibe-coding a debugger for a DSL. ~ Joachim Breitner. #LeanProver
- Bidirectional interpolation for the lambda-calculus – Revisiting and formalising Craig-Čubrić interpolation. ~ Meven Lennon-Bertrand, Alexis Saurin. #RocqProver #ITP
- Machine-generated, machine-checked proofs for a verified compiler (Experience report). ~ Zoe Paraskevopoulou. #RocqProver #ITP