Fully abstract models for effectful λ-calculi via category-theoretic logical relations
We present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lift...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Association for Computing Machinery
2022
|
| _version_ | 1797092242113953792 |
|---|---|
| author | Kammar, O Katsumata, S-Y Saville, P |
| author_facet | Kammar, O Katsumata, S-Y Saville, P |
| author_sort | Kammar, O |
| collection | OXFORD |
| description | We present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lifting, and ⊤⊤-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming. |
| first_indexed | 2024-03-07T03:43:20Z |
| format | Conference item |
| id | oxford-uuid:be9ee57c-cc97-4b7d-9ae6-6612cb47d75a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T03:43:20Z |
| publishDate | 2022 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:be9ee57c-cc97-4b7d-9ae6-6612cb47d75a2022-03-27T05:41:07ZFully abstract models for effectful λ-calculi via category-theoretic logical relationsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:be9ee57c-cc97-4b7d-9ae6-6612cb47d75aEnglishSymplectic ElementsAssociation for Computing Machinery2022Kammar, OKatsumata, S-YSaville, PWe present a construction which, under suitable assumptions, takes a model of Moggi’s computational λ-calculus with sum types, effect operations and primitives, and yields a model that is adequate and fully abstract. The construction, which uses the theory of fibrations, categorical glueing, ⊤⊤-lifting, and ⊤⊤-closure, takes inspiration from O’Hearn & Riecke’s fully abstract model for PCF. Our construction can be applied in the category of sets and functions, as well as the category of diffeological spaces and smooth maps and the category of quasi-Borel spaces, which have been studied as semantics for differentiable and probabilistic programming. |
| spellingShingle | Kammar, O Katsumata, S-Y Saville, P Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title | Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title_full | Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title_fullStr | Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title_full_unstemmed | Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title_short | Fully abstract models for effectful λ-calculi via category-theoretic logical relations |
| title_sort | fully abstract models for effectful λ calculi via category theoretic logical relations |
| work_keys_str_mv | AT kammaro fullyabstractmodelsforeffectfullcalculiviacategorytheoreticlogicalrelations AT katsumatasy fullyabstractmodelsforeffectfullcalculiviacategorytheoreticlogicalrelations AT savillep fullyabstractmodelsforeffectfullcalculiviacategorytheoreticlogicalrelations |