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...
| Հիմնական հեղինակներ: | , , |
|---|---|
| Ձևաչափ: | Conference item |
| Լեզու: | English |
| Հրապարակվել է: |
Association for Computing Machinery
2022
|