Deferring the Details and Deriving Programs
summary
Claims a proof-delay applicative that moves embedded proof terms out of data and program ASTs, implemented in Trip inside Agda. Builds a verification-condition generator that turns Agda typed holes into stepwise program derivation and an HList of delayed goals. Demonstrates on ordered lists, binary-search trees, a swap routine and a cumulative-sum writer, uses generated setter and guarded-assignment macros, and proves semantics and soundness; examples compile and require a short separate block of delayed proofs.
AI-written summary · about
chapters (6)
- 0:00Start
- 2:33Loop Invariant
- 3:00Arbitrary State Updates
- 3:21Rule of Consequence
- 4:09Deterministic Constructs
- 13:16Guarded Assignment
related talks
18mDeveloping a Dependently Typed Language with Runtime Proof Search
20mGenerating Well-Typed Terms that are not "Useless"
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
46mRefinement Types from Light to Deep Verification
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
41mTotal Functions for Automated Reasoning:Building Terminating Theorem Provers
01h 07mErasure In Dependently Typed Programming