Automating Derivations of Abstract Machines from Reduction Semantics: - A Generic Formalization of Refocusing in Coq. - Filip Sieczkowski; Malgorzata Biernacka; Dariusz Biernacki (IFL, 2010)

Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. - Jesper Bengtson; Jonas Braband Jensen; Filip Sieczkowski; Lars Birkedal (ITP, 2011)

A Concurrent Logical Relation. - Lars Birkedal; Filip Sieczkowski; Jacob Thamsborg (CSL, 2012)

Formalized Verification of Snapshotable Trees: Separation and Sharing. - Hannes Mehnert; Filip Sieczkowski; Lars Birkedal; Peter Sestoft (VSTTE, 2012)

A Separation Logic for Fictional Sequential Consistency. - Filip Sieczkowski; Kasper Svendsen; Lars Birkedal; Jean Pichon-Pharabod (ESOP, 2015)

ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. - Filip Sieczkowski; Ales Bizjak; Lars Birkedal (ITP, 2015)

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. - Ralf Jung 002; David Swasey; Filip Sieczkowski; Kasper Svendsen; Aaron Turon; Lars Birkedal; Derek Dreyer (POPL, 2015)

Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. - Kasper Svendsen; Filip Sieczkowski; Lars Birkedal (ESOP, 2016)

Dag-calculus: a calculus for parallel computation. - Umut A. Acar; Arthur Charguéraud; Mike Rainey; Filip Sieczkowski (ICFP, 2016)

A Kripke logical relation for effect-based program transformations. - Lars Birkedal; Guilhem Jaber; Filip Sieczkowski; Jacob Thamsborg (Inf. Comput., 2016)

Heartbeat scheduling: provable efficiency for nested parallelism. - Umut A. Acar; Arthur Charguéraud; Adrien Guatto; Mike Rainey; Filip Sieczkowski (PLDI, 2018)

Handle with care: relational interpretation of algebraic effects and handlers. - Dariusz Biernacki; Maciej Piróg; Piotr Polesiuk; Filip Sieczkowski (Proc. ACM Program. Lang., 2018)

Equational Theories and Monads from Polynomial Cayley Representations. - Maciej Piróg; Piotr Polesiuk; Filip Sieczkowski (FoSSaCS, 2019)

Typed Equivalence of Effect Handlers and Delimited Control. - Maciej Piróg; Piotr Polesiuk; Filip Sieczkowski (FSCD, 2019)

Abstracting algebraic effects. - Dariusz Biernacki; Maciej Piróg; Piotr Polesiuk; Filip Sieczkowski (Proc. ACM Program. Lang., 2019)

A Reflection on Continuation-Composing Style. - Dariusz Biernacki; Mateusz Pyzik; Filip Sieczkowski (FSCD, 2020)

Binders by day, labels by night: effect instances via lexically scoped handlers. - Dariusz Biernacki; Maciej Piróg; Piotr Polesiuk; Filip Sieczkowski (Proc. ACM Program. Lang., 2020)

Reflecting Stacked Continuations in a Fine-Grained Direct-Style Reduction Theory. - Dariusz Biernacki; Mateusz Pyzik; Filip Sieczkowski (PPDP, 2021)

A General Fine-Grained Reduction Theory for Effect Handlers. - Filip Sieczkowski; Mateusz Pyzik; Dariusz Biernacki (Proc. ACM Program. Lang., 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Zenodo, 2023)

The Essence of Generalized Algebraic Data Types. - Filip Sieczkowski; Sergei Stepanenko; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2024)