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

Fully Abstract Encodings of λ-Calculus in HOcore through Abstract Machines.
Małgorzata Biernacka, Dariusz Biernacki, Sergueï Lenglet, Piotr Polesiuk, Damien Pous, and Alan Schmitt.
Logical Methods in Computer Science (LMCS), Vol. 20 (3:3), pp. 1–45, 2024.
[doi] [PDF]

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

Logical Relations for Effect Capabilities. (extended abstract)
Patrycja Balik and Piotr Polesiuk.
HOPE 2024, Milan, Italy, September 2024.
[PDF]

Fram: Named Parameters Pushed to the Limit. (extended abstract)
Patrycja Balik and Piotr Polesiuk.
ML Family Workshop 2024, Milan, Italy, September 2024.
[PDF]

Functorial Syntax for All. (extended abstract)
Piotr Polesiuk and Filip Sieczkowski.
The Tenth International Workshop on Coq for Programming Languages (CoqPL 2024), London, UK, January, 2024.
[PDF]

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

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

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 PhD Students

Patrycja Balik
Working on language design and formal models for algebraic effects.

Bartłomiej Królikowski
Working on mariage of algebraic effects and dependent types.

Current MSc Students

Szymon Jędras
Working on formalization and implementation of Fram programming language. Exact topic will be determined..

Wojciech Pokój
Implementation of pretty-printer in Fram.

Adam Szeruda
Incremental lambda-calculus in practice.

Current BSc Students

Former MSc Students

Patrycja Balik
Relational models for a language with effect capabilities, 2024.

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

Jakub Marcinkowski
Plankalkül: the first attempt to describe a high-level programming language, 2024.

Dawid Sroka
Kernel in Python: a high-level implementation of the basic functionality of an operation system, 2024.

Mikołaj Fornal
Compile-time generation of LR(1) parsers using Scala 3 macros, 2024.

Szymon Jędras
Static analysis for folding multi-argument functions, 2024.

Wiktor Bukowski
Implementation of bidirectional type-and-effect reconstruction in presence of rank-N polymorphism, 2024.

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