Event Title: Modal (Propositions as Types)

Speaker: Nachiappan (Nachi) Valliappan

Dates: Thursday, 27^th November 2025

Time: 11am (GMT)

Location: Edinburgh Bayes Coffee House (4^th floor Bayes Center, EH8 9BT)

Join Online：https://app.huawei.com/wmeeting/join/97172374/EBLvR69PyCciIQAbMEtNCHM4PJYNA1XrY

Meeting ID：97172374

Passcode：507513

Talk Abstract:

“Propositions as types” is a slogan that refers to the one-to-one correspondence between propositions in formal logic and types in programming language theory. The discovery of this correspondence in the twentieth century opened the gates for cross-disciplinary exchange of ideas and has since had an enormous impact on the mutual development of formal verification tools and programming languages. In recent times, however, programming language research has seen a rise in the development of so-called “modal” types whose status is yet to be settled from the perspective of logic. These appear, at the surface level, an awful lot like modalities in modal logic, but much has remained unclear on the matter. This gap in the propositions-as-types correspondence is a lost opportunity: modal logics enjoy a rich suite of analysis tools that could be readily ported to modal type systems via the correspondence. This talk is about ongoing research in the conjunction of intuitionistic modal logic and programming languages to bridge this gap, and the potential applications of this research in modular program transformation and security analyses.

Speaker:
Nachiappan (Nachi) Valliappan is a Royal Society Newton International Fellow in the Laboratory for Foundations of Computer Science at the University of Edinburgh.

Event Title: Sound Interval-Based Synthesis of Probabilistic Programs

Speaker: Guilherme Espada

Dates: Thursday, 20^th November 2025

Time: 11am (GMT)

Location: Edinburgh Bayes Coffee House (4^th floor Bayes Center, EH8 9BT)

Join Online:  https://app.huawei.com/wmeeting/join/96296184/ihsFKR3egE2YzZOkWHrI7TIfWGtAe2bCN

Meeting ID：96296184

Passcode：100424

Abstract:

Probabilistic programming has become a standard practice to model the stochasticity inherent in modeling the real world, and to analyse behavior of nature in different scientific disciplines. However, domain practitioners also need to be experts in statistics in order to select which probabilistic model is suitable for a given particular problem. Additionally, automatically selecting the model is challenging due to the large search space, mostly occupied by invalid programs that may only be detected in a subset of executions.
We propose a bounds-based type system to statically identify invalid probabilistic programs and a type-directed synthesis algorithm that guarantees correctness by construction. The resulting system allows for fast sampling of programs and enables application of techniques that previously suffered from the complexity of synthesis, such as Genetic Programming.

Bio:Guilherme Espada earned his M.Sc. in Computer Science from the University of Lisbon (Faculdade de Ciências) in 2020. He is currently pursuing a Ph.D. at LASIGE, University of Lisbon, where he authored research on grammar-guided genetic programming, symbolic regression, and type systems.

Event Title: Exploring Network Analysis in Telecom, the Macaque Brain and Other Stories

Speaker: Prof. Amit A. Nanavati

Dates: Thursday, 30^th October 2025

Time: 11am (GMT)

Location: Edinburgh Bayes Coffee House (4^th floor Bayes Center, EH8 9BT)

Join Online: https://app.huawei.com/wmeeting/join/98718641/aygjCvYF0uw08IwFj6UMR8dkxAplu4FQQ

Abstract: We will explore social networks induced by calling patterns of the customers of Telecom Service Providers. We build a social network of the telecom subscribers from the “who-calls-whom” CDR (Call Detail Record) data: we find communities, predict potential churners, identify influencers, etc. We will also take a look at the Macaque Monkey’s brain network as an information network to glean insights from it. Social media platforms such as Twitter have been the target of hatred and hostility. We will discuss models for the spread of hate speech. Finally, we will also briefly visit “signed networks” where edges have a +/- sign associated to indicate a positive/negative interaction between its endpoints.

Bio: Amit A. Nanavati is a Professor at Ahmedabad University and was a visiting researcher at the Informatics Forum (Feb – July, 2025). Prior to this, Amit was a part of IBM Research (2000-2016) and IBM GTS Innovation Labs (2016-21). Amit led the Telecom Research group on The Spoken Web and SNAzzy projects.  The Spoken Web project received the National Award 2009 for Technological Innovation/Best Applied Research Aimed at Improving the Life of Persons with Disabilities given by the President of India. The SNAzzy project won an Outstanding Science Accomplishment Research Division Award in 2015.  His 2008 paper “Social Ties and their Relevance to Churn in Mobile Telecom Networks” won the EDBT Test of Time Award in 2018. He became an ACM Distinguished Speaker in 2014, and an ACM Distinguished Scientist in 2015.

Join us for this exciting talk by Dr. Adrien Bousseau, senior researcher at Inria Université Côte d’Azur in the GraphDeco group. In this talk, Dr. Bousseau will share his research on how the geometric language and drawing techniques implicit in sketches can be used to automate modelling from 2D to 3D.

Event Title: Interpreting Drawings for 3D Design – From Drawing Techniques to Algorithms

Speaker: Dr. Adrien Bousseau

Dates: 9^th July 2025

Time: 11:00-12:00 (UK Time, UTC +1)

Location: Edinburgh Bayes Coffee House (4^th floor Bayes Center, EH8 9BT)

Join Online: https://www.chaspark.com/#/live/1157038585460486144?multi=en

Abstract: Designers draw extensively to externalize their ideas and communicate with others. But drawings are currently not directly interpretable by computers. To test their ideas against physical reality, designers have to create 3D models suitable for simulation and 3D printing. However, the visceral and approximate nature of drawing clashes with the tediousness and rigidity of 3D modeling. As a result, designers only model finalized concepts, and have no feedback on feasibility during creative exploration.

The long term goal of our group is to bring the power of 3D engineering tools to the creative phase of design by automatically estimating 3D models from drawings. However, this problem is ill-posed: a point in the drawing can lie anywhere in depth. Our originality is to exploit drawing techniques that designers developed to communicate shape most efficiently. Each technique provides geometric constraints that help viewers understand drawings, and that we shall leverage for 3D reconstruction.

Bio: Adrien Bousseau is a senior researcher at Inria Université Côte d’Azur in the GraphDeco research group. He completed his PhD at Inria Rhône-Alpes and his postdoc at UC Berkeley. Adrien Bousseau conducts research on image creation and manipulation, particularly drawings and photographs. His work has included image stylization, image editing and relighting, vector graphics, and sketch-based modeling. He received one of three 2011 Eurographics PhD awards for his research on expressive image manipulation, as well as a young researcher award from the French National Research Agency (ANR) for his work on computer-aided drawing.

He received an ERC Starting Grant and a Proof of Concept Grant to work on drawing interpretation for 3D design.

Title: Maximus: A Modular Accelerated Query Engine for Data Analytics on Heterogeneous Systems

Speaker: Marko Kabić | ETH Zurich

Location: Online

Time: 05/07(Wed) 13:30-14:30 (UTC+01:00)London

External: https://app.huawei.com/wmeeting/join/95709180/ML6masIeHafOBZ9P8HZysSWGQt3RA4okX

Meeting ID: 95709180

Passcode:375969

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

Several trends are changing the underlying fabric for data processing in fundamental ways. On the hardware side, machines are becoming heterogeneous with smart NICs, TPUs, DPUs, etc., but specially with GPUs taking a more dominant role. On the software side, the diversity in workloads, data sources, and data formats has given rise to the notion of composable data processing where the data is processed across a variety of engines and platforms. Finally, on the infrastructure side, different storage types, disaggregated storage, disaggregated memory, networking, and interconnects are all rapidly evolving, which demands a degree of customization to optimize data movement well beyond established techniques. To tackle these challenges, in this paper, we present Maximus, a modular data processing engine that embraces heterogeneity from the ground up. Maximus can run queries on CPUs and GPUs, can split execution between CPUs and GPUs, import and export data in a variety of formats, interact with a wide range of query engines through Substrait, and efficiently manage the execution of complex data processing pipelines. Through the concept of operator-level integration, Maximus can use operators from third-party engines and achieve even better performance with these operators than when they are used with their native engines. The current version of Maximus supports all TPC-H queries on both the GPU and the CPU and optimizes the data movement and kernel execution between them, enabling the overlap of communication and computation to achieve performance comparable to that of the best systems available, but with a far higher degree of completeness and flexibility.

Bio:

I am a PhD student in Computer Science in the Systems Group at ETH Zurich (Switzerland), supervised by prof. Gustavo Alonso. During the studies, I did an internship at Hewlett-Packard Labs. Before commencing my PhD studies, I worked for several years at Swiss National Supercomputing Centre (CSCS). My research focuses on data management systems for data analytics on heterogeneous hardware.

Title: Applied Programming Language Theory at Scale

Speaker: Nick Benton

Time: 05/01(Thur) 11:00-12:00 (UTC+01:00)London

Location: Bayes Coffee House Bayes Centre 4^th Floor, 47 Potterrow, Edinburgh EH8 9BT

External: https://app.huawei.com/wmeeting/join/94300732/e63CVQfGjz0pwKxkIYXCGkFCiy8Toyd5T

Meeting ID: 94300732

Passcode: 362414

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

Facebook’s codebase is powered by a language called Hack, a typed evolution of PHP. We’ll dive into the story of how programming language theory shaped Hack’s design and implementation, and the new theory we developed along the way. We’ll also describe the challenges and compromises involved in evolving a language in active use at enormous scale.

Bio:

Nick Benton recently retired after 8 years as a software engineer and engineering manager at Meta in London, working mainly on the Hack language and the Infer static analyser. Prior to that, he spent 18 years at Microsoft Research in Cambridge.

His research ranges from proof theory and categorical logic, through semantics of programming languages and static analyses, to programming language design and compiler implementation. His thesis was on strictness analysis and he has since worked on topics that include term calculi and categorical models for linear logic, MLj and SML.NET (optimizing compilers from SML to the JVM and .NET with extensions for interlanguage working), Polyphonic C#/Cω (C# with join-calculus concurrency and XML/relational data constructs), monads and effect systems, models for dynamic allocation, compositional compiler correctness, mechanically formalized logics for reasoning about machine code programs, and reactive programming.

Nick has a degree in Mathematics and a PhD in Computer Science, both from the University of Cambridge, and is a Fellow Commoner of Queens’ College.

Title: Practices of Using Small and Large Language Models for Entity Resolution

Time: 04/28(Mon) 13:00-14:00 (UTC+01:00)London

Location: Online

Speaker: Zeyu Zhang | University of Amsterdam

External: https://app.huawei.com/wmeeting/join/95886293/MipIlMdSMCMSGacGvUoquknvJnJSqHfS0

Meeting ID: 95886293

Passcode: 505536

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

While Large Language Models (LLMs) excel at knowledge reasoning tasks, they face significant challenges in formal mathematical theorem proving due to data scarcity and strict logical precision requirements. This talk introduces the DeepSeek-Prover series, highlighting how automated dataset construction and reasoning annotations have effectively transferred knowledge from data-rich to data-scarce domains, achieving state-of-the-art results in formal proofs. Additionally, formal theorem proving will be discussed as an ideal benchmark for evaluating rigorous reasoning capabilities of language models.

Bio:

Zeyu Zhang is a third-year Ph.D. student at the INDElab, University of Amsterdam. He finished his bachelor and master study from the Harbin Institute of Technology (HIT) and the Eindhoven University of Technology (TU/e), respectively. Zeyu’s research focuses on tabular data understanding, spanning from conventional machine learning models to large language models.

One of the key challenges in achieving reasoning capabilities in generative AI models is grounding, or the ability to link information bits, such as entities, concepts, actions, etc, across different modalities.

This talk explores how explicit grounding can significantly improve multimodal AI systems through two case studies:

Visual Storytelling – Maintaining narrative coherence across modalities

Instructional Video Understanding – True comprehension of procedural knowledge

Title: Grounding across Modalities and Domains

Speaker: Frank Keller | School of Informatics, University of Edinburgh

Time: 04/29(Tues) 11:00-12:00 (UTC+01:00)London

Location: Bayes Center G03

External: https://app.huawei.com/wmeeting/join/97996549/XSZeBJABg80yz3SqXLYLxSeeYuWYBzpdl

Meeting ID: 97996549

Passcode: 228808

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

In order to understand or generate multimodal inputs, AI systems must perform grounding — the process of linking entities or actions across different modalities. For example, objects depicted in images and videos need to be associated with corresponding textual references.

However, large language models struggle with grounding, limiting their performance in tasks such as image generation and video understanding.

In this talk, I will present two case studies demonstrating how explicit grounding can enhance multimodal AI. First, I will argue that character grounding is essential for visual storytelling — the task of turning a sequence of images into a coherent narrative. I will introduce a model that generates visually grounded stories by building coreference chains for characters across images and text, leading to stories that are more specific, coherent, and engaging.

The second case study focuses on understanding instructional videos, such as those demonstrating cooking or home improvement tasks. In this domain, entities are often implicit (not mentioned in text) and frequently change (being merged, separated, or transformed), making grounding particularly challenging. I will present models that address this challenge by computing the semantic roles of both explicit and implicit entities and tracking them across instructional steps, even as they undergo transformations. These models enhance procedural understanding, improving AI’s ability to follow and reason about complex tasks.

Bio:

Frank Keller is a professor in the School of Informatics at the University of Edinburgh. He has held visiting positions at MIT and the University of Washington. His research focuses on natural language processing, particularly language and vision tasks such as image description, video summarization, and visual storytelling. He is also develops systems that understand long-form narratives, including books and screenplays, and builds computational models of human language processing.

Prof. Keller co-leads the UKRI Centre for Doctoral Training in Responsible Natural Language Processing, which aims to develop trustworthy and ethical NLP systems. He serves on the editorial board of Transactions of the ACL and is an ELLIS fellow. Previously, he was awarded an ERC grant for his research on language and vision.

Title: Leveraging Large Language Models for Formal Mathematical Theorem Proving: Data Synthesis and Chain-of-Thought Annotation in the DeepSeek-Prover Series

Time: 04/09(Wed) 11:00-12:00 (UTC+00:00)London

Location: Bayes Center G03

Speaker: Huajian Xin | University of Edinburgh

External: https://app.huawei.com/wmeeting/join/96997133/ZYcf41v9fw0RPa2ttq43IyJzlH3zLlndd

Meeting ID: 96997133

Passcode: 165433

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

Large language models (LLMs) excel at information retrieval, knowledge memorization, and reasoning, yet they face challenges in domains with scarce data and long-tail distributions, such as formal mathematical theorem proving. In this domain, LLMs must generate rigorous, verifiable proof scripts for interactive theorem-proving systems. Challenges stem from limited natural-language corpora, the demand for logical precision, and strict accuracy requirements. In developing DeepSeek-Prover V1, we automated large-scale translation of natural-language mathematical problems into formal propositions and synthesized corresponding proofs. After rigorous multi-level filtering, fine-tuning on this dataset achieved state-of-the-art results, effectively distilling knowledge from data-rich to data-scarce parallel domains. DeepSeek-Prover V1.5 further introduced automatic annotation of chain-of-thought reasoning within proof code data, enabling smaller models to adopt explicit reasoning strategies that significantly improve long-reasoning tasks. This talk will also introduce formal mathematical theorem proving as an ideal benchmark for evaluating and training language models’ capabilities in rigorous reasoning.

Bio:

Huajian Xin is currently a PhD student at the University of Edinburgh under Professor Li Wenda. His research focuses on enabling large language models (LLMs) to perform formalized mathematical theorem proving, with a particular emphasis on autoformalization tasks that bridge natural language and formal language, as well as agent tasks that leverage computer algebra systems and other tools. He is also interning with the ByteDance Doubao/Seed Team and previously interned at DeepSeek, where he led the research on the DeepSeek Prover series of models. For more information, please visit his personal homepage at https://xinhuajian.wordpress.com.

Title: On Optimizing the Optimizer

Time: 03/19(Wed) 13:00-14:00 (UTC00:00)London

Speaker: Prof. Wolfgang Lehner

Location: 2SS 5F-Meeting Room 1 (14 pax)

External: https://app.huawei.com/wmeeting/join/97284648/RkY0TJkd6WSgy8VlqDebOsp1wK5jjTkmZ

Meeting ID: 97284648

Passcode: 223007

Registration: https://www.smartsurvey.co.uk/s/3N8U7J/

Abstract:

The traditional cost-based query optimizer approach enumerates different execution plans for each individual query, assesses each plan with costs, and selects the plan that promises the lowest costs for execution. However, – as we all know – the optimal execution plan is not always selected. To steer the optimizer in the right direction, many database systems provide optimizer hints. These hints can be set for workloads, individual queries or even for query fragments.

Within this talk, we first show the potential of optimizer hinting by presenting the results of a comprehensive and in-depth evaluation using three benchmarks and two different versions of the open-source database system PostgreSQL. Subsequently, we highlight that query optimizer hinting is a nontrivial challenge and show two potential solutions: On the one hand, we propose TONIC, a novel cardinality estimation-free extension for generic SPJ query optimizers. TONIC follows a learning-based approach and revises operator decisions for arbitrary join paths based on learned query feedback. To continuously capture and reuse optimal operator selections, we introduce a lightweight yet powerful Query Execution Plan Synopsis (QEP-S). On the other hand, we provide insights into FASTgres, a context-aware classification strategy for a more holistic hint set prediction. Both strategies show in the context of end-to-end evaluations significant reductions of benchmark runtimes.

Bio: 

Wolfgang Lehner is professor at TU Dresden, leading the database technology group as well as the institute of systems architecture. He is mostly interested in cross-cutting data management themes from complex analytical tasks and workflows to technologies pushing the envelope in compile and runtime of a data system. He serves the international database community in many ways (e.g. VLDB Endowment, PVLDB Management Editor, PC-CoChair/MetaReviewer/Reviewer activities). He is an appointed member of the German Council for the Sciences and Humanities as well as a member of the Academy of Europe. In this talk, he presents some of the research he and his research team has been conducting regarding optimizing the optimizer.