2026-07-23T03:49:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24631 2025-12-12T15:10:06Z ddc:004 open_access

Scott’s Representation Theorem and the Univalent Karoubi Envelope van der Leer, Arnoud Wullaert, Kobe Ahrens, Benedikt Lambda calculi algebraic theories categorical semantics Karoubi envelope formalization Rocq-UniMath univalent foundations Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category. We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arnoud van der Leer and Kobe Wullaert and Benedikt Ahrens 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.33 urn:nbn:de:0030-drops-246318 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.33 eng https://creativecommons.org/licenses/by/4.0/legalcode