<< BIO
Vitals
US Citizen
Born: 18 October, 1983 {age 31}
Erdös number: 3 {Passmore > Gurevich > Shelah > Erdös}
My Academic Family Tree
(where `parent' means `Ph.D. supervisor'), extracted from The Mathematics Genealogy Project
Current Positions
 CoFounder and CEO, Aesthetic Integration,
London
 Principal, Imandra Capital Group Limited, Guernsey
 Life Member, Clare Hall, University of Cambridge
 Honorary Associate, LABORES  Laboratoire de Recherche Scientifique, Paris
(Recent) Previous Positions
{October, 2010  April, 2014}
Researcher on CambridgeEdinburgh EPSRC
grant Automatic Proof Procedures for Polynomials and Special
Functions
{October, 2010  April, 2014}
Research Associate, LFCS, University of Edinburgh
{December, 2010  December, 2012}
Postdoctoral Associate in Metamathematics of Real Algebraic Geometry, Clare Hall, University of Cambridge
{July  December, 2012}
Visiting Scientist with André Platzer, Logical Systems Laboratory, Carnegie Mellon University
{January  July, 2012}
Programme Participant, SAS: A Legacy of Alan Turing, Isaac Newton Institute for Mathematical Sciences, Cambridge, England
{January, 2011}
Visiting Researcher with Yuri Gurevich, Microsoft Research [FSE],
Redmond, Washington, USA
{September, 2007  October, 2010}
PhD Student of Paul B. Jackson, LFCS and Mathematical Reasoning Group,
University of Edinburgh, Scotland
{April, 2010}
Visiting Researcher with Florent Kirchner, INRIA/IRISA [CELTIQUE],
Rennes, Bretagne, France
{April  June, 2009}
Research Intern with Leo de Moura, Microsoft Research [SRR],
Redmond, Washington, USA
{May  October, 2008}
Visiting Fellow with N. Shankar and Sam Owre, SRI International [FMDS],
Menlo Park, California, USA.
Funded by NASA Cooperative Agreement NNX08AC59A and by NSF SGER Grant No. CNS0823086.
Education
PhD, University of Edinburgh {2011} PhD
Dissertation: Combined Decision Procedures for Nonlinear
Arithmetics, Real and Complex
PhD Area: Automated Theorem Proving and Algorithmic Algebraic Geometry
PhD Supervisor: Dr. Paul B. Jackson
Mathematical Reasoning Group & Algorithms and Complexity Group
Laboratory for Foundations of Computer Science (LFCS), School of
Informatics
PhD Examiners: Dr. Daniel Kroening (Oxford) and Dr. Alan Smaill (Edinburgh)
Master Class, Mathematical Research Institute in The Netherlands
{2007}
Project: Abstract Properties of Partial Combinatory Algebras
Advisor: Jaap van Oosten
Administered by Department of
Mathematics, Universiteit Utrecht &
Department of Mathematics,
Katholieke Universiteit Nijmegen
BA, University of Texas at Austin {2007}
Honors Thesis: Diophantine Sets and Their Decision Problems
Thesis Advisor: Prof. Dr. Robert S. Boyer
Department of Mathematics
Lectures Given and Scientific Participation {20042014}
 Queen Mary Theory Seminar
September 10th, 2014
I presented a talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
Research Group in Theoretical Computer Science
Queen Mary, University of London
London, England, UK
 MAP: Mathematics = Algorithms + Proofs
May 2630th, 2014
I presented an invited talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
IHP Trimester on Semantics of Proofs and Certified Mathematics
Institut Henri Poincaré
Paris, France
 DPMMS, Cambridge
 Departmental Talk
April 24th, 2014
I presented a talk titled ``Computing Downward LowenheimSkolem:
Hands on with the Real Algebraic Numbers.''
Dept of Pure Mathematics and Mathematical Statistics (DPMMS)
University of Cambridge
Cambridge, England, UK
 Royal Society International Seminar: Computational Interpretations of
Mathematical Theorems
November 2526th, 2013
Kavli Royal Society International Centre
The Royal Society at Chicheley Hall
Buckinghamshire, England, UK
 COST Action Meeting  EU Rich Model Toolkit Working Group
October 17th, 2013
I presented a talk (joint with Leo de Moura) titled ``Exact Global Nonlinear Optimization on Demand.''
IMDEA Software Institute
Madrid, Spain
 Schloss Dagstuhl Seminar on Deduction and Arithmetic
October 6th  8th, 2013
I presented a talk (joint with Leo de Moura) titled ``Exact Global Optimization on Demand.''
Schloss Dagstuhl  LeibnizZentrum für Informatik
Dagstuhl, Germany
 SIAM Conference
on Applied Algebraic Geometry
August 1st  4th, 2013
I presented a talk (joint with Leo de Moura) titled ``Automatic
Proofs for Transcendental Function Inequalities and an Application to
Global Optimization.''
Colorado State University
Fort Collins, Colorado, USA
 24th International Conference on Automated Deduction (CADE24)
June 9th  14th, 2013
Leo de Moura presented a talk on our joint work titled ``Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.''
Lake Placid, NY, USA
 Automated Deduction: Decidability, Complexity, Tractability (ADDCT2013)
June 10th, 2013
I presented a talk (joint with Leo de Moura) titled ``(Exact Global Nonlinear) Optimization on Demand.''
Colocated with CADE24
Lake Placid, NY, USA
 Edinburgh Mathematical Reasoning Group (DReaM Talk)
May 14th, 2013
I presented a talk (joint with Leo de Moura) titled ``Some Unexpected Applications of Nonstandard Models.''
Mathematical Reasoning Group
University of Edinburgh
Edinburgh, Scotland, UK
 Reproducibility in Computational and Experimental Mathematics
December 14th, 2012
Jeremy Avigad presented a talk (including our joint work on logic in SAGE) called ``Interactive Theorem Proving, Automated Reasoning, and Mathematical Computation.''
Institute for Computational and Experimental Research in Mathematics (ICERM)
Brown University
Providence, Rhode Island, USA
 CMACS Seminar on Real Algebra and Hybrid Systems
September  December, 2012
I gave a series of lectures on real algebra and decision procedures over real closed fields and transcendental extensions.
Logical Systems Laboratory
Carnegie Mellon University
Pittsburgh, Pennsylvania, USA
 Conference on Intelligent Computer Mathematics
July 8th  13th, 2012
I presented a talk (joint with Larry Paulson and Leo de Moura) titled ``Real Algebraic Strategies for MetiTarski Proofs.''
Jacobs University
Bremen, Germany
 International Workshop on Strategies in Rewriting, Proving and Programming
July 1st, 2012
I presented a talk (joint with Leo de Moura) titled ``The Strategy Challenge in SMT Solving.''
Part of IJCAR, 2012
University of Manchester
Manchester, England
 Computability in Europe 2012: Turing Centenary Conference
June 19th, 2012
I presented a talk (joint with Paul Jackson) titled ``Abstract Partial Cylindrical Algebraic Decomposition I: The Lifting Phase.''
University of Cambridge
Cambridge, England
 SAT/SMT Summer School 2012
June 12th  15th, 2012
Fondazione Bruno Kessler
Trento, Italy
 Robin Milner Symposium 2012
April 15th  18th, 2012
University of Edinburgh
Edinburgh, Scotland
 Semantics and Syntax: A Legacy of Alan Turing (SAS) Programme
January 19th, 2012
I presented a talk titled ``Decision Methods over Real and Algebraically Closed Fields.''
Isaac Newton Institute for Mathematical Sciences
Cambridge, England
 Visiting Jeremy Avigad at Carnegie Mellon University
December 12th  17th, 2011
Pittsburgh, Pennsylvania, USA
 Visiting Leonardo de Moura at Microsoft Research, Redmond
December 7th  11th, 2011
Redmond, Washington, USA

Dulles High School Math and Science Academy
December 6th, 2011
I presented a talk titled ``On the Mathematical Experience'' to my high school alma mater!
Sugar Land, Texas, USA

17th International Conference on Principles and Practice of Constraint Programming
September 14th, 2011
Leonardo de Moura presented a talk on our joint work titled ``Orchestrating Decision Engines.''
Perugia, Italy

18th International Symposium on Fundamentals of Computation Theory
August 2225, 2011
Yuri Gurevich presented a lecture on our joint work titled ``Impugning Randomness, Convincingly.''
University of Oslo
Oslo, Norway

CUNY Logic Seminar
March 22nd, 2011
Yuri Gurevich presented a seminar on our joint work titled ``Impugning Randomness, Convincingly.''
Graduate Center CUNY
New York, New York, USA

Deduction at Scale
March 8th, 2011
Paul B. Jackson presented a talk on our joint work titled ``Improved Techniques for Proving Nonlinear Arithmetic Problems.''
Ringberg Castle
Max Planck Society
Tegernsee, Germany

Deduction at Scale
March 7th, 2011
Leonardo de Moura presented a talk on our joint work titled ``Orchestrating Decision Engines.''
Ringberg Castle
Max Planck Society
Tegernsee, Germany

Cambridge Automated Reasoning Group Lunch
February 22nd, 2011
I presented a talk titled ``The Strategy Challenge in Computer Algebra.''
Computer Laboratory
University of Cambridge
Cambridge, England, UK

Galois, Inc. Tech Talk
February 7th, 2011
I presented a talk titled ``The Strategy Challenge in Computer Algebra.''
Galois, Inc.
Portland, Oregon, USA

Principia Mathematica 100th Anniversary Symposium
November 2728th, 2010
Trinity College
University of Cambridge
Cambridge, England, UK
 Trusted Extensions of Interactive Theorem Provers
August 1112th, 2010
I presented (joint with Paul B. Jackson and Florent Kirchner) a talk titled ``Thoughts on Trusting RAHD Computations.''
University Centre
University of Cambridge
Cambridge, England, UK
 Logics for System Analysis
Colocated with LICS and IJCAR (FLoC)
July 15th, 2010
I presented (joint with Paul B. Jackson) an introductory tutorial titled ``Combined Decision Techniques for the
Existential Theory of the Reals.''
I presented (joint with Florent Kirchner) a talk titled ``Thinking Outside the (Arithmetic) Box: Certifying RAHD
Computations.''
University of Edinburgh
Edinburgh, Scotland, UK
 LFCS Lab Lunch
July 6th, 2010
I presented a talk titled ``Some Recent Work on SAT Modulo Nonlinear Real Arithmetic.''
University of Edinburgh
Edinburgh, Scotland, UK
 Gametheoretic Probability and Related Topics
June 21st  23rd, 2010
I presented a talk (joint with Yuri Gurevich) titled ``Towards Algebraic Descriptive Randomness.''
Royal Holloway, University of London
London, England, UK
 Dagstuhl Seminar on Decision Procedures in Hardware, Software, and Bioware
April 1823rd, 2010
I presented a talk (joint with Leo de Moura and Paul B. Jackson) titled
``Abstract Groebner Bases and Some Applications in Z3 and RAHD.''
Here is a photograph!
Schloss Dagstuhl  Leibniz Center for Informatics
Dagstuhl, Germany
 INRIA/IRISA Team Celtique Seminar
April 2nd, 2010
I presented a talk (joint with Leo de Moura and Paul B. Jackson) titled ``Abstract Groebner Bases and Nonlinear Arithmetic in SMT.''
INRIA/IRISA Bretagne
Rennes, Bretagne, France
 Scottish Theorem Proving Seminar
November 20th, 2009
I presented a talk (joint with Leo de Moura) titled ``Recent Advances in SAT Modulo Nonlinear Real Arithmetic.''
University of Edinburgh,
Scotland, UK
 SYNASC 2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing)
September 26th  29th, 2009
I presented a talk (joint with Leo de Moura) titled ``Superfluous
Spolynomials in Strategyindependent Groebner Bases.''
West University, Timisoara, Romania,
RISC Linz, Johannes Kepler University, Austria, and
Research Institute eAustria Timisoara
Timisoara, Transylvania, Romania
 SMT 2009 (SATisfiability Modulo Theories)
colocated with CADE 2009 (Conference on Automated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``On Locally
Minimal Nullstellensatz Proofs.''
McGill University
Quebec, Montreal, Canada
 ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability)
colocated with CADE 2009 (Conference on Automated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``Universality of
Polynomial Positivity and a Variant of Hilbert's 17th
Problem.''
McGill University
Quebec, Montreal, Canada
 Calculemus 2009: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning
July 7th, 2009
I presented a talk (joint with Paul B. Jackson) titled ``Combined Decision Techniques for the Existential Theory of the
Reals.''
Work appears in the book ``Intelligent Computer Mathematics'' published by SpringerVerlag.
Grand Bend, Ontario, Canada
 MSR Internship Final Talk
June 26th, 2009
I presented a talk titled ``Some Results on Nonlinear Arithmetic Helpful to Z3.''
The results covered can be found in two joint papers by Leo de Moura and myself:
 ``On Locally Minimal Nullstellensatz Proofs'' (in SMT2009; pdf),
 ``Superfluous Spolynomials in StrategyIndependent Groebner Bases'' (in submission; pdf).
Microsoft Research Redmond
Redmond, WA, USA
 Verification Working Group
April 16th, 2009
I presented a talk titled ``A Highlevel Sketch of the RAHD (`Real Algebra in High Dimensions') Decision Method.''
See here for an abstract of my talk.
Microsoft Research Redmond
Redmond, WA, USA
 Workshop on Linking Formal Design and Verification Tools to
Create Trustworthy Software
Nov 2728th, 2008
I presented two posters (both joint with Paul Jackson):
Microsoft Research Cambridge
Cambridge, England, UK
 SRI Computer Science Laboratory Seminar
October 30th, 2008
I presented a talk titled ``RAHD: A Feasible Decision Method for Real Algebra in High Dimensions.''
See here for an abstract of my talk.
SRI International
Menlo Park, CA, USA
 Summer School Marktoberdorf 2008  Engineering Methods and Tools for Software Safety and Security
August 517th, 2008
An Advanced Study Institute of the NATO Science for Peace and Security Programme, and
The Institut für Informätik, Technische Universitat München
Marktoberdorf, Germany
 SRI Formal Methods and Dependable Systems Group Talk
I presented a talk titled ``Decision Methods for the Existential Theory of Real Closed Fields.''
June 27th, 2008
SRI International
Menlo Park, CA, USA
 Formal Methods Outreach Workshop
June 910th, 2008
SRI International
Menlo Park, CA, USA
 CAMELEON  CambridgeLeedsNorwich Logic and Set Theory Meeting
April 23rd, 2008 (a postaction shot!)
I presented a talk titled ``A Family of Decidable Nonlinear Fragments of the True Existential Theory of the Rational Number Field.''
Centre for Mathematical Sciences
Department of Pure Mathematics and Mathematical Statistics
University of Cambridge
Cambridge, England, UK
 BCTCS2008  24th British Colloquium for Theoretical Computer Science
April 710th, 2008 (an action shot!)
I presented a talk titled ``Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field.''
Grey College at Durham University
Banquet at Durham Castle (pretty!)
Durham, England, UK
 TTVSI  A Festschrift in Honour of Prof. Michael J. C. Gordon FRS
March 2526th, 2008
Paul Jackson and I presented a short talk and poster on our joint work titled ``A Continuous Relaxation for Proving
Discrete
ACL2 Theorems over Real Closed Fields.''
The Royal Society
London, England, UK
 IDT Talk: Edinburgh Interdisciplinary Tea Seminar
March 17th, 2008
I presented a talk titled ``Isolating Decidable Nonlinear Fragments of Undecidable Number Theories.''
See here for more information.
Department of Informatics
University of Edinburgh
Edinburgh, Scotland, UK
 CAMELEON  CambridgeLeedsNorwich Logic and Set Theory Meeting
December 11th, 2007
Department of Mathematics
University of East Anglia
Norwich, England, UK
 ACL2 Theorem Prover Workshop 2007
November 1516th, 2007
Matt Kaufmann, Jacob Kornerup, and Mark Reitblatt presented a ``Rump Session'' talk on
our joint work centered around using the ACL2 theorem prover to prove properties of
programs written in the graphical parallel dataflow programming language LabVIEW/G.
Jeff Kodosky, the inventor of LabVIEW and founder of our theorem proving project, gave
a Keynote Address on his vision for the future
of our project.
Note: I was sadly not able to be there in person.
Colocated with FMCAD2007
Austin, TX, USA
 DReaM Talk: Edinburgh Mathematical Reasoning Group
October 5th, 2007
I presented a talk titled ``Hilbert's Tenth Problem and Some Weak Relatives.''
See here for an abstract of my talk.
Mathematical Reasoning Group
University of Edinburgh
Edinburgh, Scotland, UK
 MAP (Mathematics: Algorithms and Proofs)
January 812th, 2007
The Lorentz Center
Universeteit Leiden
Leiden, The Netherlands
 CAMELEON CambridgeLeedsNorwich Logic and Set Theory Meeting and CL Minicourse on Countable Ordinals
November 29th  December 2nd, 2006
Center for Mathematical Sciences, and
Computer Laboratory
University of Cambridge
Cambridge, England, UK
 PSSL84 (Peripatetic Seminar on Sheaves and Logic)
October 1415th, 2006
Institut fur Theoretische Informatik
Technical University of Braunschweig
Braunschweig, Germany
 Association for Symbolic Logic Annual Conference
Special Goedel Centennial Meeting
May 1721st, 2006
Universite du Quebec a Montreal
Montreal, Quebec, Canada
 N.I.TECH  National Instruments Corp. Annual Technical Conference
April 7th, 2006
Dr. Jacob Kornerup and I presented a talk titled ``How LabVIEW and its Theorem Prover Help You Build Absolutely Reliable Systems.''
National Instruments Corporation  Main Campus
Austin, TX, USA
 College of Natural Sciences' Undergraduate Research Forum
April 7th, 2006
I presented my work titled ``Proof Theory in Proof Theory: A Computational Relativisation of Hilbert's Program.''
Under the auspices of the Department of Computer Sciences and the Department of Mathematics
College of Natural Sciences, Welch Hall Forum
University of Texas at Austin
Austin, TX, USA
 Arizona Winter School in Computational and Algorithmic Aspects of Algebra and Arithmetic
March 11th15th, 2006
Special courses in:  integer factorization,
 explicit methods for solving Diophantine equations,
 computing cohomology in algebraic geometry,
 and discriminants, resultants, and their tropicalization.
Southwestern Center for Arithmetical Algebraic Geometry
University of Arizona
Tucson, AZ, USA
 Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL2006)
June 8th12th, 2006 Cancelled
I am on the programme committee. Click here for CfP.
Part of The International Computer Science Symposium in Russia (CSR2006)
St. Petersburg Department of Steklov Institute of Mathematics, &
Euler International Mathematical Institute
St. Petersburg, Russia
 UT Austin ACL2 Seminar
October 19th, 2005 (one day after my 22nd birthday!)
I presented a talk titled "Automated Reasoning in LabVIEW with the Method/ACL2 System."
A short abstract can be found here.
Dept. of Computer Sciences / ACL2 Group
University of Texas, Austin
Austin, TX, USA
 Argonne Workshop on Automated Reasoning and Deduction (AWARD2005)
August 1113, 2005
I presented a talk titled "Automated Reasoning in LabVIEW and Some Elementary Thoughts on Proof Theoretic Techniques for Automating Interpretability."
Mathematics and Computer Science Division
Argonne National Laboratory
University of Chicago
Chicago, IL, USA
 Topics in Graduate Mathematics: Summer Workshop in Proof Theory
June 6  June 17th, 2005
University of Notre Dame
Southbend, IN, USA
Group Photo!
 Austin Center for Advanced Studies Annual Conference
April 2005
IBM Austin Center for Advanced Studies
Austin, TX, USA
 Association for Symbolic Logic Annual Conference
March 2005
Stanford University
Palo Alto, CA, USA
 Association for Symbolic Logic Annual Conference
May 2004
Carnegie Mellon University
Pittsburgh, PA, USA
Reviewing and Professional Service
Publicity and Web Chair
 International Conference on Automated Deduction (CADE2013)
Reviewing: Journals and Books
 Annals of Mathematics and Artificial Intelligence (2014)
 Theoretical Computer Science (2013)
 ACM Transactions on Mathematical Software (2012, 2013)
 Journal of Automated Reasoning (2009, 2011, 2012)
 International Journal of Computer Science and Technology (2012)
 Journal of Symbolic Computation (2011)
 New Computational Paradigms (2007)
Reviewing: Conferences and Workshops
 ‹PC› International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC2015)
 ‹PC› Conference on Intelligent Computer Mathematics (CICM2015)
 ‹PC› Conference on Intelligent Computer Mathematics (CICM2014)
 ‹PC› International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC2014)
 International Symposium on Symbolic and Algebraic Computation (ISSAC2013)
 International Conference on Automated Deduction (CADE2013)
 ‹PC› International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS2013)
 ‹PC› International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC2013)
 NASA Formal Methods Symposium (NFM2013)
 International Colliquium on Automata, Languages and Programming (ICALP2013)
 International Conference on Formal Engineering Methods (ICFEM2012)
 ‹PC› International Symposium on Symbolic and
Numeric Algorithms for Scientific Computing (SYNASC2013)
 ‹PC› Symposium on Integration of Symbolic Computation and Mechanised Reasoning (Calculemus2011)
 ‹PC› Computer Algebra in ComputerAided Design and
Verification (CAVCA2011)
 Formal Methods in ComputerAided Design (FMCAD2010)
 Symposium on Integration of Symbolic Computation and Mechanised Reasoning (Calculemus2009)
 Frontiers of Combining Systems (FRoCoS2009)
 Theorem Proving in HigherOrder Logics (TPHOLS2008)
 Computer Science Logic (CSL2008)
 ‹PC› Logic for Automated Reasoning and Automated Reasoning for Logic (LARARL2006)
 Logic for Programming Artificial Intelligence and Reasoning (LPAR2005)
Memberships in Professional Socieities
The Edinburgh Mathematical Society
The American Mathematical Society
The Mathematical Association of America
The Association for Symbolic Logic
The Association for Computability in Europe
The Computability and Complexity in Analysis Network
The Association for Automated Reasoning
The Association of Lisp Users
The Association for Advancement of Artificial Intelligence
Foundations of Mathematics (FOM)
Cambridge and Edinburgh
I am very lucky to be working in two of the most magical cities in the world. 
Cambridge, England photo by Kevin Allen  Edinburgh, Scotland photo by JuanJ (Flickr) 
Home Sweet Home
I grew up mostly upon the idyllic Oyster
Creek in Sugar Land, Texas.  
