5 papers
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…
From the NYU Ultracomputer to Modern Exascale: A Historical and Architectural Survey of In-Network Computing and Scalable Synchronization
Lars Warren Ericson
This paper presents a historical and technical survey of the hardware architectures, interconnection networks, and synchronization primitives that have shaped massively parallel sy…
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…