Research
Teaching
Commercial
Admin
Other

Research

My interests include computer security (particularly proof-carrying code and authentication), programming and specification languages (particularly type systems and modules) and theorem proving (particularly proof development environments and proof language foundations).

I'm a member of the Laboratory for Foundations of Computer Science (LFCS) and the Mathematical Reasoning Group.

Publications

(NB: these lists are out of date; I am in progress of updating to a new web site; meanwhile DBLP has a pretty complete list of my work)

Upcoming/recent Meetings

EclipseCon 2010. I'm attending to reminisce about Proof General Eclipse (which isn't quite dead, but is in suspended development) and to discuss ideas for an Eclipse static analysis framework.

UITP 2010. Please submit a paper to User Interfaces for Theorem Provers, 2010. It's part of the massive FLoC, in sunny Edinburgh this summer.

Research Projects

The Mobility and Security Group is working on ideas for new projects. Our two main projects ended in 2009, these were:

ReQueST has an EPSRC-funded follow-on project called Resource Static Analysis building static analysis tools for Java programs to analyse and check their resource usage.

Together with Mike Just I have been working on studying new and current techniques for Knowledge-Based Authentication.


Proof General logo

Proof General, which provides generic proof development environments for Isabelle, Coq, and other theorem provers.

I am also a co-Investigator on the main Platform Grant The Integration and Interaction of Multiple Mathematical Reasoning Processes held in the Mathematical Reasoning Group which is conducting a range of exciting work connected with automated and interactive theorem proving. We have recently been awarded funding for a visiting mathematician to work on formalising some new parts of mathematics inside Isabelle, in a grant entitled The potential of automated reasoning tools to assist the working mathematician.

See also some of my past projects.

Research Students

Current students:

If you're interested in studying for a PhD, drop me a line to discuss topics and check the Informatics PG page and the LFCS PG page. I will supervise students within my areas of interest,

Former students:



Valid XHTML 1.0!
my Vcard
David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact   GPG key (Instant HOWTO)