Thomas is learning about interactive theorem proving and working on automating verification of Pancake programs.
More contact information is available at the Contact page.
