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.
- 2017. A Type Theory for Probabilistic and Bayesian Reasoning. Leibniz International Proceedings in Informatics.
- 2016. A Strongly Normalizing Computation Rule for Univalence in Higher-Order Minimal Logic. arXiv.org.
- 2014. QPEL - Quantum Program and Effect Logic. Electronic Proceedings in Theoretical Computer Science. 172: 133-153. doi: 10.4204/EPTCS.172.10
- 2011. A Pluralist Approach to the Formalisation of Mathematics. Mathematical Structures in Computer Science. 21: 913-994. doi: 10.1017/S0960129511000156
- 2010. Classical Predicative Logic-Enriched Type Theories. Annals of Pure and Applied Logic. 161: 1315-1345. doi: 10.1016/j.apal.2010.04.005
- 2009. Weyĺ's Predicative Classical Mathematics as a Logic-Enriched Type Theory. ACM Transactions on Computational Logic. 11. doi: 10.1007/978-3-540-74464-1_1
- 2008. Structural Subtyping for Inductive Types with Functorial Equality Rules. Mathematical Structures in Computer Science. 18: 931-972. doi: 10.1017/S0960129508006956
- 2006. Pure Type Systems with Judgemental Equality. Journal of functional programming (Print). 16: 219-246. doi: 10.1017/S0956796805005770
- 2009. Coercive Subtyping in a Lambda-Free Logical Framework. Paper 4, pages 30-39. In:
- 2009. LFMTP 2009 : proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages : theory and practice : August 2, 2009, Montréal, Canada. ACM Press. 87 pages. ISBN: 978-1-60558-529-1.
- 2007. Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. Paper 1, pages 1-17. In:
- 2007. Types for Proofs and Programs, International Workshop, TYPES 2006, Revised Selected Papers. Springer. 268 pages. ISBN: 978-3-540-74463-4.
- 2006. Formalized Metatheory with Terms Represented by an Indexed Family of Types. Paper 1, pages 1-16. In:
- 2006. Types for Proofs and Programs. Springer. 273 pages. ISBN: 978-3-540-31429-5.
- 2004. A Modular Hierarchy of Logical Frameworks. Paper 1, pages 1-16. In:
- 2004. Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers. Springer. 408 pages. ISBN: 3-540-22164-6.
Robin Adams and Bart Jacobs. A Type Theory for Probabilistic and Bayesian Reasoning. To appear in 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.
The Coq files referred to in this paper are available here.
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.PhD thesis, University of Manchester, 2004.
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.