I just saw a poster for the QTCat workshop, which is a workshop for queer and trans people in category theory, which is being held this August 12-14, 2026 in Hamburg. Unfortunately, registration has closed, but I still wanted to post about it because they are going to livestream their talks, and it's got a pretty fascinating lineup of invited speakers: Jules Hedges , Theo Johnson-Freyd , Ioannis…
I’ve been implementing a new language, and one of the things I have been doing is implementing a language server for the first time. Interestingly, this has changed how I will write bidirectional typecheckers from now on! A bidirectional type system is a set of (syntax-directed) rules with a mode assignment, telling you which bits of the rules are inputs, and which bits are outputs. This lets you…
...it's Rocq, and no longer Coq!
One of the key skills for any academic researcher is reading other peoples' papers. The trouble is that our peers write papers faster than we can read them, and to fully understand a paper takes a long time, because each paper summarizes months to years of effort. So you cannot fully read all the relevant literature, even if you did nothing but reading. This means you need to have a way to…
The Ackermann-Péter function is defined as: A : ℕ × ℕ → ℕ A ( 0 , n) = n + 1 A (m + 1 , 0 ) = A (m, 1 ) A (m + 1 , n + 1 ) = A (m, A (m + 1 , n)) Famously, it is not expressible as a primitive recursive function. However, in lecture I showed my students that it is possible to define this function in Gödel's T. That is to say, the Ackermann-Péter function is nevertheless "higher-order primitive…
One of the weirder (and wronger) bits of "folk wisdom" surrounding the PhD is that no one reads PhD dissertations. If you look online, you'll find many posts like this one , which ask why anyone writes PhD theses when no one reads them. This would be a good question, if it were based on a true premise. In fact, if you write even a moderately decent thesis, it will probably be read by many…
My birthday just passed, and to relax I wrote a parser combinator library. Over the last few years, I have worked quite a bit with Ningning Xie and Jeremy Yallop on parser combinators, which has led to a family of parser combinators which have optimal linear-time performance in theory, and which are many times faster than lex+yacc in practice. But these use advanced multistage programming…
We have a new paper on combining separation logic and refinement types to verify C code, appearing at POPL 2023 in a couple of months. It's called CN: Verifying Systems C Code with Separation-Logic Refinement Types , and it's by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and me. Despite significant progress in the verification of hypervisors, operating…
The rule of thumb I use is that Noam Zeilberger is generally five to ten years ahead of me in identifying interesting problems. A decade ago he was working intensively on the semantics of refinement types, and lo and behold, in the last couple of years so have I. So I'd like tto tell you about two draft papers developing both the theory of refinement types, and how to apply them to verification…
I was chatting with a PhD student while back, who remarked to me that many senior PL researchers seemed stuck in a defensive crouch. I though that was quite a striking observation, because (a) he was not wrong, but (b) people his age don't have or need that posture because we are currently in a golden age for PL research. What I mean by that is that there was a period where the research tradition…
I recently read Shriram Krishamurthi and Kathi Fisler's ICER 2021 paper, Developing Behavioral Concepts of Higher-Order Functions . In this paper, they study not the theory of higher-order functions, bur rather the pedagogy of higher-order functions: how do we teach students how to program with them? In particular, they studied how students understood different higher-order functions -- e.g., map…
Henry Mercer, Cameron Ramsay, and I have a new draft paper on type inference out! Check out Implicit Polarized F: Local Type Inference for Impredicativity . System F, the polymorphic lambda calculus, features the principle of impredicativity: polymorphic types may be explicitly instantiated at other types, enabling many powerful idioms such as Church encoding and data abstraction. Unfortunately,…
If you read about programming languages on the Internet, you'll inevitably run into (or even participate in) long arguments about whether dynamic or static typing is better. A long time ago, before I went to grad school, I enjoyed arguing with people on the Internet about this very topic. But, I no longer find myself interested in that debate. This is for two reasons. One, like so many addicts…
One of the more surprising facts about the discipline of programming language theory is that it is actually possible to define what programming languages are in a reasonably mathematically satisfying way. A language is a presentation of a (generalised) algebraic theory. Basically, think of a language as a set of generators and relations in the style of abstract algebra. You need to beef up the…
Jeremy Yallop , Ningning Xie , and I have a new draft out about combinator parsing, entitled Fusing Lexing and Parsing . The abstract is short, but sweet: Lexers and parsers are typically defined separately and connected by a token stream. This separate definition is important for modularity, but harmful for performance. We show how to fuse together separately-defined lexers and parsers,…
My PhD student Faustyna Krawiec, along with me and several other coauthors, has a new paper out, which is due to appear at POPL 2022 : Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation Faustyna Krawiec, Simon Peyton-Jones, Neel Krishnaswami, Tom Ellis, Richard A. Eisenberg, and Andrew Fitzgibbon. In this paper, we give a simple and efficient…
A few weeks ago, Shriram Krishnamurthi asked an interesting question on Twitter : It's common in PL to have benchmarks for performance . But does anyone know of PL design benchmarks? This caught my attention because my longest-running research program -- my work on functional reactive programming, with 7 papers so far -- has been explicitly guided by a handful of design benchmarks. I've never…
I have an opening for a postdoctoral position in Cambridge with the European ERC Consolidator Grant project TypeFoundry. This is a 2-year position, with the possibility of extension. The TypeFoundry project aims to use recent developments in proof theory and semantics, such as polarized type theory and call-by-push-value, to identify the theoretical structures underpinning bidirectional type…
Thanks to the influence of machine learning, differentiating programs has become a big business. However, there are a lot of other things in programming language theory which are also derivatives, and people sometimes get confused about the inter-relationships. So I decided to lay out some of them and some of their interconnections. 1. Brzozowski Derivatives The first kind of derivative is the…
I am very pleased to have received an ERC Consolidator Grant for my TypeFoundry proposal. This will be a five year project to develop the foundations of bidirectional type inference. If you are interested in pursuing a PhD in this area, or conversely, are finishing a PhD in this area, please get in touch! Many modern programming languages, whether developed in industry, like Rust or Java, or in…
My blogging has been limited this past year due to RSI, but I do not want to leave things entirely fallow, and last year I wrote an email which can be edited into a decent enough blog post. Quite often, people will hear that System F, the polymorphic lambda calculus, satisfies a property called relational parametricity . We also often hear people say that the parametricity property of System F…
I just finished "attending" PLDI 2020 , a programming languages conference. Like many conferences in computer science, due to COVID-19, on short notice the physical conference had to be cancelled and replaced with an online virtual conference. Talks were streamed to Youtube, questions were posted to a custom Slack channel, there was a startling variety of online chat applications to hold…
Recently, I read a blog post in which Ben Karel summarized the reaction to a request John Regehr made about how to teach compilers , and as one might predict, the Internet was in agreement that the answer was "absolutely everything". Basically, everyone has a different perspective on what the most important thing is, and so the union of everyone's most important thing is everything. In fact, from…
Today I'd like to blog about the nicest proof of Kleene's theorem that regular expressions and finite automata are equivalent that I know. One direction of this proof -- that every regular expression has a corresponding finite automaton -- is very well-known to programmers, since Thompson's construction , which converts regular expressions to nondeterministic automta, and the subset construction ,…
Along with J. Dunfield, I have written a new survey paper on bidirectional typechecking . Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to break the decidability barrier of Damas-Milner approaches; using synthesis enables…