OLEG, A Type Theory With Holes, Lets And Guesses

You Can't Put A Hole Where A Hole Don't Belong

These slides describe the method I used for adding a sound account of holes (less informatively known as metavariables) to an existing dependent type theory, without using a notion of explicit substitution. I don't claim it's the best way of doing things, just that it's very cheap, and required only a small rearrangement of LEGO.

Since the slides tend to be animated or multistage, each `episode' is represented by an HTML frameset, with the images on the left and the navigational information on the right. Simply clicking on each link in turn through the body of the commentary will operate the correct sequence.

So, here's the place to begin

Conor's home page.