Piotr Polesiuk

Assistant professor in the Institute of Computer Science at the University of Wrocław
Member of the Group of Programming Languages

Research Interests

Non-Research Interests

Journal and Conference Papers

A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Paris, France, June 29–July 6 2020.
LIPIcs, Vol. 167, pp. 7:1–7:22. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[doi] [PDF]

Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers.
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
In 47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), New Orleans, Louisiana, United States, January 19–25, 2020.
Proceedings of the ACM on Programming Languages, Vol. 4 (POPL), pp. 48:1–48:29. ACM.
[doi] [PDF] [Coq] [Helium]

Bisimulations for Delimited-Control Operators.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
Logical Methods in Computer Science (LMCS), Vol. 15 (2:18), pp. 1–57, 2019.
[doi] [PDF]

Diacritical Companions.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Barbara König, editor, Proceedings of the Thirty-Fifth Conference on the Mathematical Foundations of Programming Semantics (MFPS 2019), London, UK, June 4–7, 2019.
Electronic Notes in Theoretical Computer Science, Vol. 347, pp. 25–43. Elsevier.
[doi] [PDF] [Coq]

Typed Equivalence of Effect Handlers and Delimited Control.
Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Dortmund, Germany, June 24–30, 2019.
LIPIcs, Vol. 131, pp. 30:1–30:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[doi] [PDF] [Coq]

A Complete Normal-Form Bisimilarity for State.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures – 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019.
Lecture Notes in Computer Science, Vol. 11425, pp. 98–114. Springer.
[doi] [PDF]

Equational Theories and Monads from Polynomial Cayley Representations.
Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
In Mikołaj Bojańczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures – 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019.
Lecture Notes in Computer Science, Vol. 11425, pp. 453–469. Springer.
[doi] [PDF]

Proving Soundness of Extensional Normal-Form Bisimilarities.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
Logical Methods in Computer Science (LMCS), Vol. 15 (1:31), pp. 1–24, 2019.
[doi] [PDF] [Coq]

Abstracting Algebraic Effects.
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
In 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Cascais, Portugal, January 13–19, 2019.
Proceedings of the ACM on Programming Languages, Vol. 3 (POPL), pp. 6:1–6:28. ACM.
[doi] [PDF] [Helium]

Logical Relations for Coherence of Effect Subtyping.
Dariusz Biernacki and Piotr Polesiuk.
Logical Methods in Computer Science (LMCS), Vol. 14 (1:11), pp. 1–28, 2018.
[doi] [PDF] [Coq]

Handle with Care: Relational Interpretation of Algebraic Effects and Handlers.
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
In 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), Los Angeles, CA, USA, January 10–12, 2018.
Proceedings of the ACM on Programming Languages, Vol. 2 (POPL), pp. 8:1–8:30. ACM.
[doi] [PDF] [Coq]

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation.
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
Logical Methods in Computer Science (LMCS), Vol. 13 (3:27), pp. 1–26, 2017.
[doi] [PDF] [Technical report]

Proving Soundness of Extensional Normal-Form Bisimilarities.
Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Alexandra Silva, editor, Proceedings of the Thirty-Third Conference on the Mathematical Foundations of Programming Semantics (MFPS 2017), Ljubljana, Slovenia, June 12–15, 2017.
Electronic Notes in Theoretical Computer Science, Vol. 336, pp. 41–56. Elsevier.
[doi] [PDF] [Coq]

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines.
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, and Alan Schmitt.
In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, June 20–23, 2017.
pp. 1–12. IEEE Computer Society.
[doi] [PDF] [Technical report]

Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation.
Andrés Aristizábal, Dariusz Biernacki, Sergueï Lenglet, and Piotr Polesiuk.
In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Porto, Portugal, June 22–26, 2016.
LIPIcs, Vol. 52, pp. 9:1–9:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[doi] [PDF] [Technical report]

Logical Relations for Coherence of Effect Subtyping.
Dariusz Biernacki and Piotr Polesiuk.
In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Warsaw, Poland, July 1-3, 2015.
LIPIcs, Vol. 38, pp. 107–122. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[doi] [PDF] [Coq]

Other Papers

Programming with Abstract Algebraic Effects. (extended abstract)
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
ML Family Workshop 2018, Saint Louis (MO), USA, September 2018.
[PDF]

Logical Relations for Algebraic Effects. (extended abstract)
Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski.
HOPE 2017, Oxford, UK, September 2017.
[PDF]

IxFree: Step-Indexed Logical Relations in Coq. (extended abstract)
Piotr Polesiuk.
The Third International Workshop on Coq for Programming Languages (CoqPL 2017), Paris, France, January 2017.
[PDF] [Coq]

Code

Language Implementation

Helium: Experimental Programming Language with Abstract Algebraic Effects
DBL: Experimental Programming Language with Lexical Effect Handlers and Implicit Parameters

Coq Libraries

IxFree: Reasoning about step-indexed logical relations

Coq Formalizations

Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Proving Soundness of Extensional Normal-Form Bisimilarities
Logical Relations for Coherence of Effect Subtyping

Students

Current MSc Students

Patrycja Balik
Relational models of effect capabilities.

Current BSc Students

Dawid Sroka
Implementing Unix-like kernel in Python.

Jakub Marcinkowski
Reconstruction of Plankalkül: the first high-level programming language.

Wiktor Bukowski
Implicit Instances of Algebraic Effects.

Mikołaj Fornal
Generating LR(1) parsers at compile-time using Scala 3 macros.

Former MSc Students

Dominik Gulczyński
Domain-specific logic for terms with variable binding, 2023.

Arkadiusz Kozdra
IoT devices fuzzing: discovering bugs in communications protocol implementation, 2023.

Former BSc Students

Szymon Kiczak
Functional programming with algebraic effects, 2024.

Aleksander Pogoda
Deamortization of persistent data structures via defunctionalization, 2024.

Antoni Nowak
Emulation of Z80 processor, 2023.

Aleksandra Kosińska and Cezary Stajszczyk
Raspberry Pi BASIC, 2023.

Adam Szeruda
Generating Well-Typed Parsers in Continuation-Passing Style, 2023.

Patrycja Balik
Algebraic Effect Instance Scopes, 2022.

Teaching

I'm mostly engaged in teaching low-level stuff (Computer Architectures and Operating Systems) and Programming Methods (Metody Programowania): a first-year course on abstraction building and functional programming.

Selected Courses