A denotationally-based program logic for higher-order store

DOI10.46298/ENTICS.12232MaRDI QIDQ6831479zbMATH OpenFDO

Authors Frederik Lerbjerg Aagaard, Jonathan Sterling, Lars Birkedal

Publication date 2 April 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/ENTICS.12232

zbMATH Keywords

BI-hyperdoctrinedenotational semanticsgeneral referencesguarded recursionhigher-order separation logichigher-order storeimpredicative polymorphismrecursive typessynthetic guarded domain theory

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites work

• A model of PCF in guarded type theory
• A relational modal logic for higher-order stateful ADTs
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on
• Categorical logic and type theory
• Completeness for algebraic theories of local state
• Denotational semantics for guarded dependent type theory
• Edinburgh LCF. A mechanized logic of computation
• Guarded dependent type theory with coinductive types
• scientific article; zbMATH DE number 3825806 (Why is no real title available?)
• scientific article; zbMATH DE number 3949678 (Why is no real title available?)
• scientific article; zbMATH DE number 3550923 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• scientific article; zbMATH DE number 1948165 (Why is no real title available?)
• scientific article; zbMATH DE number 1531624 (Why is no real title available?)
• scientific article; zbMATH DE number 2087441 (Why is no real title available?)
• Impredicative encodings of (higher) inductive types
• Intensional type theory with guarded recursive types qua fixed points on universes
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• LCF considered as a programming language
• Local local reasoning: a BI-hyperdoctrine for full ground store
• Logic and Computation
• Natural models of homotopy type theory
• Notions of computation and monads
• On models of higher-order separation logic
• Practical foundations for programming languages
• Propositions as [Types]
• Realisability semantics of parametric polymorphism, general references and recursive types
• Sheaves in geometry and logic: a first introduction to topos theory
• Verified software toolchain (invited talk)

This page was built for publication: A denotationally-based program logic for higher-order store

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6831479)