Maribel Fernandez (Joint FSCD-CADE)

King’s College London

Title: Nominal Techniques for Software Specification and Verification

Abstract: The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. With a user-friendly first-order syntax, nominal logic provides a formal framework to reason about binding operators similar to conventional, on-paper reasoning. Indeed, nominal logic uses the well-understood concept of permutation groups acting on sets to provide a rigorous first-order treatment for the common informal practice of fresh and bound names. 

In this talk, I will present our current work towards incorporating nominal techniques into two widely-used rule-based first-order verification environments: the K specification framework and the Maude programming environment. Read More

Mateja Jamnik (Joint FSCD-CADE)

University of Cambridge, UK (Department of Computer Science and Technology)

Title: How can we trust AI?

Abstract: Not too long ago most headlines talked about our fear of AI. Today, AI is ubiquitous, and the conversation has moved on from whether we should use AI to how we can trust the AI systems that we use in our daily lives. In this talk I look at some key technical ingredients that help us build confidence and trust in using intelligent technology. I argue that intuitiveness, interaction, explainability and inclusion of human domain knowledge are essential in building this trust. I present some of the techniques and methods we are building for making AI systems that think and interact with humans in more intuitive and personalised ways, enabling humans to better understand the solutions produced by machines, and enabling machines to incorporate human domain knowledge in their reasoning and learning processes.

Bio: Mateja Jamnik is Professor of Artificial Intelligence at the University of Cambridge, UK. She is developing AI techniques for human-like computing – she combines AI reasoning with machine learning techniques in order to advance the explainability of AI systems, and applies them to personalised medicine and tutoring systems. Mateja is passionate about bringing science closer to the public and engages frequently with the media and outreach events. She has been advising the UK government on policy direction in relation to the impact of AI on society.

Giulio Manzonetto

LIPN&CNRS, Université Sorbonne Paris Nord

Title: A Lambda Calculus Satellite

Abstract: Barendregt’s book “The Lambda Calculus, its syntax and semantics”
(1981/84) has become a ‘classic’ in Theoretical Computer Science because it presents the state of the art in lambda calculus at that time in a comprehensive way. Moreover, a number of open problems and conjectures were proposed. In 2022, Barendregt and Manzonetto published a ‘sequel’ of this book, presenting the solutions of several of these problems, and more. In this talk, I will present a selection of these problems and the key ingredients that were employed in their solutions.

Akihisa Yamada

Cyber Physical Security Research Center, National Institute of Advanced Industrial Science and Technology (AIST)

Title: Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition

Abstract: Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly.

Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.