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