Skip to main content

Professor Ursula Martin CBE FREng FRSE DSc 

Ursula Martin retired in January 2023. She is Professor Emerita at the University of Edinburgh, Emeritus fellow at Wadham College Oxford, a Distinguished Honorary Fellow of the Department of Computer Science and Technology at the University of Cambridge, and a Visiting Professor in both the School of Mathematics of the University of St Andrews, and the Mathematical Institute of the University of Oxford.

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,  and an Honorary Fellow of Royal Holloway University of London,  She holds a PhD and MSc from the University of Warwick,  and an MA and BA from the University of Cambridge.  

From 2014 to 2023 she held a UKRI/EPSRC Established Career Fellowship, "The social machine of mathematics", initially as a member of the Computer Science Department and Mathematical Institute of the University of Oxford (2014 - 2018), and subsequently as a member of the School of Informatics of the University of Edinburgh (2018-2023).  

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 (2003 - 2013). She was Vice-Principal for Science and Engineering (2005 - 2009),  and Director of the impactQM project (2009-2012),  an innovative knowledge transfer initiative which was a finalist in the Times Higher Education Awards.  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 re-orient her research to mitigate the long-term consequences  of extended chemotherapy. She was a Professor at the University of St Andrews (1992 - 2002), where she was the second female professor in any discipline since its foundation in 1411, the first having been appointed in some fifty years before. Earlier she was at Royal Holloway University of London (1985 - 1992), appointed in 1990 the University of London's first female professor of computer science, and before that held appointments at Manchester;  and Urbana Champaign.  

Throughout her career she was involved in many activities for women in science,  including: establishing the pioneering Women@CL project at the University of Cambridge; serving on the UK Royal Society's Diversity Committee and chairing ACM-W, the Committee on Women of the ACM; and leading research and outreach based on the mathematics of Ada Lovelace.  Numerous national roles included the UK Defence Science Advisory Council,   the 2001 and 2008  UK HEFCE Research Assessment Exercise Panels for Computer Science,  and the UKRI'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,  broadened to encompass wider social and cultural approaches to understanding the circulation and impact of foundational research in computer science and mathematics. 

EPSRC Fellowship, the Social Machine of Mathematics

The purpose of this UKRI/EPSRC Fellowship, 2014 - 2023, was to investigate cultures of mathematics viewed as a so-called "Social machine", an over-arching framework for considering human-machine collaboration. The resulting highly interdisciplinary portfolio of work drew on philosophy, social science, ethnography  and history, alongside computer science research in artificial intelligence, argumentation theory and verification.  

A particular focus was career development for postdocs, whose destinations included: Joe Corneli (Oxford Brookes), David Dunning (University of Pennsylvania), Chris Hollings (University of Oxford), Lorenzo Lane (UK government), Lee Macdonald (Greenwich Observatory), Jess Meagher (Royal Collection Trust), Alison Pease (University of Dundee), Gabriela Rino-Nesin (University of Brighton), Brigitte Stenhouse (University of Toronto), Máté Szabó (University of Greenwich), Fenner Tanswell (Technische Universität Berlin), Jacob Ward (University of Maastricht).  

A landmark event was Big Proof , a major programme at the Cambridge Newton Institute in Summer 2017, which is  credited with shifting the dial on how mathematicians think about using computation in proof. Other workshops included:  Group knowledge and mathematical collaboration  7-8 April 2017, Oxford Mathematics;  Enabling mathematical cultures  5-7 December 2017, Oxford Mathematics;  Mathematical Collaboration II St Andrews 7-8 April 2018, and Big Proof II  27-31 May 2019, ICMS Edinburgh.

EPSRC Fellowship: Impact

Mathematics policy and the impact of mathematics 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. The work was cited in a number of submissions to the 2017 HEFCE consultation on the REF, and in the 2019 Bond Review on Mathematics Knowledge Transfer, which led a substantial uplift in UK mathematics funding.

Collaborations with Libraries and Museums led to four public engagement projects, and a UKRI Impact Case Study, as described at the links:

  • The mathematics of Ada Lovelace, 2015-2021, including a popular book, highly cited journal papers, museum displays in the UK and USA,  a conference, numerous public talks, and collaborations with composers. The work was submitted as an Impact Case Study for the 2021 UK Research Excellence Framework. 
  • Oxford's female computing pioneers, 2020, a series of oral history interviews by Georgina Ferry, archived in Oxford's Bodleian Library.
  • Imagining AI, 2022, including a workshop, displays at the Bodleian Library and the History of Science Museum, and bespoke video of the Jevons "Reasoning piano". A much larger display had originally been planned, but could not go ahead because of the pandemic.
  • Archiving Babbage 2022, the cataloguing, digitisation and dissemination of MSS Buxton, manuscripts of Charles Babbage collected by Harry Wilmot Buxton and now held in Oxford's History of Science Museum.

EPSRC Fellowship: Main research themes

Mathematical collaboration online  Online collaboration captures informal processes that are  normally not recorded. A variety of quantitative and qualitative  techniques were used to investigate the PolyMath projects, and the MathOverflow Q&A site,  to understand what's involved in developing a  proof, and the fit with the model provided by social machines.

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

Philosophy and mathematical practice The "Polymath" online mathematical collaborations were used as an evidence base for understanding mathematical practice, in particular to assess notions of explanation in mathematics. Fenner Tanswell works on the connection between formal and informal proofs 

  • Alison Pease, Andrew Aberdein, Ursula Martin, 2019, Explanation in mathematical conversations: An empirical investigation, Philosophical Transactions of the Royal Society A 377 Uses analysis of a polymath conversation as an evidence base to assess 9 hypotheses, drawn from the philosophical literature, about mathematical explanation 
  • Lorenzo Lane, Ursula Martin et al, 2019, Journeys in mathematical landscapes: genius or craft? Proof Technology in Mathematics Research and Teaching (Springer) 197-212 Explores craft as a metaphor for creating mathematics
  • Fenner Tanswell 2018 Conceptual engineering for mathematical concepts Inquiry 61, 881-913
  • Fenner Tanswell 2017 Playing with LEGO® and Proving Theorems, LEGO® and Philosophy: Constructing Reality Brick by Brick, 217-226
  • Fenner Tanswell 2016 Saving proof from paradox: Gödel’s paradox and the inconsistency of informal mathematics , Logical Studies of Paraconsistent Reasoning in Science and Mathematics, 159-173
  • Fenner Tanswell 2015 A Problem with the Dependence of Informal Proofs on Formal Proofs  Philosophia Mathematica 23, 295-310

The early roots of contemporary mathematical and computational practices 

  • David Dunning, 2023, George Boole and the ‘Pure Analysis’ of the Syllogism. 2023 In Aristotle’s Syllogism and the Creation of Modern Logic: Between Tradition and Innovation, FGHI–FKLI, eds. Lukas M. Verburgt and Matteo Cosci.  Bloomsbury Academic.
  • David Dunning, 2021, The Work of Writing Programs: Logic and Inscriptive Practice in the History of Computing, IEEE Annals of the History of Computing 25, 27-42
  • David Dunning, 2021, The Logician in the Archive: John Venn’s Diagrams and Victorian Historical Thinking. Journal of the History of Ideas 82, 593-614
  • David Dunning,  2020, Always Mixed Together’: Notation, Language, and the Pedagogy of Frege’s Begriffsschrift. Modern Intellectual History 17 (1099-1131)
  • Máté Szabó et al (2023). How Computers Entered the Classroom in Hungary: A Long Journey from the Late 1950s into the 1980s. In Flury C, Geiss M (Ed.), How Computers Entered the Classroom, 1960–2000: Historical Perspectives. Oldenbourg:De Gruyter
  • Máté Szabó (2021). Péter on Church’s Thesis, 17th Conference on Computability in Europe, CiE 2021, Springer (pp. 434-445).
  • Máté Szabó (2021). From the West to the East and Back Again: Hungary's Early Years in the Ryad. IEEE Xplore Digital Library,
  • Máté Szabó (2020). Alonzo Church Tihanyban. Érintö, Elektronikus Matematikai Lapok
  • Jacob Ward, 2020, Computer Models and Thatcherist Futures: From Monopolies to Markets in British Telecommunications, Technology and Culture 61 (843-870)
     

The nature of mathematical collaboration, an ethnographic approach These careful ethnographic studies at mathematics research institutes looked at the activities of mathematicians as they collaborated in person, and identified a variety of processes for generating shared knowledge 

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

Research in verification, logic and algebra

2003 onwards, computational 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. Significant papers include:

  • 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. Significant papers include:

  • 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. Significant papers include:

  • 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. Significant papers include: 

Research assistants, graduate students and co-authors 1983-2023  Andrew Aberdein, Andrew Adams, Rob Arthan, Richard Boulton, Muffy Calder, Adam Cichon, Dave Cohen, Victoria Coleman, Joe Corneli, Nick Cropper, Jeremy Dick, David Dunning, Martin Dunstan, Hanne Gottliebsen, Ruth Hardy, Geir Helleloid, Chris Hollings, John Kalmus, Tom Kelsey, Mike Lai, Lorenzo Lane, Olga Lightfoot, Steve Linton, Athen Ma, Lee Macdonald, Erik Mathiesen, Laura Meagher, Natasa Milic-Frayling, Bill Mitchell, Hanan Mohammed, Dave Murray-Rust, Kathy Norrie, Tobias Nipkow, Paulo Oliva, Sam Owre, Alison Pease, Peter Prohle, Adrian Rice, Gabriela Rino-Nesin, Elizabeth Scott, Brigitte Stenhouse, Tim Storer, Duncan Shand, Máté Szabó, Fenner Tanswell, Jacob Ward, Phil Watson, Jeannette Wing.

 

Back to Top