2026-07-21T21:09:27Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19690 2024-03-06T11:04:40Z ddc:004 open_access

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics Sterling, Jonathan Gratzer, Daniel Birkedal, Lars univalent foundations homotopy type theory impredicative encodings synthetic guarded domain theory guarded recursion higher-order store reference types We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap - a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jonathan Sterling and Daniel Gratzer and Lars Birkedal 2024 Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2024.47 urn:nbn:de:0030-drops-196901 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47 eng https://creativecommons.org/licenses/by/4.0/legalcode