(http://www.dcs.ed.ac.uk/~da/) is a Lecturer with the Laboratory for Foundations of Computer Science in the School of Informatics at the University of Edinburgh. He received his PhD in 1997 from the University of Edinburgh. During and since his PhD, he has worked on several topics related to this proposal, including fundamentals of type systems and recent work on resource bounded type systems as part of a EPSRC Grant GR/N28436 ``Type Systems for Resource-Bounded Programming and Compilation'' recently completed with Martin Hofmann. Aspinall also brings considerable experience in building high-quality research prototypes; for the last five years he has led work on the Proof General generic control system for interactive proof assistants (see http://www.proofgeneral.org).