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:
- Ported PVS’s BDD package to 64-bit machines, as 64-bit builds were starting to become common at the time.
- Ported PVS to SBCL. Prior to that, it only ran on Allegro Common Lisp, a commercial product. Some work had already been done on porting to other lisps, but I got PVS to run on a second Lisp for the first time. To be fair, Sam Owre had to do a fair amount of work on top of my port before the bugs were really ironed out.
- Contributed theorems to the PVS prelude. Just search for my name in there.
- Contributed theorems to the NASA PVS Library. You can see the collections to which I contributed here.
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 have been working on recursive function theory. I hope to submit my work upstream soon. In the meantime, I’ve been helping to make proofs shorter in set.mm.