Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
summary
Construction takes a model of Moggi’s computational λ-calculus with sums, effect operations and primitives and produces an adequate, fully abstract refinement of that model by cutting nondefinable maps. The method uses fibrations, categorical glueing and TT-lifting plus TT-closure to form concrete logical relations (predicates) indexed by a chosen set I that names base elements, ensuring every morphism preserves all relations. Works over Set, diffeological and quasi-Borel spaces and yields a concrete fully abstract model.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:12Standard bits
- 3:08Full abstraction
- 5:05Semantic interpretation
- 9:57General Construction
- 14:15Sufficient Conditions
- 15:30Strategy
- 18:00Summary
related talks
45mA categorical view of computational effects
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
51mA Gentle Introduction to Modern Model Theory
22mAlgebraic Effects Meet Hoare Logic in Cubical Agda
24mClassical Notions of Computation and the Hasegawa-Thielecke Theorem
56mCalculating Intuitionistic Logic in Scala
23mImplementing a category-theoretic framework for typed abstract syntax
14mAdequacy for Algebraic Effects Revisited