Kevin Watkins

I am a Ph.D. student in the School of Computer Science at Carnegie Mellon University.

My curriculum vitae is available.

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. Don't believe everything you read.

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

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

*

*

**