Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning R Jung, D Swasey, F Sieczkowski, K Svendsen, A Turon, L Birkedal, ... ACM SIGPLAN Notices 50 (1), 637-650, 2015 | 372 | 2015 |

Handle with care: relational interpretation of algebraic effects and handlers D Biernacki, M Piróg, P Polesiuk, F Sieczkowski Proceedings of the ACM on Programming Languages 2 (POPL), 1-30, 2017 | 56 | 2017 |

Abstracting Algebraic Effects D Biernacki, M Piróg, P Polesiuk, F Sieczkowski POPL 2019, 2019 | 52 | 2019 |

Binders by day, labels by night: effect instances via lexically scoped handlers D Biernacki, M Piróg, P Polesiuk, F Sieczkowski Proceedings of the ACM on Programming Languages 4 (POPL), 1-29, 2019 | 48 | 2019 |

Verifying object-oriented programs with higher-order separation logic in Coq J Bengtson, JB Jensen, F Sieczkowski, L Birkedal Interactive Theorem Proving: Second International Conference, ITP 2011, Berg …, 2011 | 36 | 2011 |

Typed equivalence of effect handlers and delimited control M Piróg, P Polesiuk, F Sieczkowski 4th International Conference on Formal Structures for Computation and …, 2019 | 34 | 2019 |

A concurrent logical relation L Birkedal, F Sieczkowski, JJ Thamsborg Dagstuhl Seminar Proceedings 16, 2012 | 30 | 2012 |

Automating derivations of abstract machines from reduction semantics: A generic formalization of refocusing in Coq F Sieczkowski, M Biernacka, D Biernacki Implementation and Application of Functional Languages: 22nd International …, 2011 | 25 | 2011 |

Heartbeat scheduling: provable efficiency for nested parallelism UA Acar, A Charguéraud, A Guatto, M Rainey, F Sieczkowski Proceedings of the 39th ACM SIGPLAN Conference on Programming Language …, 2018 | 24 | 2018 |

A separation logic for fictional sequential consistency F Sieczkowski, K Svendsen, L Birkedal, J Pichon-Pharabod ESOP 2015, 2015 | 24 | 2015 |

Formalized verification of snapshotable trees: Separation and sharing H Mehnert, F Sieczkowski, L Birkedal, P Sestoft Verified Software: Theories, Tools, Experiments: 4th International …, 2012 | 21 | 2012 |

Transfinite Step-indexing: Decoupling Concrete and Logical Steps K Svendsen, F Sieczkowski, L Birkedal ESOP 2016, 2016 | 18 | 2016 |

ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages F Sieczkowski, A Bizjak, L Birkedal Interactive Theorem Proving, 2015 | 16 | 2015 |

Dag-calculus: a calculus for parallel computation UA Acar, A Charguéraud, M Rainey, F Sieczkowski Proceedings of the 21st ACM SIGPLAN International Conference on Functional …, 2016 | 13 | 2016 |

Reflecting Stacked Continuations in a Fine-Grained Direct-Style Reduction Theory D Biernacki, M Pyzik, F Sieczkowski 23rd International Symposium on Principles and Practice of Declarative …, 2021 | 7 | 2021 |

A Reflection on Continuation-Composing Style D Biernacki, M Pyzik, F Sieczkowski 5th International Conference on Formal Structures for Computation and …, 2020 | 6 | 2020 |

A Kripke logical relation for effect-based program transformations L Birkedal, G Jaber, F Sieczkowski, J Thamsborg Information and Computation 249, 160-189, 2016 | 6 | 2016 |

Equational Theories and Monads from Polynomial Cayley Representations M Piróg, P Polesiuk, F Sieczkowski International Conference on Foundations of Software Science and Computation …, 2019 | 2 | 2019 |

Towards Modular Reasoning for Realistic Programming Languages F Sieczkowski PhD thesis, IT University of Copenhagen, 2013 | 1 | 2013 |

A General Fine-Grained Reduction Theory for Effect Handlers F Sieczkowski, M Pyzik, D Biernacki Proceedings of the ACM on Programming Languages 7 (ICFP), 511-540, 2023 | | 2023 |