Personal tools
You are here: Home Events Abstract Archives 2001 The View from the Left

The View from the Left

Conor McBride 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.)

Document Actions