Department of Computer Science,
Royal Holloway, University of London,
Egham,
Surrey. TW20 0EX.
Phone: +44 (0)1784 443690
Fax: +44 (0)1784 439786
Email: robin@cs.rhul.ac.uk
Skype: radams78
| Robin Adams, Department of Computer Science, Royal Holloway, University of London, Egham, Surrey. TW20 0EX. Phone: +44 (0)1784 443690 Fax: +44 (0)1784 439786 Email: robin@cs.rhul.ac.uk 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.
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.
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.
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.
Robin Adams and Zhaohui Luo. Classical Predicative Logic-Enriched Type Theories. Annals of Pure and Applied Logic 161 (2010) 1315--1345
This paper started as an attempt to investigate which is stronger - LTTW (see 'Weyl's Predicative Mathematics...' below) or ACA0, which is usually taken to be a formalisation of Weyl's foundation. (It is.) However, it grew into something much more. It presents a method of showing that one LTT is conservative over another. The proof is technically complex, but I believe the core idea is absolutely beautiful. The method is very general, applying to type theories and logics too; in particular, we show how it gives a new proof of the conservativity of ACA0 over PA.
Robin Adams. Lambda-Free Logical Frameworks. To be published in 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 motivation for this work was to see if LTTs can formalise some schools of thought in the foundations of mathematics that cannot be captured properly by either a type theory or an orthodox system of logic alone. We looked at Hermann Weyl's Das Kontinuum, and were in for a shock - read with a modern eye, the definition of his system reads exactly like a logic-enriched type theory. We give the formal definition of this logic-enriched type theory LTTW, and describe a formalisation of every result in Das Kontinuum in this LTT using the proof checker Plastic.
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.
Categorical Semantics for Logic-Enriched Type Theories. PDF
Talk given at TYPES 2011. My current work, and something I'm very excited about. I've found a general definition of logic-enriched type theory, syntactic translation, model and semantic functor between models that (seems to) generalise(s) all the important cases from both traditional first- and second-order logic, and the categorical semantics of type theories. Moreover, it makes Curry-Howard into an object to be studied - one of these syntactic translations. I really think this might lead us to a better understanding of Curry-Howard in the next few years.
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.
Control Operators and Natural Numbers are Degenerate. PDF
I show that, if we have control operators, we can write a term that reduces either to a successor or to zero, depending which reduction strategy is followed. This is the clearest example I know of as to why control operators don't play well with the other features of type theory. The idea is not at all original, but I haven't seen the details made explicit before. Edit: The ideas were made explicit in Charles Stewart's thesis.
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 polished it up and published it in LFMTP'09.
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.