Department of Computer Science - University College London - Gower Street - London - WC1E
6BT - 
+44 (0)20 7679 7214 - Copyright © 1999-2025 UCL
Disclaimer: This page's design is cloned from the official page.
The PPLV group hosts an (approximately) weekly research seminar. Upcoming talks are listed on this page, and are open to any interested UCL student or staff member. An archive of past talks from 2018 to 2023 can be found here.
If you are interested in giving a research seminar, please contact Quang Loc Le in the first instance.
| Time / date: | December 5th 2025 / 1-2pm |
|---|---|
| Speaker: | Mina Abbaszadeh (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Compositional Concept Generalization with Variational Quantum Circuits |
| Abstract: | Compositional generalization is a key facet of human cognition, but lacking in current AI tools such as vision-language models. Previous work examined whether a compositional tensor-based sentence semantics can overcome the challenge, but led to negative results. We conjecture that the increased training efficiency of quantum models will improve performance in these tasks. We interpret the representations of compositional tensor-based models in Hilbert spaces and train Variational Quantum Circuits to learn these representations on an image captioning task requiring compositional generalization. We used two image encoding techniques: a multi-hot encoding (MHE) on binary image vectors and an angle/amplitude encoding on image vectors taken from the vision-language model CLIP. We achieve good proof-of-concept results using noisy MHE encodings. Performance on CLIP image vectors was more mixed, but still outperformed classical compositional models. |
| Time / date: | January 8th 2026 / 1-2pm |
|---|---|
| Speaker: | Moshe Y. Vardi (Rice University) |
| Homepage: | https://www.cs.rice.edu/~vardi/ |
| Location: | Seminar Room G01, 66-72 Gower Street |
| Title: | What Is Theoretical Computer Science? |
| Abstract: |
Wikipedia defines theoretical computer science (TCS) as “a subfield of
computer science and mathematics that focuses on the abstract mathematical
foundations of computation.” I will take issue with this definition.
I believe that thinking of TCS as a branch of mathematics is harmful to the discipline. The centrality of computing stems from the fact that it is a technology that has been changing the world for the past 80 years. As computer scientists, we should look for inspiration from physics rather than from mathematics. Theoretical physics is highly mathematical, but it aims to explain and predict the real world. Theories that fail at this “explain/predict” task would ultimately be discarded. Analogously, I will argue that the role of TCS is to explain/predict real-life computing. We should remember the warning of John von Neuman, one of the greatest mathematicians and computer scientists of the 20th century, regarding the danger of mathematics driven solely by internal esthetics: “There is a grave danger that the subject will develop along the line of least resistance.” I will use Boolean reasoning as the running example to illustrate this thesis. |
| Time / date: | December 1st 2025 / 1-2pm |
|---|---|
| Speaker: | Yoàv Montacute (University of Cambridge) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Logic of Space and Time |
| Abstract: | The search for a complete logic for dynamical systems, posed as an open problem by Kremer and Mints in the mid-2000s, has been a central challenge in the study of spatiotemporal modal logics. Using the Cantor derivative interpretation within the topological semantics of modal logic, we have established a complete logical framework for dynamical systems. The logic of dynamical systems includes a global temporal modality, which comes at the cost of undecidability. To address this, we introduce a topological fixed-point operator, retaining expressivity while restoring decidability. These advancements pave the way for efficient formal reasoning and verification techniques for dynamical systems. This talk will provide a brief overview of the research programme on logic and dynamical systems, along with its most recent developments. |
| Time / date: | November 27th 2025 / 1-2pm |
|---|---|
| Speaker: | Bruno Gavranović (University of Strathclyde) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | TensorType: Implementing and extending Deep Learning with Types |
| Abstract: |
Category theory has seen a rise in applications in deep learning, bringing with it ideas and tools from functional programming and dependent type theory. However, practical implementations of these ideas face significant friction. Successful neural network frameworks only exist in dynamically typed languages such as Python, and attempts to implement these ideas in statically-typed languages have struggled with expressiveness and ergonomics, typically only replicating what exists without imagining what can be.
In this talk, I will introduce TensorType, a tensor processing framework implemented in Idris 2 aiming to demonstrate that ergonomics and rigor need not be at odds. TensorType provides tensor operations checked at compile-time while enabling fundamentally new capabilities: tensors that branch and recurse instead of being confined to rectangular shapes. I will walk through the design choices behind TensorType, showcase how containers power its core abstractions, and explore strange new worlds it enables. |
| Time / date: | November 13th 2025 / 1-2pm |
|---|---|
| Speaker: | José Jeremías Valenzuela Morales (George Washington University) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Computable categoricity relative to the c.e. Turing degrees and beyond |
| Abstract: |
In the context of Model Theory, a complete theory in a countable language is $\omega-$categorical if it has exactly one model of cardinality $\omega$, up to isomorphisms. In a similar vein, given a Turing degree \textbf{d}, one may define the following property for computable structures: A computable structure $\mathcal{A}$ is computably categorical relative to \textbf{d} if for any \textbf{d}-computable copy $\mathcal{B}$ of $\mathcal{A}$, there exists a \textbf{d}-computable isomorphism between $\mathcal{A}$ and $\mathcal{B}$.
As the Turing degrees form a rich upper semilattice, it is of interest to know how well-behaved this property is for different types of degrees. In this talk, we will go over Downey, Harrison-Trainor, Slaman, and Melnikov's proof of the existence of a computable structure whose categoricity is nonmonotonic relative to an $\omega-$chain between $\emptyset$ and $\emptyset '$. Furthermore, we will employ the \textit{true stages} method to modify the original construction and open avenues for future research. |
| Time / date: | November 6th 2025 / 1-2pm |
|---|---|
| Speaker: | Alessandro Di Giorgio (University of Pisa) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Parametric Iteration in Resource Theories |
| Abstract: |
Many algorithms are specified with respect to a certain parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories—general calculi of processes with a string diagrammatic syntax— introducing a parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems – for instance, proving that guessing a randomly generated key has negligible success.
|
| Time / date: | October 30th 2025 / 1-2pm |
|---|---|
| Speaker: | Damian Arellanes (Lancaster University) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Algebraic Composition for Models of High-level Computation |
| Abstract: | Models of High-level Computation (MHCs) elevate the level of abstraction of their classical, low-level counterparts, aiming to describe not isolated computing devices but structured interactions among a collection of them. As interactions are defined through composition mechanisms, compositionality emerges as a fundamental property for the inductive construction of complex computing devices from simpler ones, without the need of delving into internal structures. In this talk, I will examine the role of algebraic composition in this context and introduce a category-theoretic framework that abstracts and generalises the core structural principles underlying composition. This framework provides a rigorous foundation for reasoning about MHCs via categorical colimits, offering a principled and unified perspective on compositional computation. | Bio: | Dr. Damian Arellanes is a full-time Lecturer in Computer Science in the School of Computing and Communications at Lancaster University, UK. He is a member of the Software Engineering group and a Fellow of the Higher Education Academy. Prior to joining Lancaster, he served as a Research Associate in the Department of Computer Science from the University of Manchester, where he obtained his PhD in 2020, specialising software compositionality. His research examines the theoretical foundations of algebraic composition for models of high-level computation, with particular emphasis on using categorical structures to reason about compositionality in the inductive modelling and construction of large-scale, complex computing systems. |
| Time / date: | October 23nd 2025 / 1-2pm |
|---|---|
| Speaker: | Ye He (University College London) |
| Location: | G08 Sir David Davies LT, Roberts Building |
| Title: | Knowledge Graphs + AI: The Evolution of Automated GitHub Issue Resolution |
| Abstract: | AI coding agents are getting smarter and achieving high accuracy in benchmarks such as SWE-bench, but most still struggle with real-world challenges such as issue reproduction, precise context retrieval from large codebases, and the high cost of LLMs. In this talk, I will introduce our recent code agent, Prometheus — a knowledge graph-powered, multi-agent system designed to tackle GitHub issues in practice. Prometheus transforms entire repositories into a unified knowledge graph, persisted in Neo4j for scalable and structured reasoning. This enables precise, cross-language context retrieval, allowing large language models to generate accurate and efficient fixes. Powered by the DeepSeek-V3 model, Prometheus delivers strong performance, resolving unique issues across seven programming languages. I will show how combining LLMs with knowledge graphs can advance automated issue resolution beyond today’s benchmark-driven limits. We have recently transformed our research into an off-the-shelf product to help industry resolve software issues automatically. |
| Bio: | He Ye is an Assistant Professor at University College London. She previously worked as a Postdoctoral Researcher at Carnegie Mellon University and received her PhD from KTH Royal Institute of Technology. Her research centers on developing the next generation of code agents to automate software engineering tasks, with a focus on codebase context retrieval, automated issue resolution, and code agent memory construction. Beyond academia, she is the co-founder of EuniAI, a startup committed to turning research into real-world solutions that help developers address practical software challenges. Personal page: https://heye.me EuniAI page: https://euni.ai Contact: he.ye@ucl.ac.uk |
| Time / date: | October 16th 2025 / 1-2pm |
|---|---|
| Speaker: | Victor Luis Barroso Nascimento (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | On the power and flexibility of base-extension semantics |
| Abstract: | Proof-theoretic semantics (PtS) provides an alternative to model-theoretic semantics by considering proof, not truth, as the basic unit of semantic analysis. This is informed by the philosophical view that our way of engaging with and obtaining knowledge about the world is essentially inferential in nature. Although multiple approaches to PtS are currently being developed, base-extension semantics (BeS) has distinguished itself as one of the most fruitful. In this talk I will present a series of results across multiple contexts with the aim of showing how flexible and powerful BeS is a semantic framework. The first, developed in the context of logical ecumenism, shows that a particular treatment of the absurdity constant allows us to formulate a interesting proof-theoretic concept of classical proof, and by letting it peacefully coexist with the traditional (intuitionistic) concept we obtain semantics for an ecumenical logic. The second, developed in the context of logical bilateralism, shows that the syntactic structure of bases allows us not only to formulate non-interreducible atomic concepts of proof and of refutation, but also to show that syntactic isomorphisms between them have strong semantic bearing, leading to a principle of semantic harmony according to which the proof and refutation conditions of a connective will be harmonic whenever they preserve a fundamental duality already observed at the atomic level. This framework also has very interesting connections with Nelson's strong negation and his concept of constructive falsity. The third, fourth and fifth results, presented in lesser amount of detail, show that there are at least two ways to enrich the notion of proof by making it resource-sensitive to obtain semantics for intuitionistic linear logic; that by promoting a very simple restriction on the quantification over atoms made in the semantic clauses of BeS for the intuitionistic version of a logic we get a semantics for the classical version of that logic and, finally, that if we build a semantics by considering proofs in multi-succedent sequent calculus instead of natural deduction we obtain a very simple, harmonic semantics for classical logic, which is nevertheless sensitive to how structural features of the logic are handled. |
| Time / date: | October 9th 2025 / 1-2pm |
|---|---|
| Speaker: | Yll Buzoku (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Base-extension Semantics for Classical Modal Logics without world relations |
| Abstract: | Modal logics are a well-studied and interesting family of logics for various reasons. Their Kripke semantics is usually quite simple to understand and relies on some notion of an accessibility relation between some objects, usually interpreted as some type of possible world. This requirement continues into the various Proof-theoretic Semantics developed by myself, Timo Eckhardt and David Pym for both classical and intuitionistic modal logics. However, worlds and accessibility relations as they have been used so far are very “model-theoretic” constructs. A question one should ask is “Can one give a reasonable Proof-theoretic Semantics for Modal logics that doesn’t appeal to the use of such an explicit accessibility relation?” The answer to this question is, interestingly, yes. In this talk, I will present one such semantics I have developed for the classical modal logic S4. If we have time, I will also talk about connection between this semantics and work I have previously presented on Intuitionistic Linear Logic, the relation of this semantics to the IPL semantics of Sandqvist and, most interestingly, how one uses this semantics as a basis to obtain similar Proof-theoretic Semantics for the Classical Modal logics: K, T and S5. |
| Time / date: | October 1st 2025 / 1-2pm |
|---|---|
| Speaker: | Jean Krivine (IRIF - Université de Paris) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Reversible computations are computations (joint work with Clément Aubert, Augusta University. USA) |
| Abstract: | Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the observation of its causes. The present work establishes that this simple requirement is equally relevant when the occurrence of an event is invertible. We propose a conservative extension of causal models for concurrency that accommodates reversible computations. We first model reversible computations using a symmetric residuation operation in the general model of configuration structures. We show that stable configuration structures, which correspond to prime algebraic domains, remain stable under the action of this residuation. We then derive a semantics of reversible computations for prime event structures, which is shown to coincide with a switch operation that dualizes conflict and causality. |
| Time / date: | September 25th 2025 / 1-2pm |
|---|---|
| Speaker: | Theo Iosif (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Reviewing DisCoCat – a bridge between language and (quantum) computation |
| Abstract: | Languages can be described mathematically in various ways, from simple models such as bag-of-words or word sequences to grammar aware ones such as dependency grammar or Lambek calculus. The latter fuels our model of interest, the Distributional Compositional Categorical (DisCoCat) model for language. DisCoCat is crafted specifically for the purpose of generating word embeddings quickly based on simple classification tasks. As such, it is implemented in the Python package "lambeq" with the help of tensor networks and quantum circuits. In this talk I will briefly present the model and its corresponding implementation and show theoretical advantages as well as shortcomings. Following this, I plan on outlining possible connections to other topics such as dependency graphs and even quantum theory itself. I hope that this talk will quickly become an interactive discussion about the topic and its connections. |
| Time / date: | August 7th 2025 / 1-2pm |
|---|---|
| Speaker: | Sam Coward (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Equality Saturation and Industrial Circuit Design |
| Abstract: | In this talk I’ll give a brief background on e-graphs and equality saturation, attempting to distill the reasons behind the significant interest in this approach. I’ll then present my research, in collaboration with Intel, into high-performance circuit design exploring how equality saturation can help us to design efficient computational circuits. |
| Time / date: | June 26th 2025 / 1-2pm |
|---|---|
| Speaker: | Daniel Luckhardt (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Expressivity and Hennessy-Milner theorems for bisimulation pseudometrics in a measurable set-up |
| Abstract: | Hennessy-Milner theorems are a key tool in characterising Bisimulation. On the other hand quantified versions of bisimulation in forms of pseudo-metrics have received increased popularity over past decades. When combining both directions technical challenges arise. So far, they forced the resort to a topological structure on the state space. In recent research Beohar, Kupke and I overcame these hurdeles. After giving some motivation, I will explain, how to construnct the behavioral pseudo-distance as a fixt point and then state our adequacy and expressivity results, that combine to a Hennessey-Milner theorem. It will become apparent, that perfectness of the measures—a notion famously introduced by Kolmogorov—and a parametrisation of the language (by a second countable locally compact structure, to be very general) play the key role. Hence, mostly we can work with general measurable spaces. If not, our arguments certainly work for analytic spaces, which have been considered so far as the most general class on which one can work conveniently. |
| Time / date: | June 19th 2025 / 1-2pm |
|---|---|
| Speaker: | Pedro Azevedo de Amorim (University of Oxford) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | A 2-categorical theory of logical relations |
| Abstract: | Logical relations are a key tool in the semanticist's armoury. They play a central role in proofs of adequacy, in chararacterising definability, and in comparing different implementations of the same effect. From a denotational perspective, logical relations are elegantly captured by "fibrations for logical relations". These are fibrations---categorical axiomatisations of the structure of predicates / relations---which strictly preserve the interpretation of types. This theory is well-developed for models of the simply-typed lambda calculus and monadic-style CBV languages with effects, but it is not obvious how to extend it to other kinds of calculi. In this talk I will outline the existing theory, then show how taking a 2-categorical perspective leads naturally to a mathematically-justified definition of fibration---and hence logical relations---for a wide variety of modal languages, including Levy's call-by-push-value. No prior knowledge of 2-categories or fibrations will be assumed. |
| Time / date: | November 6th 2025 / 1-2pm |
|---|---|
| Speaker: | Fredrik Dahlqvist (Queen Mary University of London) |
| Location: | Seminar Room G01, 66-72 Gower Street |
| Title: | Some Terms Are More Equal Than Others |
| Abstract: | Full equality is often impossible to achieve, but this needn't be the end of our struggle to reason equationally about lambda-terms! In this 1st of May seminar we will consider several systems of lambda-terms ranging from totalitarian systems where terms can be terminated or duplicated at will, to individualistic systems where the integrity of terms is sacrosanct. We will show: (i) how quantitative equational theories can be used to reason about the separation between lambda-terms in these systems, and (ii) how sound and complete semantics for these theories can be developed from the close solidarity between terms and morphisms in categories that are enriched in a suitable way (i.e. without reinforcing capitalist exploitation). This is joint work with comrade Renato Neves. |
| Time / date: | April 3rd 2025 / 1-2pm |
|---|---|
| Speaker: | Sergey Goncharov (University of Birmingham) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | From Small-Step to Big-Step, Abstractly |
| Abstract: | Small-step and big-step operational semantics are two fundamental styles of structural operational semantics (SOS). Small-step semantics defines a fine-grained, one-step reduction relation on programs, while big-step semantics directly relates programs to their final evaluation results with respect to the ambient evaluation strategy. Although their agreement is critical for program analysis and reasoning, this is typically proven on a case-by-case basis, lacking a general theoretical foundation. We address this by leveraging higher-order mathematical operational semantics -- an abstract framework recently introduced as a generalization of its established first-order counterpart due to Turi and Plotkin. Specifically, we introduce an abstract categorical notion of big-step SOS, complementing the existing (small-step) notion of abstract higher-order GSOS. We provide a general construction for deriving big-step semantics from small-step semantics, and prove an abstract equivalence between the two. The talk is based on a joint work with Stelios Tsampas and Pouya Partow. |
| Time / date: | March 27th 2025 / 1-2pm |
|---|---|
| Speaker: | Antonio Lorenzin (University College London) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | The Aldous-Hoover Theorem in Categorical Probability |
| Abstract: | The Aldous-Hoover Theorem concerns an infinite matrix of random variables whose distribution is invariant under finite permutations of rows and columns. It states that, up to equality in distribution, each random variable in the matrix can be expressed as a function only depending on four key variables: one common to the entire matrix, one that encodes information about its row, one that encodes information about its column, and a fourth one specific to the matrix entry. After an intuitive explanation of the statement, I will introduce a category-theoretic approach to probability through Markov categories and present the relevant axioms for a synthetic proof of the theorem. We will also briefly discuss the proof technique, which basically consists of verifying three families of conditional independencies. |
| Time / date: | March 20th 2025 / 1-2pm |
|---|---|
| Speaker: | Ian Lo (University College London) |
| Location: | 1.19, Mallet Place Engineering |
| Title: | Quantum-Like Contextuality in Large Language Models |
| Abstract: | Contextuality is a distinguishing feature of quantum mechanics and there is evidence that it is a necessary condition for quantum advantage in the context of magic state distillation. In order to make use of it, researchers have been asking whether similar phenomena arise in other domains. The answer has been affirmative, e.g.\ in behavioural sciences. However, one has to move to frameworks that take some degree of signalling into account. Two such frameworks exist: (1) a signalling-corrected sheaf-theoretic model, and (2) the Contextuality-by-Default (CbD) framework. This paper provides the first large-scale experimental evidence for contextuality in the large language model BERT. We construct a linguistic schema modelled over a contextual quantum scenario, instantiate it in the Simple English Wikipedia and extract probability distributions for the instances. This led to the discovery of 77,118 sheaf-contextual and 36,938,948 CbD contextual instances. We prove that these contextual instances arise from semantically similar words by deriving an equation that relates degrees of contextuality to the Euclidean distance of BERT's embedding vectors. Our linguistic schema is a variant of the coreference resolution challenge. These results suggest that quantum methods may be advantageous in the field of Natural Language Processing. |
| Time / date: | March 13rd 2025 / 1-2pm |
|---|---|
| Speaker: | Guy McCusker (University of Bath) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Taylor Expansion for Imperative Programs |
| Abstract: | The 2024 Alonzo Church Award honoured Ehrhard and Regnier’s body of work on differential lambda calculus and the Taylor expansion of lambda-terms. This powerful technique provides a new approximation theory for functional programs, which understands lambda-terms as formal sums of terms of a linear “resource calculus”. In the resource calculus, ordinary application — in which a term may duplicate or erase its arguments — is replaced by a linear application of terms to multisets of arguments. We explore what happens if the multisets of the resource calculus are replaced by lists, making application order-sensitive. The resulting calculus provides a target for a Taylor expansion of higher order imperative programs with local variables, giving an interpretation of Reynolds’s “Syntactic Control of Interference” (SCI) as formal sums of resource calculus terms. We show that this interpretation is sound and adequate, and that the normal forms of the resource calculus correspond to elements of Reddy’s relational model of SCI. Joint work-in-progress with Pierre Clairambault and Lionel Vaux-Auclair (Aix-Marseille Université) |
| Time / date: | February 27th 2025 / 1-2pm |
|---|---|
| Speaker: | Glynn Winskel (University of Cambridge) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | From Concurrent Games to Goedel's Dialectica Interpretation |
| Abstract: | Computation today is highly distributed and interactive. Event structures represent computation in terms of causal dependency and conflict relations on events; the relations make precise the sense in which events can occur concurrently (independently, in parallel). By redeveloping games in sufficient generality, as event structures, interactive computation becomes a strategy and its type a game. Then the dichotomy between a system and its environment is caught in the distinction between Player and Opponent moves. A functional approach has to handle the dichotomy much more ingeniously, through its blunter distinction between input and output. This has led to a variety of functional approaches, specialised to particular interactive demands. A surprise in the development of concurrent games has been that several, seemingly disparate, historical approaches in logic and computation reappear as special cases. They include stable domain theory; nondeterministic dataflow; geometry of interaction; the dialectica interpretation; lenses and optics; and their extensions to containers in dependent lenses and optics. |
| Time / date: | February 20th 2025 / 1-2pm |
|---|---|
| Speaker: | Greg Restall (University of St Andrews) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Defining Rules for Quantifiers and Identity |
| Time / date: | February 13rd 2025 / 1-2pm |
|---|---|
| Speaker: | Luiz Carlos Pereira (PUC Rio) |
| Location: | 1.02, Malet Place Engineering Building |
| Title: | Revisiting Full Intuitionistic Linear Logic and other (strange) exponentials and quantifiers |
| Abstract: | In 1991, during the LMPS conference organized in Uppsala, Sweden, Valeria de Paiva gave a presentation in which there was a proposal for a categorical semantics for what was then called “Complete Intuitionist Linear Logic”. This logic was named FILL. As far as I know, this was the first public mention to such a complete intuitionistic linear logic. The main idea was the following: to propose a categorical semantics for an intuitionistic linear logic which also contained a multi- plicative disjunction and the exponential “?” (Why not?). According to the de Paiva, this Logic could be easily described by a Gentzen-like sequent calculus where the usual restriction to mono- succedent is imposed only on the rule for (-right. Using this idea, there would be a natural analogy between [1] Gentzen’s LK and Classical Linear Logic (CLL), [2] Gentzen’s LJ and Intuitionistic Linear Logic (ILL), and [3] Maehara’s system LJ 0 and F ILL. In fact, the real analogy would not be between LJ 0 and F ILL, but between a sequent calculus based on LJ 0 for the logic Constant Domains (CD) and F ILL and, given this analogy, simple counter-examples for cut-elimination for F ILL were found. A solution to the cut-elimination problem for Full Intuitionistic Linear Logic was based on a technique explored by Kashima and Shimura with respect to the logic CD of Constant Domains: to replace a cardinality restriction by a control of dependency relations. In this way, a new version of the F ILL system for complete intuitionistic linear logic was proposed. My modest goals will be: [1] to show that this new version of F ILL is not really intuitionist, but rather an intermediate system between a complete intuitionistic linear logic and classical Linear Logic (CLL), in the same sense in which the logic CD is intermediate betwen Intuitionistic Logic (IL) and classical logic (CL); and [2] to investigate some relations between FILL and other het- erodoxical exponentials (as in Dissymetrical Linear Logic - DLL) and quantifiers (like CD, and Dissymetrical First Order Logic - DFOL). |
| Time / date: | February 6th 2025 / 1-2pm |
|---|---|
| Speaker: | Amin Karamlou (University College London) |
| Location: | Room 247, Torrington Place 1-19 |
| Title: | Quantum relaxations of CSP and structure isomorphism |
| Abstract: |
We investigate quantum relaxations of two key decision problems in computer science: the constraint satisfaction problem (CSP) and the structure isomorphism problem. CSP asks whether a homomorphism exists between two relational structures, while structure isomorphism seeks an isomorphism between them. In recent years, it has become increasingly apparent that many special cases of CSP can be reformulated in terms of the existence of perfect classical strategies in non-local games, a key topic of study in quantum information theory. These games have allowed us to study quantum advantage in relation to many important decision problems, such as the k-colouring problem, and the problem of solving binary constraint systems. Abramsky et al. (2017) have shown that all of these games can be seen as special instances of a non-local CSP game. Moreover, they show that perfect quantum strategies in this CSP game can be viewed as Kleisli morphisms of a graded monad on the category of relational structures, which they dub the quantum monad. In this way, the quantum monad provides a categorical characterisation of quantum advantage for the non-local CSP game.
In this talk we shall answer several open questions about the non-local CSP game. We then study a non-local structure isomorphism game, which generalises the well-studied graph isomorphism game. We show how the construction of the quantum monad can be refined to provide categorical semantics for quantum strategies in this game. This results in a category where morphisms coincide with quantum homomorphisms and isomorphisms coincide with quantum isomorphisms. |
| Time / date: | January 30th 2025 / 1-2pm |
|---|---|
| Speaker: | Mina Doosti (University of Edinburgh) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Understanding Quantum Learning and the Quest for Quantum Advantage |
| Abstract: | I will talk about quantum learning theory as a foundational framework for studying quantum machine learning (QML) from a theoretical perspective and its role in uncovering quantum advantages in practical applications. I will provide an overview of some key learning models we developed for the learnability of quantum processes, such as quantum statistical queries (arXiv:2310.02075) and quantum agnostic learning (arXiv:2410.11957). Additionally, I will discuss the connections between these methods and other recently explored theoretical toolkits in QML. Finally, I will mention some future directions for using foundational methods to better characterise the role of quantumness in learning. |
| Time / date: | January 23rd 2025 / 1-2pm |
|---|---|
| Speaker: | Carmen Constantin (University of Oxford) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Localisable Monads |
| Abstract: |
Monads govern side effects in programming semantics and, when a computation uses more than one effect, the corresponding monads can be combined using distributive laws into a single monad. A related use of monads is to have several layers of access to a computational effect, as modelled by indexed and graded monads. This is usually conceived in a 'bottom-up' fashion, where one specifies the behaviour at each level and then adds interplay between the levels.
In this talk, the opposite, 'top-down' approach will be taken: starting with a single monad on a category with some structure we will ask when and how is that monad a combination of constituent monads. This is done using the mathematical formalism of tensor topology, which associates a notion of base space to a given monoidal category. The category then decomposes as a sheaf of categories over its associated base space. Thus, the main question is when and how a monad respects this decomposition. This work is a first step towards an intrinsic theory of computational effects, which does not need to specify in detail how constituent effects have to interact in advance. |
| Time / date: | April 25th 2024 / 1-2pm |
|---|---|
| Speaker: | Dhurim Cakiqi (University of Birmingham) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Algorithmic syntactic causal identification |
| Abstract: | Causal identification in causal Bayes nets (CBNs) is an important tool in causal inference allowing the derivation of interventional distributions from observational distributions where this is possible in principle. However, most existing formulations of causal identification using techniques such as d-separation and do-calculus are expressed within the mathematical language of classical probability theory on CBNs. However, there are many causal settings where probability theory and hence current causal identification techniques are inapplicable such as relational databases, dataflow programs such as hardware description languages, distributed systems and most modern machine learning algorithms. We show that this restriction can be lifted by replacing the use of classical probability theory with the alternative axiomatic foundation of symmetric monoidal categories. In this alternative axiomatization, we show how an unambiguous and clean distinction can be drawn between the general syntax of causal models and any specific semantic implementation of that causal model. This allows a purely syntactic algorithmic description of general causal identification by a translation of recent formulations of the general ID algorithm through fixing. Our description is given entirely in terms of the non-parametric ADMG structure specifying a causal model and the algebraic signature of the corresponding monoidal category, to which a sequence of manipulations is then applied so as to arrive at a modified monoidal category in which the desired, purely syntactic interventional causal model, is obtained. We use this idea to derive purely syntactic analogues of classical back-door and front-door causal adjustment, and illustrate an application to a more complex causal model. |
| Time / date: | Feb 15th 2024 / 1-2pm |
|---|---|
| Speaker: | George Kaye (University Of Birmingham) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | A Fully Compositional Theory of Sequential Digital Circuits |
| Abstract: | Digital circuits, despite having been studied for nearly a century and used at scale for about half that time, have until recently evaded a fully compositional theoretical understanding, in which arbitrary circuits may be freely composed together without consulting their internals. Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated symmetric traced category. However, this was done informally, and in this talk I will show how we have refined and expanded on the previous work in several ways, culminating in the presentation of three sound and complete semantics for digital circuits: denotational, operational and algebraic. |
| Time / date: | Jan 25th 2024 / 1-2pm |
|---|---|
| Speaker: | Carlos Olarte (Université Sorbonne Paris Nord) |
| Location: | Seminar Room 405, 66-72 Gower Street |
| Title: | Process-as-formula interpretation: Subexponentials, focusing and multimodalities in concurrent systems |
| Abstract: | We show how the processes-as-formulas interpretation, where computations and proof-search are strongly connected, can be used to specify different concurrent behaviors as logical theories. The proposed interpretation is parametric and modular, and it faithfully captures behaviors such as: Linear and spatial computations, epistemic state of agents, and preferences in concurrent systems. The key for this modularity is the incorporation of multimodalities in a resource aware logic, together with the ability of quantifying on such modalities. Our tight adequacy results rely on a focusing discipline controlling the proof search process, and we show that one step of logical reasoning corresponds exactly to one step of computation. (Joint work with Elaine Pimentel and Vivek Nigam). |
Department of Computer Science - University College London - Gower Street - London - WC1E
6BT - +44 (0)20 7679 7214 - Copyright © 1999-2025 UCL
Disclaimer: This page's design is cloned from the official page.