The Operational Curry–Howard: Proof Discovery as Navigated Software Architecture
We propose a framework that unifies two perspectives on formal proof
construction: **proof as pathfinding** in a type-theoretic state
space and **proof as programming** via the Curry–Howard
correspondence.
Verified
26 claims
37,516 words