6 papers
On the Number of Distinct Topological Bases of a Finite Set of Size
Lars Warren Ericson
For a finite set with , the number of families that are topological bases is $\#(N) = \sum_{\mathcal{T} \in \operator…
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…
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…
A Lean 4 Formalization of Scott's 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…
Revisiting average case complexity of multilevel syllogistic
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…