Robin Adams

Robin Adams
Institute for Computing and Information Sciences
Radboud University

Mercartor 1
Toornooiveld 212
6525EC Nijmegen


0243652031

I am a post-doctoral researcher in Computer Science at Radboud University Nijmegen on the ERC project Quantum Computation, Logic, and Security, led by Prof Bart Jacobs.

Research Interests

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.

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.

Publications

Talks and Posters

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.

My CV

My profiles on: