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 than we can read them, and to fully understand a paper takes a long time, because each paper summarizes months to years...

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