Department of Computer Science
University of Durham
4pm Wednesday 12 December
Room 2511, JCMB, King's Buildings
I present our new high-level syntax for functional programming in dependent type theory, together with a prototype tool for programming interactively in the style it supports.
As well as supporting pattern matching on inductive families of datatypes, as envisaged by Coquand, our notation also permits the abstraction and subsequent analysis of intermediate computations on the left-hand sides of programs. This easily subsumes the notion of `Boolean guards' in simply typed languages. Moreover, when combined with the power of dependent pattern matching to refine type information, it delivers Wadler's notion of `view' for free!
By way of example, we develop a typechecker for the simply-typed lambda calculus, which furnishes a view of raw terms as either being well-typed, or containing an error. The implementation of this view is a proof that typechecking is decidable.
(Joint work with James McKinna.)
Martin Grohe
Tuesday 9 October 2001
An error occured whilst processing this directive