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...

Descrizione completa

Dettagli Bibliografici
Autori principali: Kammar, O, Katsumata, S-Y, Saville, P
Natura: Conference item
Lingua:English
Pubblicazione: Association for Computing Machinery 2022

Documenti analoghi