Logic with a black tie and tails

I've had lots of fun with formal logic and theorem provers. This is a partial list of what I have done.

PVS

Just after graduate school, when I was working at the University of Kansas, I discovered PVS, a formal verification system. PVS lets you write a formal specification of a system, then prove theorems about that system. After learning my way around the system, I made a number of contributions, including:

Metamath

My use of PVS petered out around 2007. Fast forward to 2016. After reading an article about metamath, I decided to give it a try. It's fun! I've been formalizing the material in N. J. Cutland's book, Computability: An introduction to recursive function theory. I've gotten through Definition 2.3 on page 27, in chapter 2. If you would like to see it, look here. This is based on the develop branch of the set.mm git repository, on top of commit 285ac8b75204fc0effea8fc8ed5355f7bbef5acd by Norm Megill on Friday May 19, 2017.