Trustworthy Formal Natural Language Specifications
summary
A prototype embeds an extensible fragment of English inside the Lean proof assistant, using categorial grammars encoded as type class instances to parse sentences into formal meanings and to emit proof certificates as persistent evidence. The system translates many textbook specifications (Verified Functional Algorithms) into Lean, producing alpha‑equivalent formalizations with a modest lexicon; parsing runs from about 1 to 7 seconds. One specification fails because it refers to syntactic rearrangement (nested union) rather than a semantic claim. Artifacts are available.
AI-written summary · about
chapters (12)
- 0:00Trustworthy formal NL specs
- 1:48Specification gap in formal verification
- 3:35Goals and non-goals
- 5:21Why this work differs
- 7:06Categorial grammars for parsing
- 13:26Trustworthy evidence during parsing
- 16:58Prototype in Lean
- 18:22Evaluating specs vs textbooks
- 20:30Linguistic insights
- 22:39Extensibility and future
- 23:43Tool demo
- 25:08Questions and answers session
related talks
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
47mIs There a Future for a Formally Specified Haskell Report
01h 04mLean4Lean: Mechanizing the Metatheory of Lean
29mExplicit Refinement Types
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
01h 05mAll the Languages Together
46mRefinement Types from Light to Deep Verification
01h 01mMulti-Modal Verification of Distributed Systems in Lean