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...
Autori principali: | Kammar, O, Katsumata, S-Y, Saville, P |
---|---|
Natura: | Conference item |
Lingua: | English |
Pubblicazione: |
Association for Computing Machinery
2022
|
Documenti analoghi
Documenti analoghi
-
Implicit automata in typed λ-calculi I: Aperiodicity in a non-commutative logic
di: Nguyễn, LTD, et al.
Pubblicazione: (2020) -
Heuristic principles and logical calculi /
di: 323486 Serebryannikov, Oleg Fedorovich
Pubblicazione: (1972) -
On Graphical Calculi for Modal Logics
di: Paulo A. S. Veloso, et al.
Pubblicazione: (2016-12-01) -
Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
di: Luís Pinto, et al.
Pubblicazione: (2011-01-01) -
Relation between classical and intuitionistic sequent calculi of temporal logic
di: Romas Alonderis
Pubblicazione: (2001-12-01)