Tomas Petricek, Dominic Orchard and Alan Mycroft. In Proceedings of ICFP 2014
We present a general calculus for tracking contextual properties of computations,
including per-variable properties (usage patterns, caching requirements) and
whole-context properties (platform version, rebindable resources). This resolves
questions that were left unanswered in the ICALP 2013 paper below.
Tomas Petricek. In Proceedings of AISB 2014
This essay looks how theories from philosophy of science apply
to programming language research. I argue that it is important to clearly state research
programme, avoid early over-emphasis on precision and I consider how to produce truly reusable
Tomas Petricek and Don Syme. In Proceedings of PADL 2014.
F# computation expressions F# provide a uniform syntax for computations such as
monads, monad transformers and applicative functors. The syntax is adaptable and
close to built-in language features of Python and C#. This article provides the details
shows that the right syntax can often be determined by considering laws.
Papers published previously
Tomas Petricek, Dominic Orchard and Alan Mycroft. In Proceedings of ICALP 2013.
Effects capture how computations affect the environment, coeffects capture the
requirements that computations place on the environment. We present a unified
coeffect system that can be used for checking liveness and properties of
data-flow or distributed programs,
Tomas Petricek. In Proceedings of MSFP 2012.
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 Haskell Symposium 2011.
The paper introduces a
docase notation for Haskell that 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. In Proceedings of ITAT 2009
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.
Articles and reports
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.
Tomas Petricek. Unpublished draft, 2007
This paper presents one of the first "Ajax" programming frameworks that let you develop
integrated client/server applications in an integrated way using a single language. The
framework lets you use F# on both sides and provides a smooth integration between client
and server-side code.
Tomas Petricek. First year report, Computer Laboratory.
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.
Theses and older projects
Master thesis. Charles University in Prague, 2010
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.
Bachelor thesis. Charles University in Prague, 2007
The thesis presents a web development framework for F# that automatically splits a single F#
Work in progress
Start here if you want to know that I'm currently working on and what I recently
completed. Unpublished drafts are marked as such and I'm always looking for feedback!
Tomas Petricek, Don Syme. Submitted in ML 2014 post-proceedings
Most programming languages were designed before the age of web. This matters because the web
changes many assumptions that typed functional language designers take for granted.
In this paper, we present how F# language and libraries face the challenges posed by the web.
Tomas Petricek. Submitted in December 2014
The key point made by this thesis is the realization that an execution environment or a context is
fundamental for writing modern applications and that programming languages should provide abstractions
for programming with context and verifying how it is accessed. The thesis summarizes all my work on
Tomas Petricek. In Pre-proceedings of TFPIE 2012.
Functional programming is often taught at universities, but with the recent rise of functional
programming in the industry, it is becoming important to teach functional concepts to experienced
developers. This requires a very different approach.
Talks and recordings
- Video: Coeffects - a calculus of context-dependent computation
(Presentation from ICFP 2014, Gothenburg)
- Video: Doing web-based data anlytics with F#
(Presentation from ML Workshop 2014, Gothenburg)
- Video: Understanding the World with F#
(Video lecture, Recorded at Channel 9, 2013)
- Video: How F# Learned to Stop Worrying and Love the Data
(Video lecture, Recorded at Channel 9, 2013)
- Coeffects: Types for tracking context-dependence
(Massachusetts Institute of Technology, 2013)
- Information-rich programming in F#
(Invited talk at the ML Workshop, 2012)
- Video: Coeffects: The essence of context-dependence
(Student Research Competition at ICFP 2012)
- Video: Reactive pattern matching for F#
(Lang.NET Symposium 2009, Microsoft, Redmond)
Supervisions and teaching
I'm happy to supervise Part II (final year) projects that are related to functional
and web programming or other interesting topics.
I had the pleasure of supervising some great Part II students:
I supervised the following Computer Laboratory courses for various colleges
and I'm happy to supervise them again:
I was a member of the Program Committee (PC) for
ML 2013, ML 2012,
and PSW 2012
and a member of External Review Committee (XRC) for
ISMM 2012 and
I also reviewed papers for
CC 2013 and
I'm happy to review papers that (broadly) match my interest in programming models, types,
concurrent & distribtued and reactive programming, data & web and langauge integration
(and also any controversial, provocative and novel work).
Teaching in Prague
As an undergraduate and Master's student at the Charles University in Prague, I
helped to organize and teach non-compulsory courses.
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 seminar 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).