Department of Computer Science,
Royal Holloway, University of London,
Egham,
Surrey. TW20 0EX.
Phone: +44 (0)1784 443696
Fax: +44 (0)1784 439786
Email: robin@cs.rhul.ac.uk
| Robin Adams, Department of Computer Science, Royal Holloway, University of London, Egham, Surrey. TW20 0EX. Phone: +44 (0)1784 443696 Fax: +44 (0)1784 439786 Email: robin@cs.rhul.ac.uk |
|
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 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 both in the metatheory of type theory, and its implementation in proof checkers.
I have also been working on a formalisation of the theory of PTSs in Coq, and of Weyl's predicative mathematics in Plastic.
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.
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.Robin Adams and Zhaohui Luo. Predicative Classical Logic-Enriched Type Theories. Accepted for publication in a special edition of Annals of Pure and Applied Logic on Computation and Classical Logic.
Robin Adams. Lambda-Free Logical Frameworks. Submitted to Annals of Pure and Applied Logic.
A journal paper setting out the core results from my thesis and putting them into an up-to-date context. I have found several mistakes in the proofs in my thesis since its publication, and have not been able to prove the results claimed there in full gerenality. I present correct proofs of weaker results in this paper. Several lambda-free logical frameworks have been created independently by other researchers since the publication of my thesis, and I show how my work can be applied to them.
Robin Adams and Zhaohui Luo. Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. ACM TOCL 11(2), 2010.
The journal version of the paper below.
Robin Adams and Zhaohui Luo. Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. In T. Altenkirch and C. McBride (eds.) Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers. LNCS 4502. Springer, 2007. DVI GZipped PS
Robin Adams. Coercive Subtyping in Lambda-free Logical Frameworks. In Proceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages: theory and Practice (Montreal, Quebec, Canada, August 02 - 02, 2009). LFMTP '09. ACM, New York, NY, 30-39. PDF
Zhaohui Luo and Robin Adams. Structural Subtyping for Inductive Types with Functorial Equality Rules. Mathematical Structures in Computer Science 18 (2008), 931-972. PDF
R. Adams. Formalized Metatheory with Terms Represented by an Indexed Family of Types In Filiatre, Paulin-Mohring and Werner (eds.), Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers. LNCS 3839. Springer, 2006. 1-16. DVI GZipped PS PDF
R. Adams. Pure Type Systems with Judgemental Equality. Journal of Functional Programming 16 (2): 219-246, 2006. DVI GZipped PS Abstract (text).
I prove subject reduction for functional PTSs, and hence show that the traditional system (based on beta-convertibility) and the system that uses a judgement form for equality are equivalent.
R. Adams. A Modular Hierarchy of Logical Frameworks. In Stefano Berardi, Mario Coppo, Ferruccio Damiani (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. LNCS 3085. Springer, 2004. 1-16. DVI GZipped PS.
Essentially an extended abstract for my thesis, I show briefly how to construct a system of weak logical frameworks that can be embedded as subsystems in existing frameworks.
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.
A Survey of Predicativity. DVI GZipped PS PDF
A historical survey of the various forms the idea of predicativity has taken over the years. This grew out of the background research for the paper Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. I'm hoping some day soon to get it into a publishable form.
Coercive Subtyping in Lambda-Free Logical Frameworks. DVI GZipped PS PDF
This was the talk I gave at TYPES 2007. The paper was rejected for the proceedings, but I'm hoping to polish it up and publish it somewhere.
The Consistency of Several Theories of Inductive Types. DVI.
We give set-theoretical semantics to several type theories involving inductive types, including UTT and Martin-Löf Type Theory.
The Consistency of Large Elimination. 2004. DVI.
I show that adding the ability to eliminate over kinds as well as types in UTT (the system on which Plastic is based) can lead to an inconsistency. I am still interested in the question of for which types this is the case, and I intend to return to this work some day.
Here is the proof script mentioned in that paper: girard.lf
The Lambda-Free Core of ELF. 2003. DVI.
I describe a weak, lambda-free subsystem of ELF. This was an early result which led me to the work that formed my thesis.
Inductive Types in Pure Type Systems. 2002. DVI.
An attempt to build a theory, similar to PTSs, but which could handle more than just Pi-types. The attempt, it has to be admitted, was pretty much a failure.
Adding Logic to a Pure Type System. 2002. DVI.
We describe a way of constructing logic-enriched PTSs, and show how each is equivalent to an extension of the original PTS. Not too surprising, perhaps, but an early step in the theory of logic-enriched type theories, which is still not well explored.
R. Adams. Decidable Equality in a Logical Framework with Sigma Kinds. 2001. DVI.
Part of my first-year report, this paper extends a method for proving decidability of equality given by Coquand, to a system with Sigma types and a unit type.
| Page last updated 14 March 2009. |