Keynote Speakers
Jasmin Christian Blanchette
Ludwig-Maximilians-Universität München
Lambda-Superposition: From Theory to Trophy
Abstract: Lambda-superposition is a proof calculus for higher-order logic (simple type theory) developed in collaboration with Alexander Bentkamp, Simon Cruanes, Visa Nummelin, Sophie Tourret, Petar Vukmirović, and Uwe Waldmann. To a large extent, the calculus is a graceful generalization of standard superposition, which is a highly successful calculi for first-order logic. On the theory side, we proved the lambda-superposition refutationally complete. On the practical side, we implemented it in the Zipperposition prover and, together with Stephan Schulz, in the E prover. Zipperposition finished first in the higher-order theorem division of the CADE ATP System Competition in 2020, 2021, and 2022, suggesting that superposition is a valuable approach also in a higher-order setting.
Bio: Jasmin Blanchette is holder of the Chair of Theoretical Computer Science at Ludwig-Maximilians-Universität München. His research focuses on the use and development of proof assistants and automatic theorem provers. On the proof assistant front, he (co)developed three tools for the Isabelle/HOL proof assistant: the Nitpick model finder, the Sledgehammer proof tool, and the (co)datatype package. On the automatic theorem proving front, he and his colleagues developed lambda-superposition. He also applied proof assistants to verify the correctness of the logical calculi underlying automatic provers.
Maribel Fernandez (Joint FSCD-CADE)
King’s College London
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)
How Can We Make Trustworthy 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.