arXiv subjects

Lars Warren Ericson

Publications and source records attributed to Lars Warren Ericson.

5 recordsLinked to original sources

arXiv2026

A Lean 4 Formalization of Scott's Continuous Lattices (1972)

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 including the March 1972 Milner correction in \textbf{[Sco72]} (pp.~135--136). Scott's paper develops a model for $\lambda$-calculus from a topological starting point. He defines \emph{injective} $T_0$-spaces -- those with a strong extension property for continuous maps -- and shows that they are exactly the \emph{continuous lattices}: complete lattices whose Scott topology is determined by the order via the way-below relation ($\ll$). On this foundation he studies projections, retractions, products, function spaces, and inverse limits. The capstone (Theorem 4.4) constructs an inverse limit $D_\infty$ of function-space approximants and proves $D_\infty \cong [D_\infty \to D_\infty]$, yielding a purely mathematical model for Church's untyped $\lambda$-calculus. Our development formalizes \textbf{43 numbered results} from Scott's Sections 1--4 (Propositions, Corollaries, Lemmas, and Theorems), each as a sorry-free Lean theorem, together with supporting infrastructure (step functions, the $\Uparrow a$ basis of Scott opens, Milner's coarser-than-Scott hypothesis, the function-space tower, and the $i_\infty$/$j_\infty$ pair). The formalization is \textbf{classical} (uses \texttt{Classical.choice} transitively) and follows Scott's proof dependency order. Where the Lean proof required choices not visible in the original -- or where dead ends were encountered -- we record detailed notes in Section 5. All proofs check with the standard footprint $\texttt{[propext, Classical.choice, Quot.sound]}$. The formalization has been accepted into the Palomar registry.

cs.LO↗

arXiv2026

Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$

We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic $L(\forall)$: propositional modal logic with nominals, the satisfaction-style binder $\forall$, and the box modality. (Machine-checked completeness for basic hybrid logic, without binders, was pioneered by Asta Halkj\ae r From in Isabelle/HOL.) We build on Alex Oltean's 2023 Lean 4 formalization, which mechanized the syntax, semantics, Hilbert-style proof system, and soundness following Blackburn's Hybrid Completeness (1998), but left completeness unfinished. Finishing it requires manufacturing fresh names at two structurally different points, and our central finding is that they call for two different tools. (1) The root witnessed maximal consistent set, built by an extended Lindenbaum construction, needs at each step a nominal fresh for the whole set; the right tool is structural freshness: extend the language so an infinite supply of nominals is reserved by construction. We survey the design space (Oltean's odd/even encoding inside $\mathbb{N}$, the disjoint-sum $N \oplus \mathbb{N}$ parameterization suggested by Bud Mishra, and From's synthetic-completeness frameworks) and explain the encoding we adopt. (2) The witnessed $\Diamond$-successor of a maximal consistent set cannot be obtained this way: its canonical box-reduct provably mentions every nominal, so no reserved name is fresh. Here the right tool is one Oltean chose but left incomplete: an existence-lemma Henkin construction drawing each witness from the predecessor's witnessedness through a fresh state variable; we complete it with a data-carrying witness accumulator and a compactness argument. The theorem $\Gamma \models \varphi \to \Gamma \vdash \varphi$ is fully formalized: the development is sorry-free, and #print axioms reports only propext, Classical.choice, and Quot.sound. We port the development to Lean v4.30.0 / mathlib v4.30.0.

cs.LO↗

arXiv2026

Revisiting average case complexity of multilevel syllogistic

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 Reischuk--Schindelhauer average-case classes, an axiomatic MLS/EMLS semantics layer, a partial Ferro--Omodeo--Schwartz decision procedure with proved soundness and partial completeness on a membership-free fragment, serialization and step budgets, and conditional NP-average completeness and non-AvP hardness corollaries modulo explicitly documented structural axioms. Full Lean sources are inlined in the appendix modules.

cs.LO↗

arXiv2026

From the NYU Ultracomputer to Modern Exascale: A Historical and Architectural Survey of In-Network Computing and Scalable Synchronization

This paper presents a historical and technical survey of the hardware architectures, interconnection networks, and synchronization primitives that have shaped massively parallel systems over the past four decades. We examine the design of the NYU Ultracomputer and the IBM Research Parallel Processor Prototype (RP3), focusing on the hardware implementation of the Fetch-and-Add primitive in multistage interconnection networks. We contrast these early attempts at fine-grained, shared-memory hardware combining with the distributed-memory architectures of the IBM SP series and the modern in-network computation models found in NVIDIA SHARP and HPE Slingshot. We provide a technical analysis of message-passing synchronization, presenting a complete profiling of MPI operation frequencies and detailing the low-level hardware mapping of one-sided RMA atomics to PCIe Atomics and GPU caches. We investigate the software-hardware boundary in modern deep learning, detailing how HIP translation, Triton compilation, and 4-bit quantization (W4A16) execute on modern heterogeneous silicon. To evaluate alternative network node designs, we present a historical hardware case study analyzing the feasibility of implementing active combining switches using message-passing Inmos Transputers programmed in Occam. Finally, we contextualize the evolution of concurrent software synchronization by examining Isaac Dimitrovsky's parallel "group lock" primitive, tracing its downstream echoes in group mutual exclusion (GME) and room synchronization, and reflect on the historical, philosophical divide between American systems engineering and European formal methods.

cs.DC↗

arXiv2026

A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package

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 Domains} (Ericson, 1986). The original system implemented Lipson's catalog of procedures over integers, rationals, modular rings, polynomial rings, and truncated power series via a custom runtime dispatch mechanism in Icon. The present work separates three concerns: mathematical definitions grounded in Mathlib's \texttt{EuclideanDomain} hierarchy, computable mirrors suitable for evaluation and regression testing, and report-formatting infrastructure that reproduces the 1986 benchmark output line-for-line. All fourteen application algorithms from Section 3 of the report are defined and typecheck without \texttt{sorry}; those grounded in Mathlib -- chiefly integer gcd and extended Euclid -- additionally carry machine-checked proofs. We classify each procedure by its epistemic status relative to Mathlib, enumerate the coherence obligations between the proof and computable layers, and state precisely what is theorem-backed versus regression-trusted. The formalization makes explicit the verification boundary that the 1986 package crossed only informally.

cs.LO↗