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
A Separation Logic for Fictional Sequential
Filip Sieczkowski, Kasper Svendsen, Lars
Birkedal and Jean Pichon. Accepted for publication at ESOP 2015.
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
Iris: Monoids and Invariants as an Orthogonal Basis for
Ralf Jung, David Swasey, Filip
Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal and Derek
Dreyer. Accepted for publication at POPL 2015.
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
A Concurrent Logical Relation.
Filip Sieczkowski and Jacob Thamsborg. January 2012. Accepted for
publication at CSL 2012.
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
Formalized Verification of Snapshotable Trees: Separation
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
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
Filip Sieczkowski. PhD thesis, IT University
of Copenhagen, Denmark, November 2013.
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.
Modelling Realistic Programming Languages in Coq.
With Lars Birkedal, Aleš Bizjak and Yannick Zakowski. In
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
We have written up a paper about the ModuRes library. It is
currently under review, but a draft is
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
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.