4 papers · 1 filter
A Lean 4 Formalization of Scott's \emph{Continuous Lattices} (1972)
Lars Warren Ericson
We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \emph{Continuous Lattices} \textbf{[Sco72]}, carried out in Lean 4 against mathlib and inclu…
Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic
Lars Warren Ericson
We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic : propositional modal logic with nominals, the satisfaction-style binder , a…
Revisiting average case complexity of multilevel syllogistic: From the 1995 Courant Technical Report to Lean 4 Formalization
Lars Warren Ericson
We describe a Lean~4 formalization revisiting NYU Courant Technical Report TR1995-711 on the average-case complexity of Multilevel Syllogistic (MLS). The development encodes Reisch…
A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package
Lars Warren Ericson
We describe a Lean 4 formalization of the algorithms and domain types from NYU Computer Science Technical Report \#232, \emph{An ICON Package for Experimenting with Euclidean Domai…