I am currently engaged in the project Quantum Computation, Logic, and Security led by Prof. Jacobs. I am interested in giving semantics to quantum computing, and the analogies that Prof. Jacobs has discovered between the appropriate logic for doing this, and the logics for probabilistic and classical reasoning, the so-called state-and-effect triangles. I am creating a syntax for these triangles, provisionally entitled QPEL (Quantum Programming and Effect Logic).
My research has also been 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.
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 Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. Submitted to post-proceedings of TYPES 2015.
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of states. This conditioning uses a key aspect that distinguishes our probabilistic type theory from quantum type theory, namely the bijective correspondence between predicates and side-effect free actions (called instrument, or assert, maps). The paper shows how suitable computation rules can be derived from this predicate-action correspondence, and uses these rules for calculating conditional probabilities in two well-known examples of Bayesian reasoning in (graphical) models. Our type theory may thus form the basis for a mechanisation of Bayesian inference.
We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs — effects. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that al- lows semantics in terms of C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.
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.
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.
Zhaohui Luo and Robin Adams. Structural Subtyping for Inductive Types with Functorial Equality Rules. Mathematical Structures in Computer Science 18 (2008), 931-972.
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.
R. Adams. Pure Type Systems with Judgemental Equality. Journal of Functional Programming 16 (2): 219-246, 2006.
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.
This turned out to be 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.
QPEL - Quantum Program and Effect Language. Given at QPL 2014, Kyoto.
Warning: there are mistakes in this talk. The category of Hilbert spaces does not fit the definition of state-and-effect triangle.
A Type Theory for Formalising Category Theory. Given at RHUL 2014.
A little side project that I've been playing with for a while. An attempt to create a category theoretic foundation for mathematics, that treats categories, objects and arrows as undefined terms.
I'd like to create a type theory with three 'levels' - proofs and propositions, elements and sets, objects and categories. At the category level, we can define functors and natural transformations using lambda-abstraction, and have rules for applying functors to objects and arrows.
Categorical Semantics for Logic-Enriched Type Theories. Talk given at TYPES 2011.
I 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.
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; the ideas come from Charles Stewart's thesis. I found it useful to write down the construction on its own, and put my notes here in case others find them useful.
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.
We give set-theoretical semantics to several type theories involving inductive types, including UTT and Martin-Löf Type Theory.
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.
I describe a weak, lambda-free subsystem of ELF. This was an early result which led me to the work that formed my thesis.
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.
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.
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.
My profiles on: