Skip to main content

Ursula Martin

Personal photo - Ursula Martin

Professor Ursula Martin CBE FREng FRSE

Professor of Computer Science

Room N 3.14, Mathematical Institute

Biography

Ursula Martin joined the University of Oxford as Professor of Computer Science in 2014.  She she holds an EPSRC Established Career Fellowship, as a member of the Mathematics Institute and the Department of Computer Science,  and is a Senior Research Fellow at Wadham College.  She is a Commander of the Order of the British Empire,  a Fellow of the Royal Academy of Engineering,  a Fellow of the  Royal Society of Edinburgh,  and also holds fellowships of the British Computer Society and the Institute of Mathematics and its Applications.  She is a Doctor of Science honoris causa of the University of London,  an Honorary Fellow of Royal Holloway University of London,  and holds a PhD and MSc from the University of Warwick,  and an MA and BA from the University of Cambridge.  She is also a Visiting Professor at the University of Edinburgh.

Before 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 UK Defence Science Advisory Council,  on the 2001 and 2008  UK HEFCE RAE panels for Computer Science,  and was a SICSA distinguished visitor at the University of Edinburgh for 2012-13.  Her career was interrupted for two years by ill-health,  and she is grateful to Queen Mary for their support during this time,  which enabled her to reorient her research to mitigate the long-term cognitive impact of chemotherapy.  She has previously held appointments at the University of St Andrews (the second female professor in any discipline since its foundation in 1411, the first having been appointed in some fifty years before);  Royal Holloway University of London;  Manchester;  and Urbana Champaign.  Throughout her career she has been involved in many activities for women in science,  most recently serving on the Royal Society's Diversity Committee,  and leading research and outreach based on the mathematics of Ada Lovelace.  She is involved in many aspects of science policy,  currently serving on HEFCE's Interdisciplinary Advisory Panel for the 2021 Research Excellence Framework.

Her research,  initially in algebra,  logic and the use of computers to create mathematical proofs,  now focuses on wider social and cultural approaches to understanding the success and impact of foundational research in computer science and mathematics. 

Current research, the Social Machine of Mathematics

Since 2014 her 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.

Project workshops included Group knowledge and mathematical collaboration 7-8 April 2017, and Enabling mathematical cultures 5-7 December 2017

Other Conferences and seminars

External presentations in 2018 will include: January: AMS Joint Mathematical meetings (History of computing; crowdsourced maths) February: University of Oxford History of Science Seminar (Victorian mathematics); April: University of Oxford  [Mathematics Institute, open lecture] (Launch of Ada Lovelace book);  June: British Mathematical Colloquium [keynote]; Mathematics and Patronage meeting  [keynote]; July: IEEE Logic in Computer Science Conference, Oxford [keynote]

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 [three open lectures]; Cambridge U3A (Ada Lovelace); Cambridge Computing History Centre (Ada Lovelace); December: Enabling Mathematical Cultures, 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 online mathematical collaborations 

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.

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 approach, with Lorenzo Lane.  

  • Lane, Lorenzo and Martin, Ursula 2015 Collaboration at the Isaac Newton Institute Report for the Isaac Newton Institute
  • Lane, Lorenzo 2017 Fixed performances in fluid publics, 5th Innovation in Information Infrastructures (III) Workshop
  • Lane, Lorenzo 2017 PhD thesis, University of Edinburgh

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 44: 202-231  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  Ada Lovelace: the making 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

Projects