Invited Talks

Anuj Dawar Lower Bounds for Symmetric Algebraic Circuits

Algebraic circuits (also known as arithmetic circuits) are a model for computing polynomial functions over an arbtrary field. Valiant's conjecture that VP is different from VNP is sometimes called an algebraic analogue of the conjecture that P is different from NP and has been an open question for nearly as long. It amounts to showing that algebraic circuits for computing the permanent of a matrix are necessarily of super-polynomial size. We are able to show lower bounds on circuits computing the permanent when restricted to certain symmetry conditions. With a natural notion of symmetry, this gives an exponential separation between the size of circuits computing the permanent and those computing the determinant. The result is sensitive to the choice of symmetries considered.
In this talk, I give a general introduction to algebraic circuits and Valiant's conjecture. I explain and motivate the symmetry restrictions and explore the lower bounds that can be established. I also give an overview of the proof methods, which bring together combinatorial techniques with methods from finite model theory.

Cecilia Pradic How unconstructive is the Cantor-Bernstein theorem?

Based on joint work with Chad Brown [1] and [2].
The Cantor-Bernstein theorem states that sizes of sets can be compared meaningfully using injections: if A injects into B and vice-versa, A and B are in bijection. This is typically proven via an explicit construction that does not involve choice, but the proof cannot be constructive. For instance, [0,1] and (0,1) can be embedded into one another but are not homeomorphic, meaning that Cantor-Bernstein is violated in a number of models of intuitionistic set theory. Faced with this state of affairs, we can still ask: how bad it is?
First, we are going to see how Cantor-Bernstein implies full excluded middle. We will then turn our attention to the Myhill isomorphism theorem, a constructive version of Cantor-Bernstein that states that, for any two subsets A, B ⊆ ℕ that are inter-reducible via injections, there is a bijection ℕ → ℕ that preserves them. The theorem remains true classically if ℕ is replaced by an arbitrary set X, but this is not the case constructively. Bauer asked if there is a nice class of sets X for which it does hold constructively. After checking there is no hope for this class of sets to be closed under basic operations like disjoint unions, we will see that a version of this generalized Myhill isomorphism theorem holds for the conatural numbers ℕ∞ by adapting the usual back-and-forth construction and assuming Markov's principle. However, this does not extend much: this fails for 2× ℕ∞, ℕ + ℕ∞ as well as Cantor space. We are going to see why those failures are of different flavours, and sketch how to make this could be made more precise by using oracle modalities.

1. Pradic, C. and Brown, C. E. 2022. Cantor-Bernstein implies Excluded Middle. arXiv preprint arXiv:1904.09193. Retrieved from https://arxiv.org/abs/1904.09193
2. Pradic, C. 2025. The Myhill isomorphism theorem does not generalize much. arXiv preprint arXiv:2507.05028. Retrieved from https://arxiv.org/abs/2507.05028

Nobuko Yoshida Multiparty Session Types: Separation and Encodability Results

The talk first introduces the history and background of types for communications and multiparty session types, relating to the history of Computer Science in Oxford.
Multiparty session types (MPST) are a type discipline for enforcing the structured, deadlock-free communication of concurrent and message-passing programs. Traditional MPST have a limited form of choice in which alternative communication possibilities are offered by a single participant and selected by another. Mixed choice multiparty session types (MCMP) extend the choice construct to include both selections and offers in the same choice. This talk presents a mixed choice synchronous multiparty session calculus and its typing system, which guarantees communication safety and deadlock-freedom. We then talk expressiveness of nine subcalcli of MCMP-calculus by examining their encodability (there exists a good encoding from one to another) and separation (there exists no good encoding from one calculus to another). The highlight is the binary (2-party) mixed sessions by Casal et al (2022) is strictly less expressive than the MCMP-calculus.
A joint work with Kirstin Peters appeared in LICS'24 (https://arxiv.org/abs/2405.08104)

About the speaker:
Nobuko Yoshida is Christopher Strachey Chair of Computer Science in University of Oxford. She is an EPSRC Established Career Fellow and an Honorary Fellow at Glasgow University. Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [POPL'08, JACM] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas. She received the Test-of-time-award from PPDP'24 and the best paper awards from CC'20, COORDINATION'23, DisCoTech'23 and ECOOP’23. She received the third Suffrage Science Awards for Mathematics and Computing from MRC for her STEM activity. She is an editor of ACM Transactions on Programming Languages and Systems, Theoretical Computer Science, ACM Formal Aspects of Computing, Mathematical Structures in Computer Science, Journal of Logical Algebraic Methods in Programming, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin.

Milly Maietti Constructivity, computability and continuity relative to the Minimalist Foundation (Tutorial)

Abstract:

Issues regarding constructivity, computability, and continuity are inevitable when developing a foundation for constructive mathematics, i.e., mathematics where the underlying logical reasoning has computational contents, sets are meant as data types, and the existence of objects is shown by construction.

This tutorial aims to describe solved or still open issues of constructivity, computability, and continuity related to the Minimalist Foundation, for short MF, for constructive mathematics ideated in joint work with Giovanni Sambin in [8] and completed in [3].

First Lecture: Regarding constructivity, the Minimalist Foundation provides a solution to the problem of finding a core foundation among the most relevant constructive and classical ones, often mutually incompatible between each other, including Martin-Loef's type theory, Aczel's constructive set theory, the Calculus of Constructions, the internal theory of a topos, all shown in [3] and, finally, with Homotopy Type Theory, shown in [1]. To better achieve such a compatibility, MF is equipped with a two-level system, comprising an intensional level, an extensional one, and an interpretation of the latter on the former. Furthermore, MF distinguishes itself for being a predicative constructive foundation compatible with classical predicative mathematics a' la Weyl, especially for the treatment of the continuum. The key point is that the constructive MF has been shown in [7] to be equi-consistent with its classical version, a feature not shared by the other above-mentioned predicative foundations.

Second Lecture: Regarding computability, both levels of MF and its two-level extensions with inductive and coinductive definitions enjoy models validating the Formal Church thesis, where proofs can be seen as programs as devised in [2],[5],[6]. The key point is that such models are obtained by extending the usual Kleene realizability of intuitionistic arithmetic. They show that the intensional level of MF and its extensions are consistent with the axiom of choice, together with the Formal Church thesis, a property not shared by foundations validating extensionality of functions. Such realizability models provide the basic structure to build predicative effective toposes a' la Hyland, as in [4], where to interpret the extensional level of MF and extensions.

Regarding continuity, MF opens the way to reconcile Markov's constructivism with Brouwer's intuitionism. The key point is the presence in MF of a primitive notion of function described by lambda-terms distinct from the usual notion of functional relation, used to interpret lawlike computable sequences and Brouwer's choice sequences, respectively. As a consequence, MF has the peculiar property of being consistent with Brouwer's continuity principles (which imply that all functions between real numbers are continuous) and Church's thesis restricted to lambda-functions.

[1] M. Contente and M. E. Maietti. The compatibility of the Minimalist Foundation with Homotopy Type Theory. Theor. Comput. Sci., 2024.
[2] H. Ishihara, M. E. Maietti, S. Maschio, T. Streicher. Consistency of the intensional level of the Minimalist Foundation with Church's thesis and axiom of choice. Arch. Math. Log., 2018
[3] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Ann. of Pure and Applied Logic, 2009
[4] M. E. Maietti, S. Maschio: A Predicative variant of Hyland's Effective Topos. J. Symb. Log. 2021
[5] M. E. Maietti, S. Maschio, M. Rathjen: A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice. Log. Methods Comput. Sci., 2021
[6] M. E. Maietti, S. Maschio, M. Rathjen: Inductive and Coinductive Topological Generation with Church's Thesis and the Axiom of Choice. Log. Methods Comput. Sci., 2022
[7] M. E. Maietti and P. Sabelli. Equiconsistency of the Minimalist Foundation with its classical version. Ann. of Pure and Applied Logic, 2024
[8] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48, OUP, 2005.

Special Session

Jens Blanck A Domain Theoretical Understanding of the iRRAM

The iRRAM is a successful implementation of Exact Real Arithmetic. We will look at the implementation from a domain theoretic perspective and at some of the important choices made in its implementation.

Pieter Collins Exact Real Computation and the iRRAM

One of the main goals of research into computable analysis is to develop tools for real number computation which are both exact and efficient. Norbert Müller's iRRAM, originating from the mid 1990s, was the first system to do just this, and is still competitive today. In this talk, I'll look at the development of iRRAM and perspectives for the future of exact real computation.

Michal Konečný Multi-Valued Limits in iRRAM and cAERN

Some real-valued problems are only computable as non-deterministic functions. For example, the complex square root is not computable as a function but it is computable as a multi-valued function that returns one of the two roots non-deterministically. Moreover, the non-deterministic result is sometimes computed as a limit: The terms of the limit are non-deterministic and yet converge to one of the possible valid results.
I recall and contrast the multi-valued limit operators provided by iRRAM, AERN and cAERN. Each has some subtle aspects that require careful description. In summary, the iRRAM version is more efficient, the AERN version is simpler, and cAERN provides a way to formally verify uses of the AERN multivalued limit. cAERN’s multivalued dependent choice axiom is similar to iRRAM’s mechanism for achieving convergence of a multivalued limit.
(Joint work with Sewon Park and Holger Thies)

Dieter Spreen Computing with Compact Sets

In collaboration with U. Berger, a general framework was presented for extracting algorithms that compute on elements of compact metric spaces and their compact subsets from proofs in a many-sorted intuitionistic first-order predicate logic, extended by strictly positive inductive and coinductive definitions. The approach is computationally equivalent to Weihrauch's type-two theory of effectivity. Unlike this approach, however, it is purely logical and representation-free. Representations of the computed objects are obtained via a realizability interpretation of the logic. Note that although the logic is fundamentally intuitionistic, much of classical logic is nevertheless available: any genuine disjunction-free formula can be used as an axiom.
In this talk, we discuss the mathematical framework introduced for the treatment of elements and nonempty compact subsets of compact metric spaces in formal logic. Furthermore, we present a generalization of Berger's nested coinductive inductive characterization of uniformly continuous functions of the unit interval to the general case of compact metric spaces. This characterization enables the treatment of (constructively) uniformly continuous functions in the aforementioned first-order logical calculus and the derivation of programs for computing such functions. We re-prove some well-known results in metric space theory based on the characterization. The proofs now use coinduction and induction in a nested manner and differ significantly from the usual proofs of classical topology.