I'm a second-year PhD Student in the Computer Laboratory at the University of Cambridge and a member of the Programming, Logic and Semantics Group. My supervisors are Alan Mycroft from the Computer Laboratory and Don Syme from Microsoft Research.
Before joining the Computer Laboratory, I finished Master's degree in theoretical computer science at the Faculty of Mathematics and Physics of Charles University in Prague. I also did two internships with Don Syme.
Besides my studies, I'm an active member of the F# community, I sometimes speak at various .NET or Functional Programming industry events and I wrote a book about F# and I write a blog. See my professional home page.
I can be contacted at
I supervised the following Computer Laboratory courses and I'm happy to supervise them again:
I'm a functional programmer and I think that F# and functional programming should be used in practice. I wrote a book that explains functional concepts to professional developers with C# background using C# and F# examples.
It is available from Manning or from your favorite store.
Joinads extend monadic notation in F# and Haskell with a feature that is useful for concurrent, parallel and reactive programming.
To learn more and experiment with joinads in a web browser visit Try Joinads!
I'm a lazy photographer with no online gallery at the moment, but I have been uploading a new photo to my online calendar every month for quite some time.
I was a member of the Program Committee (PC) for ML 2012, CUFP 2012 and PSW 2012 and a member of External Review Committee (XRC) for ISMM 2012 and ISMM 2011.
I also reviewed some papers for ECOOP 2012 and CC 2013.
I'm happy to review papers for conferences or journals that (broadly) match my interest in programming models; functional programming and type systems; concurrent, distribtued and reactive programming (and also any controversial, provocative and novel work).
Charles University, Winter 2009/2010
The lecture teaches programming in the ML-family of languages and highlights the mathematical foundations of ML languages. As a results students should find it easier to understand many mathematical concepts. It also explains advanced F# features such as computation expressions.
Charles University, Summer 2005/2006
A practically oriented lecture about Windows programming using the WinFX framework (now called WPF, WCF and WF), which was in beta version in 2006. It discussed graphics, working with data and communication between applications. (Jointly taught with Vojtech Jakl).
For my other activities and projects that I am or was involved in, visit my professional home page.
I'm interested in programming models. That is, what is the best “language” for solving problems from a particular domain, how to encode these models in programming languages and how to guarantee that the programming model avoids certain kinds of errors. More specifically, I'm interested in meta-programming, embedded languages, monads and other abstract representations of computations, as well as clever type systems.
You can read about my current research programme in a first-year report. Briefly, the areas that I'm working on now or have worked on in include:
Coeffect systems. I'm working on types for tracking how computation depends on some context. For example, on which nodes (server, phone, web browser, ...) can a function execute in a distributed language. Such properties are dual to effects, so I use the term coeffect. See a recent draft for more information.
Reactive and concurrent. I designed a language extension for F# that can be used for encoding reactive, concurrent and parallel programming models. You can and experiment with it on the TryJoinads web site.
Distributed and web programming. I developed an F# framework that allows writing client/server applications in an integrated, type-safe way. See an technical report and my bachelor thesis. Recent implementations of the idea include commerical WebSharper and open-source Pit.
Below are links to accepted papers as well as drafts that I'm currently working on. Comments and suggestions are welcome. If I missed some important related work, let me know!
We consider three examples of context-dependence analysis: liveness analysis, tracking the use of rebindable resources, and calculating caching requirements for data-flow programs. Informed by these cases, we present a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads.
Abstractions such as monads, monoids and applicative functors are a useful way of expressing various computations used in practice. However, they are hard to use without a convenient syntactic sugar. In this parper, we describe F# computation expressions, which provide such syntax for a large number of practically useful computations.
Functional programming is often taught at universities. With the recent rise of functional programming in the industry, it is becoming important to teach functional concepts to experienced developers. This paper presents our experience with taching functional ideas to professional developers through C# and F#.
When translating pure functional code to a monadic version, we need to use different translation depending
on the desired evaluation strategy. In this paper, we present an unified translation that is parameterized by
malias. We also show how to give call-by-need translation for certain
Tomas Petricek, Alan Mycroft and Don Syme.
In Proceedings of Haskell Symposium 2011.
The paper introduces a
docase notation for Haskell. The notation can be used for any monad that
provides additional operations representing parallel composition, choice and aliasing. We require the
operations to form a near-semiring, which gurantees that the notation resembles pattern matching.
Tomas Petricek and Don Syme. In Proceedings of PADL 2011.
Reactive, parallel and concurrent programming models are often difficult to encode in general-purpose programming languages. We present a lightweight language extension based on pattern matching that can be used for encoding a wide range of these models.
Don Syme, Tomas Petricek and Dmitry Lomov. In PADL 2011.
We describe the asynchronous programming model in F#, and its applications. It combines a core language with a non-blocking modality to author lightweight asynchronous tasks. This allows smooth transitions between synchronous and asynchronous code and eliminates the inversion of control.
Tomas Petricek and Don Syme. In Proceedings of ISMM 2010.
The article discusses memory leaks that can occur in a reactive programming model based on events. It presents a formal garbage collection algorithm that could be used in this scenario and a correct reactive library based on this idea, implemented in F#.
Tomas Petricek. The Monad.Reader Issue 18.
The article presents several monads that can benefit from the parallel monad comprehension notation that is supported in the re-designed monad comprehension syntax in Haskell. The examples are inspired by the work on joinads and include parsers, parallel and concurrent computations.
Talk at the Institute of Cybernetics (Tallin University) that describes coeffect systems for tracking how expressions depend on some context. Coeffects are associeted with the context and can be modelled using comonads. They can be used to express properties from distributed programming, secure information flow and others.
Preliminary talk from Computer Laboratory that introduces coeffect systems for tracking how expressions depend on some context. The talk discusses relations between effects and monads & coeffects and comonads.
I presented joinads at the Lang.NET Symposium 2009. The talk presents the F# language extension and examples focusing on reactive programming. Updated slides from a talk at MSR Cambridge contain more information.
Some ideas from my reactive programming research have made it to the standard F# library. This talk from the F# user group in London shows how to write real-world reactive programms in F#.
This talk from ISMM 2010 discusses garbage collection of events in a reactive programming framework. It presents an astonishing duality between traditional references and references between events.
The research goal discussed in the report is to use types in an ML-style language to track additional properties of computations including various kinds of effects (communication, memory access) and coeffects (how a computation depends on a context). The document briefly summarizes the work done during the first-year (including the work on joinads and coeffects) and it proposes future research projects.
The thesis uses early version of joinad langauge extension for F# and garbage collection for events. Based on these concepts, it builds a simple reactive library for F# that allows writing reactive computations in both control-flow and data-flow styles.
The paper shows how to encode certain monadic computations (such as a continuation monad for asynchronus programming) using the iterator language feature in C# 2.0. The paper was presented at ITAT 2009.