Kevin Watkins

I was a Ph.D. candidate in the School of Computer Science at Carnegie Mellon University, but am currently ABD (all but dissertation) in absentia.

I am currently serving as a Senior Software Engineer at QVT Financial LP.

My resume/CV is available as a printable PDF and an HTML version with hyperlinks. A list of publications and presentations is also available.

New! Slides and manuscript on Conway's Lost Cosmological Theorem.

Contact information

Research

My research interests include programming languages, logical frameworks, type theory, linear and substructural logics, and logic programming. Some of my papers and (CMU access only) drafts are available on my research page.

More drafts

These notes are often sketchy. This section has not been updated in a while.

An LF signature for Wadler's “Girard-Reynolds isomorphism” (the March 2004 variant). And notes on Wadler's paper.

Notes and examples of ML syntax.

Probabilites for election 2004 derived from the TradeSports state-by-state electoral college futures markets

Monadic reflection

Political futures markets

Coroutines

Silly combinator tricks

Chaitin's construction

The magic constructive quantifier diagram.

Preliminary investigation of certain properties relating to extensionality in an Elf development of HOL, and a variation on the description axiom.

New Elf proof of Hurkens's simplification of Girard's paradox, which states that HOL with polymorphic terms is inconsistent. (Applications: 1. (type : type) leads to the numeralwise representability of all partial recursive functions. 2. There is no polymorphic equality predicate in any extensional model of System F.)

New draft on a representation of HOL Light's core in LF (inspired by Thomas Hales's Flyspeck talk here at CMU).

Scanned papers

What am I reading now?

Random photos

See the route of a recent bike ride (more or less).