Papers
Browse the current collection. Each entry includes its publication details, abstract, downloadable PDF, and an embedded reader.
2026
A Cubical Path from Algebra to Analysis
Abstract—We connect algebraic interfaces to constructive analysis in Cubical Agda, tracing a path through ordered rings, premetric spaces, completions, continuity, and real-number infrastructure. The work demonstrates how informal mathematical intent can be decomposed into reusable checked components that support later high-stakes formalization work. It also shows how reusable real-number components can carry definitions across a larger development.
Read paper Download PDF2025
Formal Foundry Whitepaper
Abstract—A position paper on AI-assisted formalization where proof assistants remain the deterministic checking boundary. It frames AI as an accelerator for drafting, search, and translation, while formal definitions and checked proofs provide the audit trail needed for large-scale correctness in complex intelligent systems. The emphasis is not automation alone, but a reviewable boundary where generated candidates become trustworthy artifacts only after deterministic checking.
Read paper Download PDF2026
Implementation Towers
Abstract—A framework for layered implementations with safe domains, observability, liveness, migration, and runtime protocol evidence. The formalization treats concrete systems as partial implementations of abstract ones, then asks which states, traces, controllers, and migration paths preserve the intended checked behavior. This makes architecture questions concrete: which states are safe, which arrows can run, and which migrations preserve evidence across layers.
Read paper Download PDF