Fully abstract models for effectful λ-calculi via category-theoretic logical relations
Abstract
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.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 12, 2022
- Source ID
- 10.1145/3498705
Entities
People
- Ohad Kammar
- Philip Saville
- Shin-ya Katsumata
Organizations
- Air Force Office of Scientific Research
- National Institute of Informatics
- University of Edinburgh
- University of Oxford