Semantic Domain

The Ackermann-Péter function is defined as:
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 researchers in your field. This is for a simple reason: a thesis has a much higher page limit than...

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

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