List of published papers
I published papers about programming languages including type providers, theory of coeffects, concurrent and reactive programming, but also philosophy and history of programming. The full list of published papers is below.
Tomas Petricek, Gustavo Guerra and Don Syme. In Proceedings of PLDI 2016
The paper presents F# Data, a library of type providers that integrate external data in XML, CSV and JSON formats into the type system of the F# language. F# Data infers the shape of structured documents and uses it to guarantee a relative safety property.
Alan Mycroft, Dominic Orchard, Tomas Petricek. Semantics, Logics, and Calculi, 2016
This paper joins two recent developments related to effect systems - the development of richer effect systems based on complex algebraic structures and the development of semantic models based on monads. We show how graded joinads link the two developments.
Tomas Petricek. In Proceedings of Onward! Essays 2015
What is the definition of type? Having a clear and precise answer to this question would avoid many misunderstandings but it would hurt science, "hamper the growth of knowledge" and "deflect the course of investigation into narrow channels of things already understood".
Tomas Petricek, Don Syme. In Post-proceedings of ML 2014
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.
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.
Dominic Orchard, Tomas Petricek. Haskell 2014
This paper leverages recent advances in Haskell's type system to embed fine-grained monadic computations in Haskell, providing user-programmable effect systems. We explore a number of practical examples that make Haskell even better and safer for effectful programming.
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 experiments.
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.
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,
Don Syme, Keith Battocchi, Kenji Takeda, Donna Malayeri and Tomas Petricek. DDFP 2013
In this position paper we describe the key themes in information-rich functional programming that we have observed during the work on F# 3.0 type providers.
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.
Theses and older projects
Master thesis. Charles University in Prague, 2010
The thesis uses early version of joinad language 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
Notes, articles and reports
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.
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.
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.
Work in progress
Start here if you want to know what I'm currently working on. The documents below are unpublished drafts and any feedback is more than welcome!
Tomas Petricek. Submitted in November 2016.
Computer programs do not always work as expected. In fact, ominous warnings about the desperate state of the software industry continue to be released with almost ritualistic regularity. In this paper, we look at the 60 years history of programming and at the different practical methods that software community developed to live with programming errors.
Tomas Petricek. Presented at PPIG 2016.
Our thinking is shaped by basic assumptions that we rarely question. What are some of the hidden assumptions that we never question and that determine how programming languages are designed? And what might the world of programming look like if we based our thinking on different basic principles?
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 coeffects.
Recorded research talks
- Video: History and philosophy of types
(LambdaDays 2016 talk based on my essay)
- Video: The Gamma: Programming tools for data journalism
(Talk at Future Programming Workshop 2015)
- 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: Reactive pattern matching for F#
(Lang.NET Symposium 2009, Microsoft, Redmond)
Supervisions and teaching
To get an idea about projects, have a look at the work of some great Part II students who I had the pleasure of supervising:
- Eduardo Munoz, working on Type-safe multilanguage programming
- Lewis Brown's Refactoring tool for F#, also at GSoC 2013
- David Barker, working on Functional Reactive Programming for Data Binding in C# (Bitbucket)
I also supervised a number of Computer Laboratory courses for various colleges and I'm happy to supervise them again. The courses include the obvious PL-related suspects including Semantics of Programming Languages, Concepts in Programming Language, Types, Optimising Compilers and Denotational Semantics.
I was a member of the Program Committee (PC) for TyDe 2016, HaPoP 3, TFP 2015, ML 2013, ML 2012, CUFP 2012 and PSW 2012 and a member of External Review Committee (XRC) for ISMM 2012 and ISMM 2011. I also reviewed papers for JLAMP, PLACES 2016, CiE 2015, PPDP 2015, PPDP 2013, TLCA 2013, CC 2013 and ECOOP 2012.
I'm happy to review papers that (broadly) match my interest in data-driven programming, programming models, types, concurrent and reactive programming, web and language integration, philosophy of programming (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.
Programming languages F# and OCaml (English)
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.
WinFX Programming (Czech)
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).