I'm a postdoc at Aarhus University, working with Lars Birkedal in the Logic and Semantics group. We are currently working on building a Coq formalisation of some of the recent techniques for building models of higher-order programming language, in particular the use of complete ultrametric spaces to solve recursive domain equations (a good suggestion for a name would certainly be appreciated). We are also writing a tutorial, with the idea of helping others start their own experiments with these techniques. Some details on this are available below.

Previously, I've worked with Lars and Peter Sestoft at the IT University of Copenhagen for my PhD. My main area of research during the PhD was software verification and separation logic; I've also done some work on Kripke logical relations while there. My old webpage is still there. Prior to that, I've studied at the Institute of Computer Science of the University of Wrocław. My Masters' thesis there was supervised by Dariusz Biernacki.


A Separation Logic for Fictional Sequential Consistency. Filip Sieczkowski, Kasper Svendsen, Lars Birkedal and Jean Pichon. Accepted for publication at ESOP 2015. [PDF]
We present a proof system for a high-level programming language with a relaxed memory model that supports both low-level reasoning about racy code and high-level reasoning about well-behaved code.
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal and Derek Dreyer. Accepted for publication at POPL 2015. [Iris homepage]
We present Iris, a concurrent separation logic with a simple premise: monoids and invariants are all you need. Partial commutative monoids enable us to express—and invariants enable us to enforce—user-defined protocols on shared state, which are at the conceptual core of most recent program logics for concurrency.
A Concurrent Logical Relation. Lars Birkedal, Filip Sieczkowski and Jacob Thamsborg. January 2012. Accepted for publication at CSL 2012. [PDF]
We present a logical relation for showing the correctness of program transformations based on a new type-and-effect system for a concurrent extension of an ML-like language with higher-order functions, higher-order store and dynamic memory allocation.
Formalized Verification of Snapshotable Trees: Separation and Sharing. Hannes Mehnert, Filip Sieczkowski, Lars Birkedal and Peter Sestoft. September 2011. Accepted for publication at VSTTE 2012. [PDF][Coq development (.tar.gz)]
We use separation logic to specify and verify snapshotable search trees, fully formalizing the result. We achieve local and modular reasoning about a tree, its snapshots, and their iterators, even though the implementation involves shared mutable heap data structures with no separation or ownership relation.
Verifying object-oriented programs in higher-order separation logic in Coq. Jesper Bengtson, Jonas B. Jensen, Filip Sieczkowski and Lars Birkedal. February 2011. Accepted for publication at ITP 2011. [PDF][Coq development (.tgz)]
We present a shallow Coq embedding of a higher-order separation logic with nested triples for an object-oriented programming language. We develop novel specification and proof patterns for reasoning in higher-order separation logic with nested triples about programs that use interfaces and interface inheritance.
Automating Derivations of Abstract Machines from Reduction Semantics: A Generic Formalization of Refocusing in Coq. Filip Sieczkowski, Małgorzata Biernacka and Dariusz Biernacki. September 2010. Accepted for publication at IFL 2010. [PDF][Coq development (.tgz)]
We present a generic formalization of the refocusing transformation for functional languages in the Coq proof assistant. We propose an axiomatization of reduction semantics that is sufficient to automatically apply the refocusing method, and we prove that any reduction semantics conforming to this axiomatization can be automatically transformed into an abstract machine equivalent to it.


Towards Modular Reasoning for Realistic Programming Languages. Filip Sieczkowski. PhD thesis, IT University of Copenhagen, Denmark, November 2013. [PDF]
Automated Derivation of Abstract Machines from Reduction Semantics: A Formalisation of the Refocusing Transformation in the Coq Proof System. Filip Sieczkowski. MSc thesis, University of Wrocław, Poland, July 2010. [PDF][Coq development]

Research in Progress

Modelling Realistic Programming Languages in Coq. With Lars Birkedal, Aleš Bizjak and Yannick Zakowski. In progress.
We use the typeclass system, a recent addition to Coq, to define the category of complete, 1-bounded ultrametric spaces and provide a generic solution of certain recursive domain equations. We show how these solutions can be used to model sophisticated types. At the present we mostly consider relational models (both unary and binary), but we can also use these techniques to build sophisticated program logics, especially for concurrency.
The first version of the library and a draft of a tutorial are now available here.
We have written up a paper about the ModuRes library. It is currently under review, but a draft is available here.


During OPLSS'11, I've formalised termination and contextual (observational) equivalence of Gödel's System T in Coq. It can be found here, where for some reason it remains my most popular piece of work.

Speaking of github, there's some more of my code there, mostly small and not particularly well-developed libraries for SML, and half-baked ML-like languages used for experimenting with type systems. Nothing particularly fancy, but if you're using Smackage for some reason, smbt might come in handy for handling dependencies that use FFI.

The page for the seminar on Models and Logics for Reasoning about Higher-Order Imperative Concurrent Programs that ran in Spring 2013, is here.