Upcoming talks:

• Lawrence Paulson

Time: October 25, 4:30 PM – 6:30 PM

Previous talks:

• Marcelo Fiore

Time: 2022-10-18 16:30-18:30

Abstract:
In this talk, I will outline a mathematical theory for modelling, reasoning about, and computing with tree-like structures. Main application areas are to abstract syntax (the deep syntactic structure of formal languages) and to inductive data types
(inductively defined data structures). The lecture format will be introductory and intended to be interactive, developing theory as motivated by applications.

• Andrew Pitts

Time: 2022-09-29 16:30-18:30

Title: Programming Language Semantics

Abstract:  There are very many programming languages. They often arise to meet the needs of particular application areas, from numerical computing for scientific applications in the early days of computers to the need for user interaction within a web browser or phone app in the age of the internet.

A new programming language always arrives with an
implementation. Usually one also gets a precise mathematical
description of its grammar using well developed tools from formal
language theory, so one knows exactly what is, and is not, a legal
program in the language. One might also get an informal description of how programs are supposed to behave, written in natural language. But it is much rarer (and much harder) to have a precise mathematical description of the meaning of an arbitrary legal program, independent of any particular implementation. Indeed sometimes it can be hard to agree upon what “program meaning” should mean!

Computer scientists have devised various methods for precisely describing the semantics of programming languages, making use of various kinds of mathematics and logic, sometimes in ways that are unfamiliar to mainstream mathematics. In this talk I will survey some of these developments trying to be as non-technical as I can. We will look at various styles of programming language semantics and compare their answers to the fundamental question: when are two program
phrases semantically equivalent?

• Benedikt Löwe
  Wednesday the 27th of October, 4:00pm- 6:00pm GMT+8 (9:00am- 11:00am GMT+1)
  Title: Expert agreement in peer review and the epistemic exceptionality of mathematics

  Abstract: It is seen as one of the strengths of modern science that its findings are intersubjectively stable: two independent referees who check a scientific fact are expected to reach the same conclusion. This general principle translates into a highly normative belief that in scientific practice, experts should be expected to agree. While this agreement will not always be complete, especially in the experimental sciences, mathematics has been seen by some as an “epistemic exception” where complete agreement is possible.

  As a consequence, expert agreement has been used as a proxy for the intersubjectivity of judgments about scientific facts. In a famous paper with the exasperated subtitle “Is agreement between reviewers any greater than would be expected by chance alone?”, Rothwell & Martyn (2000) studied this agreement in the case of peer review. Alas, the answer to their question was negative. Geist, Löwe, & Van Kerkhove (2010) did a similar analysis for mathematics and theoretical computer science and obtained slightly higher agreement values than those found by Rothwell & Martyn, but not the very high values that would be expected if mathematics was indeed an epistemic exception.

  In this talk, we explore whether it is reasonable to expect that peer review agreement can be used as a proxy for intersubjectivity of agreement about scientific facts.

• • Maurice Chiodo,
    Monday the 11th of October, 4:30pm- 6:30pm GMT+8 (9:30am- 11:30am GMT+1)
    
    Title: Working through ethical issues in technology (Video).
     
    Abstract: Many of us have read, or heard, about some of the ethical issues arising from the use of mathematics in technical computer-based processes. But sometimes the cases we hear about (e.g.: “AI produces biased decisions in credit card applications”) might be very far from our own work on such technologies. So how do we, as technical developers, learn lessons from other cases and uses of technology so as to ensure our own research and output is done carefully and without creating harm?

    In this talk I will review some of the guidelines I gave in my previous talk on responsible and ethical development in technology. I will then invite members of the audience to briefly describe their own research and work, so that we can see how the guidelines might be applied in these examples, what sort of ethical issues could potentially arise, and how we might address these issues early in the development process so that they do not manifest as substantial problems later on.

• José Siqueira
  Wednesday the 29th of September, 7:00pm- 9:00pm GMT+8 (12:00pm- 2:00pm GMT+1)

Title: Tripos models of Internal Set Theory (Video)

Abstract: E. Nelson introduced Internal Set Theory (IST) to serve as syntax for the use of nonstandard proof methods, in contexts such as nonstandard analysis. The intent was to make the practical use of such ideas more accessible to those not acquainted with logic, particularly model theory, but there are advantages beyond that: using a set theory makes the subject more amenable to study through topos theory. This talk will discuss the possibility of developing something akin to IST for toposes other than that of sets, by using the notion of tripos.

• Lawrence Paulson
  Wednesday the 15th of September, 4:30pm- 6:30pm GMT+8 (9:30am- 11:30am GMT+1)The talk will split into two one-hour sections with a five-minute break between each section.
  
  Part I:  A Brief Survey of Type Theory (Video)Part I abstract: Type theory in the 20th century started with Russell’s ramified type theory and continued to simple type theory and then dependent type theory. In parallel, critiques of classical mathematics led to the development of constructive mathematics and in particular Heyting’s interpretation of the logical connectives, ideas made formal by Martin-Löf in his intuitionistic type theory. These developments will be outlined, as well as some issues with dependent types: the axiom of choice, equality and irrelevance of proofs. Techniques for formalising mathematics in the more elementary world of simple type theory are then surveyed.Part II: Formalised Mathematics: Obstacles and Achievements (Video)Part II abstract: The practice of formalising mathematics is starting to attract the attention of mathematicians themselves. The main motivation is an awareness that mathematicians regularly make serious errors, some of which go undetected. But is formalised mathematics at all a realistic possibility? By now a great body of mathematics has been formalised. Unfortunately, hardly any of it approaches the sophistication of modern research mathematics. Moreover, formalised proofs are typically unreadable and require lengthy blocks of code to prove obvious facts. Researchers are now formalising more advanced mathematical concepts, but much more remains to be done.
• Zohreh Shams
  Monday the 26th of July, 4:00pm- 6:00pm GMT+8 (9:00am- 11:00am GMT+1)
  Title: Formality and Accessibility in Ontology Representation and Reasoning: A Diagrammatic Approach (Video)
  Abstract:  Ontologies are often developed and used by a diverse range of stakeholders and domain experts with different levels of familiarity with symbolic notations that ontologies are expressed in. In order to make these notations accessible to all stakeholders, the ontology community has relied on  visualisation and diagrammatic notations.  However, due to lack of formality, these visualisations are often used only for ontology representation, but do not deal with ontology reasoning, which is essential for harnessing the full benefit of using ontologies.  To address this shortcoming, our novel work shows how to enable reasoning in an existing fully formalised diagrammatic language, namely Concept Diagrams (CD), that is designed for visualising and specifying ontologies. We unify diagrammatic representation and reasoning for ontologies for the first time. Furthermore, we put the accessibility of reasoning at the forefront by conducting extensive empirical studies that guide the design and implementation of iCon, a reasoning engine for ontology engineering.  In addition to accessibility, we evaluate the theoretical aspects of our approach as well as show its domain independence and generality for use in real world applications.

• Thomas Forster (Queens’ College and DPMMS, Cambridge)
  Monday the 12th of July, 1:00pm- 3:00pm GMT+8 (6:00am- 8:00am GMT+1)
  Title: Unfoldings (Slides, Video)
  Abstract: It’s almost a slang term, but there are many ideas of unfoldings in Mathematics.  Perhaps the most straightforward is the topological idea of a universal cover, but there are discrete versions as well, and they crop up in Possible World Semantics, Formal Language Theory, BQO Theory and in Randall Holmes’ proof of the consistency of Quine’s NF.  In this introductory survey I shall try to tie these various ideas together and see what the core ideas are.

• Huw Price
  Wednesday the 30th of June, 2:00pm-4:00pm GMT+8 (7:00am- 9:00am GMT+1)
  

Title: What Ramsey Got Right (Video)
Abstract: In his late paper ‘General propositions and causality’ (1929) Ramsey articulates what seems to be a version of the principle that deliberation crowds out prediction (DCoP), saying that our present action is “an ultimate and the only ultimate contingency”. He links this to the direction of causation, and to the fact that we take the future to be open but the past fixed. I will discuss what I take to be right and important about Ramsey’s proposal, and link it to the puzzling stand off between friends and enemies of DCoP.

• Anuj Dawar
  Monday the 21st of June, 4:30pm- 6:30pm GMT+8 (9:30am- 11:30am GMT+1)
  Title: The Limits of Symmetric Computation (Slides, Video)
  Abstract: The most famous open problem in theoretical computer science, known as the P vs. NP problem challenges us to prove that for some natural search problems, no efficient algorithm is possible.  At the moment, we have no idea how to prove such a statement.  In order to make meaningful progress, we can restrict the class of algorithms we consider and show that, within these restrictions, no efficient algorithm exists.  In this talk, I consider a natural restriction to symmetric algorithms.  I explain how symmetries arise naturally in computational problems and why algorithms that respect these symmetries have inherent limitations.  Many of our most powerful algorithmic techniques are symmetry-preserving, while others are not. Exploring these limits offers a rich research agenda combining logic, algebra and combinatorics with algorithms.
• Maurice Chiodo
  Monday the 7th of June, 4:30pm- 6:30pm GMT+8 (9:30am- 11:30am GMT+1)

Title: Ethical issues in mathematical processes (Video)

Abstract: Mathematics is used in a variety of technical computer-based processes, including AI, and decentralized ledgers (blockchain). The choice – the human choice – of what mathematics to use, and how to use it, plays an integral part in determining the impact these technologies have on people, on society, and on the world around us. In this regard, mathematics is highly “de-abstracted” and given a very real and tangible use.