Semantic Domain

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

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

I recently read Shriram Krishamurthi and Kathi Fisler's ICER 2021 paper, Developing Behavioral Concepts of Higher-Order Functions . In t...