Semantic Domain

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

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

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

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

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

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