Fully abstract models for effectful λ-calculi via category-theoretic logical relations

Ohad Kammar, Shin Ya Katsumata, Philip Saville

Research output: Contribution to journalArticlepeer-review

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, ĝCurrency signĝCurrency sign-lifting, and ĝCurrency signĝCurrency sign-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.

Original languageEnglish
Article number44
Number of pages28
JournalProceedings of the ACM on Programming Languages
Volume6
Issue numberPOPL
DOIs
Publication statusPublished - 11 Jan 2022

Keywords

  • call-by-value
  • fibration
  • full abstraction
  • monad
  • O'Hearn & Riecke

Fingerprint

Dive into the research topics of 'Fully abstract models for effectful λ-calculi via category-theoretic logical relations'. Together they form a unique fingerprint.

Cite this