Skip to main content

Ursula Martin

Personal photo - Ursula Martin

Ursula Martin CBE FREng FRSE

Professor of Computer Science

Room N 3.14, Mathematical Institute


Professor Ursula Martin CBE FREng FRSE joined the University of Oxford as Professor of Computer Science in 2014, and is a member of the Mathematical Institute.  She holds an EPSRC Established Career Fellowship, and a Senior Research Fellowship at Wadham College. Her research, initially in algebra, logic and the use of computers to create mathematical proofs, now focuses on wider social and cultural approchaes to understanding the success and impact of current and historical computer science research. 


Befre joining Oxford she held  a chair of Computer Science in the School of Electronic Engineering and Computer Science at Queen Mary University of London, where she was Vice-Principal for Science and Engineering (2005-2009), and Director of the impactQM project (2009-2012), an innovative knowledge transfer initiative. She served on the U K Defence Science Advisory Council, on the 2001 and 2008  UK HEFCE RAE panel for Computer Science, and was a SICSA distinguished visitor at the University of Edinburgh for 2012-13. Her career was interrupted by a two year period of chemotherapy and its aftermath, and she is grateful to Queen Mary for their support during this time.  She has previously held appointments at the University of St Andrews (the first female professor in any discipline since its foundation in 1411), Royal Holloway University of London, Manchester and Urbana Champaign. She holds an MA in Mathematics from Cambridge, and a PhD in Mathematics from Warwick. She was appointed a Commander of the Order of the British Empire in 2012, and a Fellow of the Royal Academy of Engineering, and of the Royal Society of Edinburgh,  in  2017. She is involved in many activities for women in science, and currently serves on the Royal Society's Diversity Committee. 

Current research, the Social Machine of Mathematics

Since 2014 my research has been supported by an EPSRC Fellowship, investigating cultures of mathematics to understand mathematics as as a social machine.  The resulting highly interdisciplinary portfolio of work, using philosophy, social scence and history alongside computer science research in artificial intelligence, argumentation theory and verification, shows the scope for new computer techniques to support concept formation and argument finding, while highlighting the roles that risk, doubt, error, explanation and group knowledge play in the human production and use of mathematics.  Current postdocs are Joe Corneli and Lorenzo Lane: former postdocs Chris Hollings (Oxford), Gabriela Nesin (Brighton), Alison Pease (Dundee) and Fenner Tanswell (St Andrews) have moved on to lectureships.

The project held a workshop on "Group knowledge and mathematical collaboration"  on 7 and 8 April 2017, and will hold a workshop on "Enabling mathematical cultures" on 5, 6 and 7 December 2017

Other Conferences and seminars

 External presentations in 2017 include: January: AMS Joint Mathematical meetings (Ada Lovelace), University of Waterloo [open lecture] (Ada Lovelace); University of Waterloo [Faulty of Mathematics] (Future of Proof); MIT (Mathematical practice); February: University of Kent (Future of Proof); University of Leicester (Ada Lovelace); University of Oxford [Mirzakhani Society] (women in mathematics) April: University of Oxford [Faculty of Philosophy] (Future of Proof); May: University of Oxford [Faculty of English] (Ada Lovelace); University of Oxford [Mathematics Institute, open lecture] (Hidden Figures of Oxford Computing);  Birkbeck London [Computer Science] (Future of Proof); June: CIE conference, Turku, Finland  [keynote]; University of Glasgow, 60th anniversary of Computer SCience Department [keynote]; July: Big Proof workshop, Isaac Newton Institute, Cambridge [keynote]; ICHSTM, Rio de Janiero [history of science] (Impact of mathematics); September: UK Mathematics Trust [school students] (Ada Lovelace); Malvern Girls College and nearby schools [school students]; St Anne's Caversham and nearby schools [school students]; October: University of St Andrews Distinguished Lectures in Computer Science [open lectures]; University of Oxford [Department of Computer Science] (Social machine of mathematics); Cambridge U3A (Ada Lovelace); Cambridge Computing History Centre (Ada Lovelace); December: Enabling Mathematical Cultures Conference, Oxford [keynote].  

Main research themes

Investigation of online mathematical collaboration  to understand how proof comes about, and the model provided by social machines, in particular looking at evidence from writings by mathematicians, and from study of the polymath online mathematical collaborations initiated by Terence Tao and Timothy Gowers

Modelling mathematical conversations with argumentation theory with Alison Pease and Joe Corneli  Social machines provide models for mathematical argument using argumentation theory and LSC - the lightweight social calculus.

  • Pease, Alison, Corneli, Joseph et al, 2017 Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation Artificial Intelligence 246, 181–219
  • Corneli, Joseph, Martin, Ursula, Murray-Rust, Dave and Pease, Alison, 2017 Towards mathematical AI via a model of the content and process of mathematical question and answer dialogues, in Intelligent Computer Mathematics, 10th International Conference, CICM 2017, Edinburgh, UK, 2017, Proceedings
  • Corneli, Joseph, Martin, Ursula, Nesin, Gabriela, and Pease, Alison 2017 Modelling polymath coversations in IAT,  in preparation  

Philosophy for mathematical practice with Andrew Aberdein, Alison Pease and Fenner Tanswell. We use the polymath online mathematical collaborations as an evidence base for understanding mathematical practice, in particular to assess notions of explanation in mathematics, with our most recent paper countering a number of assertions on explanation  in the philosophical literature.  Fenner Tanswell works on the connection between formal and informal proofs 

The nature of mathematical collaboration, an ethnographic appro ach , with Lorenzo Lane.  A report was written on collaboration at the Isaac Newton Institute and forms the basis of part of Lane's PhD thesis (University of Edinburgh 2016), with further papers in preparation, details on request. 

Mathematics policy and the impact of mathematics, with Laura Meagher. We use materials submitted for the 2014 Research Excellence Framework as an evidence base to assess the mechanisms by which mathematics has impact, highlighting the importance of interdisciplinarity, relationship building and the long term view.

  • Meagher, Laura R. and Martin, Ursula, 2017  Slightly dirty maths: The richly textured mechanisms of impact  Research Evaluation 26: 15-27 
  • Popular accounts appeared in Times Higher, London Mathematical Society Newsletter, and Mathematics Today magazine, and the work was cited in a number of submissions to the 2017 HEFCE consultation on the REF.

The mathematics of Ada Lovelace, with Christopher Hollings and Adrian Rice   In 2015 Ursula Martin organised Oxford's Ada Lovelace bicentenary celebrations, including collaborations with the Bodleian Library, BBC and various science museums. She curated an exhibition, now on display at the Silicon Valley Computer History Museum, and led the digitisation of Ada Lovelace's mathematics, with the support of the Clay Mathematics Institute. Numerous presentations included lectures at the Hay Festival, Computer History Museum and Gresham College. 

  • Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 Ada Lovelace, a mathematical childhood, Journal of the British Society for the History of Mathematics 2: 221-234 Covers Lovelace's education before 1840, which  encompassed older traditions of practical geometry, newer textbooks influenced by continental approaches, wide reading, and a fascination with machinery, and challenges earlier  judgements of her mathematical knowledge and skills which have impacted later scholarly and popular discourse. 
  • Hollings, Christopher; Martin, Ursula, and Rice, Adrian 2017 The Lovelace-De Morgan Mathematical Correspondence: A Critical Re-Appraisal, Historia Mathematica, online first May 2017  The first account by historians of mathematics of Lovelace's informal correspondence course with Augustus De Morgan. Detailed contextual analysis gives a corrected ordering of the archive material, and shows Lovelace learning good habits of study, a grounding in certain areas of higher mathematics, a critical attitude towards foundational principles, the ability to make perceptive mathematical observations, and exposure to ideas then current in British mathematical research. Contrary to earlier claims, Lovelace had the mathematical background for her famous 1843 paper, the potential for serious mathematical work.
  • Hollings, Christopher; Martin, Ursula, and Rice, Adrian, 2018 A da Lovelace: the education of a computer scientist , illustrated book to be published by the Bodleian Press
  • Popular accounts have appeared in London Review of Books, BBC Oxford, EPSRC Blog, EDGE 2017 questions, London Mathematical Society Newsletter, Mathematics Today magazine, CORE magazine (Computer History Museum)

Earlier research

2003 onwards, compuational logic for control  A totally novel “block diagram logic” was devised to solve a concrete problem raised by DSTL engineers, and then generalised to the abstract domain of traced monoidal categories. This showed that the new logic, and other results in computer science, are instantiations of this general concept; most strikingly Hoare’s logic of programs, devised in the 1960s, and the foundation of contemporary “industry standard” software verification. The paper received a “Best of 2013” award from the prestigious Computing Reviews journal. The pilot work was funded by QinetiQ, with subsquent funding from EPSRC.

  • Arthan, Rob, Martin, Ursula and Oliva, Paulo 2013 A Hoare Logic for linear systems Formal Aspects of Computing, 25, 345-363
  • Arthan, Rob, Martin, Ursula, Mathiesen, Erik and Oliva, Paulo 2009 A general framework for sound and complete Floyd-Hoare logics, ACM Trans on Computational Logic, 11, 1-12
  • Boulton, Richard, Gottliebsen, Hanne, Hardy, Ruth,  Kelsey, Tom and Martin, Ursula 2004 Design verification for control engineering, Integrated Formal Methods, Springer LNCS, 2999, 21-35 

1997 onwards, combining computational logic and computer algebra This was pioneering in developing new kinds of interface specifications for numerical libraries, which was extended to a new elegant solution to the problem of deficiencies in computer algebra systems, through using restricted calls to and from the Maple computer algebra system  to specialist logic algorithms, via a limited interface that shields the user from complexity. The pilot work was developed during a sabbatical at SRI, and subsequently through a collaboration with NASA, with additional funding  from EPSRC

  • Gottliebsen, Hanne, Hardy, Ruth,  Lightfoot Olga  and Martin, Ursula 2013 Applications of real number theorem proving in PVS, Formal Aspects of Computing, 25, 993-1016 
  • Gottliebsen, Hanne, Kelsey, Tom  and Martin, Ursula 2005 Hidden verification for computational mathematics, Journal of Symbolic Computation, 39, 539-567
  • Dunstan, Martin, Kelsey, Tom, Martin, Ursula and Linton, Steve 1998 Lightweight formal methods for computer algebra, ACM Proceedings on Symbolic and Algebraic Computation, 1998, 80-87

1990 onwards, Computer algebra and computational logic Early work included the first application of computational logic in group theory, obtaining results, at the time, well beyond the scope of standard techniques; novel unification algorithms inspired by group theory; and termination algorithms that provided a unified framework for understanding the diverse methods in use at the time.

  • Martin, Ursula and Scott, Elizabeth 1997 The order types of termination orderings on monadic terms, strings and multisets, Journal of Symbolic Logic, 62, 624-635 
  • Martin, Ursula  and Lai, Mike 1992 Some experiments with a completion theorem prover, Journal of Symbolic Computation, 13, 81-100
  • Dick, Jeremy, Martin, Ursula and Kalmus, John 1990 Automating the Knuth-Bendix ordering, Acta Informatica, 28, 95-119 
  • Martin, Ursula and Nipkow, Tobias 1989 Boolean Unification: the story so far, Journal of Symbolic Computation, 7, 275-293
  • Martin, Ursula 1989 A geometrical approach to multiset orderings, Journal of Theoretical Computer Science, 67, 37-54
  • Martin, Ursula and Nipkow, Tobias 1988 Unification in Boolean rings, Journal of Automated Reasoning, 4, 381-396 

1980 onwards, Group theory and combinatorics  Research in group theory, combinatorics, and graph theory, mainly concerning symmetries of structures. First published paper, in 1980, provided a novel simple proof of a famous result of Gaschütz: in 2007, with Helleloid at Stanford, showed random groups of certain kinds have very restricted symmetry, a result with powerful implications which is still regularly applied in other domains. 

Current research collaborators Andrew Aberdein, Joe Corneli, Chris Hollings, Lorenzo Lane, Laura Meagher,  Alison Pease, Adrian Rice, Gabriela Rino-Nesin, Fenner Tanswell

Former RAs, graduate students and co-authors  Andrew Adams, Rob Arthan, Richard Boulton, Muffy Calder, Adam Cichon, Dave Cohen, Victoria Coleman, Nick Cropper, Jeremy Dick, Martin Dunstan, Hanne Gottliebsen, Ruth Hardy,  Geir Helleloid, John Kalmus, Tom Kelsey, Mike Lai, Olga Lightfoot, Steve Linton, Athen Ma, Erik Mathiesen, Natasa Milic-Frayling, Bill Mitchell, Hanan Mohammed, Kathy Norrie, Tobias Nipkow, Paulo Oliva, Sam Owre, Peter Prohle, Liz Scott, Tim Storer, Duncan Shand, Phil Watson, Jeannette Wing.

Selected Publications

View AllManage publications