Semantic Domain

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.

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.

...it's Rocq, and no longer Coq!

One of the key skills for any academic researcher is reading other peoples' papers.

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.

One of the weirder (and wronger) bits of "folk wisdom" surrounding the PhD is that no one reads PhD dissertations.

My birthday just passed, and to relax I wrote a parser combinator library.

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.

The rule of thumb I use is that Noam Zeilberger is generally five to ten years ahead of me in identifying interesting problems.

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 recently read Shriram Krishamurthi and Kathi Fisler's ICER 2021 paper, Developing Behavioral Concepts of Higher-Order Functions.

Henry Mercer, Cameron Ramsay, and I have a new draft paper on type inference out!

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.

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.

Jeremy Yallop, Ningning Xie, and I have a new draft out about combinator parsing, entitled Fusing Lexing and Parsing.

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 P…

A few weeks ago, Shriram Krishnamurthi asked an interesting question on Twitter: It's common in PL to have benchmarks for performance.

I have an opening for a postdoctoral position in Cambridge with the European ERC Consolidator Grant project TypeFoundry.

Thanks to the influence of machine learning, differentiating programs has become a big business.

I am very pleased to have received an ERC Consolidator Grant for my TypeFoundry proposal.

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.

I just finished "attending" PLDI 2020, a programming languages conference.

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".

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.

Along with J.