{"id":"palomar/PALOMAR-2026-09-28-000003","url":"https://github.com/catskillsresearch/scott2026/tree/4b57681f2804e6390c73bae4149f54a92029c50d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-28-000003-v1.json","repo":"https://github.com/catskillsresearch/scott2026","tags":["cs.LO","cs.PL","math.LO","msc:68Q55","msc:06D99","msc:03B70","msc:68V20","lean","lambda-calculus","domain-theory"],"score":0,"title":"Lean Formalization of Interpreting Lambda Calculus in Domain-Valued Random Variables (CSL 2026)","trust":"high","domain":"cs.LO","source":"palomar","authors":["Lars Warren Ericson"],"reviews":0,"subject":"cs.LO","summary":"Formalization in Lean 4 / mathlib of the existing paper by Furber, Mardare, Panangaden, and Scott, Interpreting Lambda Calculus in Domain-Valued Random Variables (LIPIcs, Vol. 363, CSL 2026, Article 48). This repository formalizes that published mathematics; it does not present the paper's results as new mathematics originating in this repository. Three capstones sit on top of the rest of the paper: Theorem 26 (internal λ-interpretation in SetoidF_A), Corollary 34 (the Engeler model with numerals in V^A), and Theorem 43 (two fair-coin subsets of ℕ that are incomparable under the λ-definable…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-09-28","reactions":{},"formalized":true,"formalizes":[{"title":"Interpreting Lambda Calculus in Domain-Valued Random Variables","identifier":"","relationship":"formalizes"}]}