Logical relations for coherence of effect subtyping
A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2018-01-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/4180/pdf |
| _version_ | 1827322770486198272 |
|---|---|
| author | Dariusz Biernacki Piotr Polesiuk |
| author_facet | Dariusz Biernacki Piotr Polesiuk |
| author_sort | Dariusz Biernacki |
| collection | DOAJ |
| description | A coercion semantics of a programming language with subtyping is typically
defined on typing derivations rather than on typing judgments. To avoid
semantic ambiguity, such a semantics is expected to be coherent, i.e.,
independent of the typing derivation for a given typing judgment. In this
article we present heterogeneous, biorthogonal, step-indexed logical relations
for establishing the coherence of coercion semantics of programming languages
with subtyping. To illustrate the effectiveness of the proof method, we develop
a proof of coherence of a type-directed, selective CPS translation from a typed
call-by-value lambda calculus with delimited continuations and control-effect
subtyping. The article is accompanied by a Coq formalization that relies on a
novel shallow embedding of a logic for reasoning about step-indexing. |
| first_indexed | 2024-04-25T01:35:11Z |
| format | Article |
| id | doaj.art-1828603354e740f485fc878eccbf0c65 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:11Z |
| publishDate | 2018-01-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-1828603354e740f485fc878eccbf0c652024-03-08T09:53:24ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742018-01-01Volume 14, Issue 110.23638/LMCS-14(1:11)20184180Logical relations for coherence of effect subtypingDariusz BiernackiPiotr PolesiukA coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.https://lmcs.episciences.org/4180/pdfcomputer science - programming languages |
| spellingShingle | Dariusz Biernacki Piotr Polesiuk Logical relations for coherence of effect subtyping Logical Methods in Computer Science computer science - programming languages |
| title | Logical relations for coherence of effect subtyping |
| title_full | Logical relations for coherence of effect subtyping |
| title_fullStr | Logical relations for coherence of effect subtyping |
| title_full_unstemmed | Logical relations for coherence of effect subtyping |
| title_short | Logical relations for coherence of effect subtyping |
| title_sort | logical relations for coherence of effect subtyping |
| topic | computer science - programming languages |
| url | https://lmcs.episciences.org/4180/pdf |
| work_keys_str_mv | AT dariuszbiernacki logicalrelationsforcoherenceofeffectsubtyping AT piotrpolesiuk logicalrelationsforcoherenceofeffectsubtyping |