{"id":"palomar/PALOMAR-2026-08-24-000005","url":"https://github.com/catskillsresearch/scott1982/tree/d3221eec09505aa75e1b818aabc73f1f04339bdc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-24-000005-v1.json","repo":"https://github.com/catskillsresearch/scott1982","tags":["cs.LO","math.LO","msc:68Q55","msc:06B35","msc:03B70","domain-theory","denotational-semantics","lean-formalization"],"score":0,"title":"catskillsresearch/scott1982","trust":"high","domain":"cs.LO","source":"palomar","authors":["Lars Warren Ericson"],"reviews":0,"subject":"cs.LO","summary":"A Lean 4 / mathlib formalization of Dana Scott's 1982 ICALP paper *Domains for Denotational Semantics*. The Palomar compared result is only the first sentence of Theorem 7.2: if A and B are information systems, then so is A → B, and the approximable mappings f : A → B are exactly the elements f ∈ |A → B|. Challenge.lean imports Mathlib only and locks Definition 2.1, Definition 2.2, Definition 5.1, and Definition 7.1 (tokens, consistency, and the constructive-witness form of entailment). The remaining apply / curry clauses of the same numbered theorem live in Scott1982/Theorem72.lean and are…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-08-24","reactions":{},"formalized":true,"formalizes":[{"title":"Domains for Denotational Semantics","identifier":"","relationship":"formalizes"}]}