There's a dodgy version of a certain proof assistant available (ask me no questions and I will tell you no lies) only in a brown paper bag.

Slides

• my Cambridge gig about Observational Type Theory, based on joint work with Thorsten Altenkirch.
• my Sheffield gig, Dependent Pattern Matching Evolves, based on joint work with Healfdene Goguen and James McKinna.
• my DT meets PP gig: Programmable Pattern Analysis
• real soon now, my Nottingham WGP gig: Universe Constructions as a Medium for Generic Programming, or Small is Beautiful
• real soon now, the gig I didn't do at TYPES 2000: Elimination with a Motive
• real soon now, slides about linear contexts for regular datatypes
• my `farewell' gig at the LFCS: A Case for Dependent Families, including types for search trees and sorted lists, together with the insert and flatten functions...
• a few general slides about dependent pattern matching
• OLEG slides
• what has Type Theory done for me? well, my proof that first-order unification terminates is refreshingly short, because my dependently typed program is structurally recursive; correctness is pretty easy too...
• slides about rumours about programs