Robin Adams

Robin Adams,
Department of Computer Science,
Royal Holloway, University of London,
Surrey. TW20 0EX.
Phone: +44 (0)1784 443690
Fax: +44 (0)1784 439786
Skype: radams78

I am a Lecturer in the Department of Computer Science at Royal Holloway, and a member of the Type Theory and Applications research group.

My office is McCrea 107.

Research Interests

My research is in the area of type theory.  I have become fascinated with the perspective on logic that it provides, from which proofs appear, not as static lists of statements, but as active computational agents, performing calculations both on ordinary mathematical objects and on one another.  I am interested primarily in the metatheory of type theory, but also in its use for formalisation in practice, implementated in proof checkers.

Current Project

In March, I began a project entitled Classical Dependent Type Theories, funded by the EPSRC First Grant Scheme. I will be attempting to find a consistent way to marry dependent types and control operators. A web page describing this project is under construction.

Previous Projects

Until 2009, I was a Research Fellow on an EPSRC Early Career Fellowship. The title of my project is "Reverse Mathematics in Dependent Type Theory".

Before the Fellowship, I was working with Zhaohui Luo as part of project Pythagoras.

I have also worked on a formalisation of the theory of PTSs in Coq, and of Weyl's predicative mathematics in Plastic.

As part of the TCS-SOUP series of seminars, Zhaohui and I organised a one-day workshop on dependent type theory on Wednesday 19th July 2006.



Unpublished Papers

The 'slush pile' - including preprints, rejected papers, and short notes on questions that, perhaps only briefly, caught my interest.  Explore at your own risk.

Don't trust the dates in the papers themselves; they simply give the last time the source code was compiled.


Page last updated 26 Jan 2012.