Search Results

Documents authored by Polesiuk, Piotr

Document
DOI: 10.4230/LIPIcs.FSCD.2020.7
A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers

Authors: Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
We present a complete coinductive syntactic theory for an untyped calculus of algebraic operations and handlers, a relatively recent concept that augments a programming language with unprecedented flexibility to define, combine and interpret computational effects. Our theory takes the form of a normal-form bisimilarity and its soundness w.r.t. contextual equivalence hinges on using so-called context variables to test evaluation contexts comprising normal forms other than values. The theory is formulated in purely syntactic elementary terms and its completeness demonstrates the discriminating power of handlers. It crucially takes advantage of the clean separation of effect handling code from effect raising construct, a distinctive feature of algebraic effects, not present in other closely related control structures such as delimited-control operators.
Cite as

Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 7:1-7:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{biernacki_et_al:LIPIcs.FSCD.2020.7,
  author =	{Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr},
  title =	{{A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{7:1--7:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.7},
  URN =		{urn:nbn:de:0030-drops-123295},
  doi =		{10.4230/LIPIcs.FSCD.2020.7},
  annote =	{Keywords: algebraic effect, handler, behavioral equivalence, bisimilarity}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.30
Typed Equivalence of Effect Handlers and Delimited Control

Authors: Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
It is folklore that effect handlers and delimited control operators are closely related: recently, this relationship has been proved in an untyped setting for deep handlers and the shift_0 delimited control operator. We positively resolve the conjecture that in an appropriately polymorphic type system this relationship can be extended to the level of types, by identifying the necessary forms of polymorphism, thus extending the definability result to the typed context. In the process, we identify a novel and potentially interesting type system feature for delimited control operators. Moreover, we extend these results to substantiate the folklore connection between shallow handlers and control_0 flavour of delimited control, both in an untyped and typed settings.
Cite as

Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. Typed Equivalence of Effect Handlers and Delimited Control. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{pirog_et_al:LIPIcs.FSCD.2019.30,
  author =	{Pir\'{o}g, Maciej and Polesiuk, Piotr and Sieczkowski, Filip},
  title =	{{Typed Equivalence of Effect Handlers and Delimited Control}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.30},
  URN =		{urn:nbn:de:0030-drops-105376},
  doi =		{10.4230/LIPIcs.FSCD.2019.30},
  annote =	{Keywords: type-and-effect systems, algebraic effects, delimited control, macro expressibility}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.9
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation

Authors: Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing techniques for establishing program equivalence in calculi with single-prompted delimited control. The basic theory that we develop is presented using Madiot et al.'s framework that allows for smooth integration and composition of up-to techniques facilitating bisimulation proofs. We also generalize the framework in order to express environmental bisimulations that support equivalence proofs of evaluation contexts representing continuations. This change leads to a novel and powerful up-to technique enhancing bisimulation proofs in the presence of control operators.
Cite as

Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk. Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{aristizabal_et_al:LIPIcs.FSCD.2016.9,
  author =	{Aristiz\'{a}bal, Andr\'{e}s and Biernacki, Dariusz and Lenglet, Sergue\"{i} and Polesiuk, Piotr},
  title =	{{Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.9},
  URN =		{urn:nbn:de:0030-drops-59756},
  doi =		{10.4230/LIPIcs.FSCD.2016.9},
  annote =	{Keywords: delimited continuation, dynamic prompt generation, contextual equivalence, environmental bisimulation, up-to technique}
}
Document
DOI: 10.4230/LIPIcs.TLCA.2015.107
Logical Relations for Coherence of Effect Subtyping

Authors: Dariusz Biernacki and Piotr Polesiuk

Published in: LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Abstract
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.
Cite as

Dariusz Biernacki and Piotr Polesiuk. Logical Relations for Coherence of Effect Subtyping. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 107-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{biernacki_et_al:LIPIcs.TLCA.2015.107,
  author =	{Biernacki, Dariusz and Polesiuk, Piotr},
  title =	{{Logical Relations for Coherence of Effect Subtyping}},
  booktitle =	{13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)},
  pages =	{107--122},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-87-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{38},
  editor =	{Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.107},
  URN =		{urn:nbn:de:0030-drops-51580},
  doi =		{10.4230/LIPIcs.TLCA.2015.107},
  annote =	{Keywords: type system, coherence of subtyping, logical relation, control effect, continuation-passing style}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact