# 2025 Program
**Source**: https://comp.anu.edu.au/lss/lectures/2025/
**Parent**: https://comp.anu.edu.au/lss/
On this page
- [2025 Program](#2025-program)
- [Fundamentals of Metalogic\
(John Slaney)](#John)
- [Computability and Incompleteness\
(Michael Norrish)](#Michael)
- [Overview of Automated Reasoning\
(Peter Baumgartner)](#Peter)
- [Introduction to Interactive Theorem-Proving with Isabelle\
(Liam O’Connor)](#Liam)
- [Intuitionistic Modal Logic \
(Sonia Marin)](#Sonia)
- [Proof Engineering for Program Logics in Isabelle/HOL\
(Chelsea Edmonds)](#Chelsea)
- [Resolution for Non-Classical Logics\
(Cláudia Nalon)](#Claudia)
- [Topics:](#topics)
- [Course Description](#course-description)
- [Barriers to Entailment\
(Gillian Russell)](#Gillian)
- [Modal Type Theories and Logical Relations\
(Vineet Rajani)](#Vineet)
# 2025 Program
**Week 1**
- [Fundamentals of Metalogic](#John) by [John Slaney](https://users.cecs.anu.edu.au/~jks/)
- [Computability and Incompleteness](#Michael) by [Michael Norrish](https://comp.anu.edu.au/people/michael-norrish/)
- [Overview of Automated Reasoning](#Peter) by [Peter Baumgartner](https://peba62.github.io)
- [Introduction to Interactive Theorem-Proving with Isabelle](#Liam) by [Liam O’Connor](https://comp.anu.edu.au/people/liam-oconnor/)
**Week 2**
- [Intuitionistic Modal Logic](#Sonia) by [Sonia Marin](https://filipendule.github.io/)
- [Advanced Isabelle for Software Verification](#Chelsea) by [Chelsea Edmonds](https://cledmonds.github.io)
- [Resolution for Modal Logics and its Implementation](#Claudia) by [Cláudia Nalon](https://nalon.org)
- [Barriers to Entailment](#Gillian) by [Gillian Russell](https://gillianrussell.net/)
- [Modal Type Theories and Logical Relations](#Vineet) by [Vineet Rajani](https://vineetrajani.github.io/)
\
---
## Fundamentals of Metalogic (John Slaney)
**Keywords**
Completeness theorems, Model theory, proof theory.
**Abstract**
This course provides an introduction to the metatheory of elementary logic. Following a “refresher” on the basics of notation and the use of classical logic as a representation language, we concentrate on the twin notions of models and proof. An axiomatic system of first order logic is introduced and proved complete for the standard semantics, and then we give a very brief overview of the basic concepts of proof theory and of formal set theory. The material in this course is presupposed by other courses in the Summer School, which is why it is presented first.
**Pre-requisites**
It is assumed that students are at least familiar with logical notation for connectives and quantifiers, and can manipulate truth tables, some kind of proof system or semantic tableaux or the like. Normally they will have done a first logic course at tertiary level. Some basic mathematical competence is also presupposed, to be comfortable with the notion of a formal language, follow proofs by induction, be OK with basic set-theoretic notation and the like.
**Lecturer**
John Slaney is the founder and convenor of the Logic Summer school. He originated in England, ever so long ago, and discovered Australia in 1977. Undeterred by the fact that it had apparently been discovered before, he gradually moved here, joining the Automated Reasoning Project in 1988 on a three-year contract because he could not think of anywhere better to be a logician. He is still here and still can’t. His research interests pretty much cover the waterfront, including non-classical logics, automated deduction and all sorts of logic-based AI. He was formerly the leader of the Logic and Computation group at the ANU, and of the NICTA program of the same name.
---
## Computability and Incompleteness (Michael Norrish)
**Keywords**
Computability; recursive Functions and Turing machines; diagonalisation; Peano arithmetic and Gödel numbering; undecidability of first-order logic; incompleteness of Peano arithmetic.
**Abstract**
We begin with two formal accounts of the intuitive notion of computability: recursive functions and Turing machines. They turn out to be the same, hence Church’s Thesis: functions that can be computed by any means are precisely the partial recursive functions. Then we revisit the old Cretan who says that all Cretans always lie, and other forms of diagonalisation argument such as Halting Problem. Next we look at an axiomatic theory of arithmetic, known as Peano Arithmetic (PA), and show how we can represent all recursive functions in PA.
This will lead to Goedel numbering: a neat trick enabling us to effectively encode notions like “theorem”, “proof” and “provability in PA” within PA itself. We spend a while discussing Diagonalisation Lemma and Derivability Conditions. Finally, in one fell swoop we prove undecidability of first-order logic (Church’s Theorem), undefinability of truth (Tarski’s Theorem), incompleteness of PA given consistency of PA (First Goedel’s Theorem) and unprovability of consistency of PA given consistency of PA (Second Goedel’s Theorem).
**Pre-requisites**
Foundations of first-order logic
**Background reading**
G. Boolos and R. Jeffrey, *Computability and Logic*.
**Lecturer**
Michael Norrish is an Associate Professor at the Australian National University. Before joining the ANU, he worked for Data61, CSIRO. He is originally from Wellington, New Zealand, and is very happy to be back in the southern hemisphere, after an extended stint in Cambridge, England. It was there that he did his PhD, and then spent three years as a research fellow at St. Catharine’s College. His research interests include interactive theorem-proving, and the application of this technology to areas of theoretical computer science, particularly the semantics of programming languages.
**Slides**
- [Lecture 1](https://comp.anu.edu.au/lss/lectures/2025/computability-goedel-1.pdf)
- [Lecture 2](https://comp.anu.edu.au/lss/lectures/2025/computability-goedel-2.pdf)
- [Lecture 3](https://comp.anu.edu.au/lss/lectures/2025/computability-goedel-3.pdf)
- [Lecture 4](https://comp.anu.edu.au/lss/lectures/2025/computability-goedel-4.pdf)
- [Lecture 5](https://comp.anu.edu.au/lss/lectures/2025/computability-goedel-5.pdf)
## Overview of Automated Reasoning (Peter Baumgartner)
**Abstract**
Automated reasoning is concerned with developing push-button technology for
logical reasoning on a computer using general methods. These general methods
take as input a problem specification in some variant of mathematical logic
and solve a specific reasoning task. For example, Sudoku puzzles can be
specified in propositional logic and the reasoning task is to find a
solution. For example, an algorithm for sorting lists of integers can be
specified in first-order logic, and the reasoning task is to prove that the
algorithm works correctly for all possible inputs.
This course gives an overview of automated reasoning with propositional and
with first-order logics. It covers important reasoning tasks, such as model
finding (solving) and automated deduction (proving). The emphasis will be on
methods (calculi) for these reasoning tasks. This includes specialized methods
for, e.g., arithmetic (theory reasoning).
The lecture is intended as a broad overview, with many examples, but will also
include some proofs or arguments of correctness.
**Lecturer**
Peter is a Principal Research Scientist at CSIRO/Data61 (Australia) since 2016 and a Honorary Associate Professor at ANU. Previous positions include NICTA (Australia) since 2005, the Max-Planck Institute for Computer Science (Germany), the University of Koblenz (Germany), and the Technical University of Munich (Germany). I have worked extensively on the automation of symbolic reasoning techniques. My current research focuses on combining these with statistical machine learning techniques, including LLMs. I am passionate about programming and translating theory into practical applications. Qualifications: Habilitation in Computer Science (U Koblenz, Germany, 2002), Ph.D. in Computer Science (Dr. Rer. Nat, U Koblenz, Germany, 1996), Master’s degree in Computer Science (Diplom, TU Munich, Germany, 1988).
**Slides**
- [Lecture slides](https://comp.anu.edu.au/lss/lectures/2025/LSS-AR-2025.pdf)
For links to resources for the Beagle theorem prover, see [Peter’s homepage](https://peba62.github.io/teaching/).
## Introduction to Interactive Theorem-Proving with Isabelle (Liam O’Connor)
**Abstract**
This course will introduce the use of interactive proof assistants both for mathematics and for work in software verification. We will introduce the basics of interactive theorem proving using the proof assistant Isabelle/HOL. Starting from elementary logical formulae, we will prove many theorems “live” in lectures, and apply what we have learned to proof exercises and challenges. Proof assistants can be both very fun and very addictive in equal measure. It is my hope to share that fun with you :)
***Topic list (tentative):***
1. Propositional and first-order logic, natural deduction proofs. Types, definitions, unfolding.
2. Structural induction, inductive definitions, induction tactics.
3. Simplifier, rewriting, function definitions, other definitions.
4. Structured proofs in Isar, calculational proofs. More automatic methods, sledgehammer.
Remaining topics to be covered if there is time:
- General recursion and termination measures
- Type classes and locales
- Program verification with SIMPL or AutoCorres
- Designing tactics with Eisbach
**Student Participation**
[Please install Isabelle from here before the first lecture.](https://isabelle.in.tum.de)
Isabelle comes as a bundle with everything needed for the three main platforms (Windows, Linux, Mac), including Isabelle/jEdit which can be launched easily from the bundle. If students have trouble installing it, contact Liam O’Connor, [liam.oconnor@anu.edu.au](mailto:liam.oconnor@anu.edu.au).
**Prerequisites**
Some familiarity with simple first order and propositional logic is assumed. Some functional programming experience (in particular, some familiarity with lambda calculus or a language like Haskell) is also recommended.
**Recommended further reading**
[Concrete Semantics, Tobias Nipkow and Gerwin Klein](http://concrete-semantics.org/)
**Lecturer**
Liam O’Connor is a Senior Lecturer at the Australian National University and an Honorary Fellow at the University of Edinburgh, where he worked until 2024. He obtained his PhD from UNSW in 2019, the dissertation for which received the John Makepeace Bennett award. He has broad interests in theoretical computer science, especially in semantics, models and specifications, as well as in the application of these theoretical techniques to practical problems in programming languages, systems and software engineering.
**Lecture notes**
[Link to Liam’s lecture notes](https://liamoc.net/forest/isa-0001)
## Intuitionistic Modal Logic (Sonia Marin)
Intuitionistic modal logic, despite more than seventy years of investigation still partly escapes our comprehension.
Applications of intuitionistic versions of modal logics can be found for example in type disciplines for programming languages or in meta-logics for reasoning about a variety of computational phenomena.
Just in the last few years, there have been work on non-wellfoudned proof theory for intuitionistic modal logics with fixed points, deep developments in modal type theory and applications to meta-programming; just to cite a few directions in which intuitionistic modal logics are now expanding.
In this course we will give an overview of the current understanding of the intuitionistic modal logic landscape and survey some of the more recent developments.
**Lecturer**
Dr. Sonia Marin is a Lecturer in the School of Computer Science at the University of Birmingham and a member of the Theory of Computation research theme. She completed her Ph.D. in Computer Science in 2018 at Inria Saclay. Her research focuses on proof theory, intuitionistic modal logics, and formal reasoning. After her Ph.D., she was a postdoctoral researcher at the IT University of Copenhagen, then joined University College London as a research fellow. Since 2021, she has been at the University of Birmingham, where she conducts research, teaches courses, and supervises students on topics related to logic, computation, and formal methods.
**Slides**
- [Lecture 1](https://comp.anu.edu.au/lss/lectures/2025/SM_Lecture1.pdf)
- [Lecture 2](https://comp.anu.edu.au/lss/lectures/2025/SM_Lecture2.pdf)
- [Lecture 3](https://comp.anu.edu.au/lss/lectures/2025/SM_Lecture3.pdf)
- [Lecture 4](https://comp.anu.edu.au/lss/lectures/2025/SM_Lecture4.pdf)
- [Lecture 5](https://comp.anu.edu.au/lss/lectures/2025/SM_Lecture5.pdf)
- [References](https://comp.anu.edu.au/lss/lectures/2025/SM_Refs.pdf)
## Proof Engineering for Program Logics in Isabelle/HOL (Chelsea Edmonds)
Program logics enable us to formally reason on the correctness of a program, but on paper proofs can be complex or long, resulting in subtle errors. Formalising such proofs in a proof assistant offers a way to avoid this; however, in such a formal environment small design choices in a program logic definition can significantly impact the complexity of formal proofs. Thus “proof engineering” decisions play a critical role in managing this, as well as supporting the modularity and reusability of formal libraries.
This course will explore several program logic definitions, focusing on Hoare logic for sequential programs and Rely-Guarantee logic for concurrent programs, including introducing a novel coinductive approach. The theory will be introduced alongside defining and reasoning on these definitions in the Isabelle/HOL proof assistant, demonstrating the impact of proof engineering decisions. Building on the introductory Isabelle course, we’ll explore a number of more advanced features such as (co)inductive definitions and tactics, as well as locales (Isabelle’s module system), and gain hands-on experience in program verification using Isabelle. If time permits, we’ll look at how some of the basic concepts translate to other popular proof assistants.
**Additional Resources:**
[Concrete Semantics, Tobias Nipkow and Gerwin Klein](http://concrete-semantics.org/)
**Lecturer**
Chelsea is a Lecturer at the University of Western Australia, having recently returned to Australia following a postdoc at the University of Sheffield.
Originally from Brisbane, she completed her
undergraduate studies in Software Engineering and Mathematics at the
University of Queensland. After a two year stint in industry as a
software engineer, she returned to academia and completed her PhD in
Computer Science at the University of Cambridge. Her research focuses
on the applications of interactive proof assistants in both
mathematics and computer science using modular proof techniques - from
formalising combinatorics to verifying security properties of
programs.
**Lecture notes and resources**
[Click here for Chelsea’s course page](https://cledmonds.github.io/anulss2025/)
## Resolution for Non-Classical Logics (Cláudia Nalon)
### Topics:
- Introduction to modal logic: normal and non-normal modal logics
- Resolution for classical propositional logic
- Resolution for normal and non-normal modal logics
- Efficient implementation of resolution
Content: Propositional modal logic, Local and global satisfiability problems, Resolution for Modal Logics
### Course Description
Modal logics have been extensively used in Computer Science as a
language for naturally describing complex systems and their
properties. Several proof methods have been designed to deal with the
reasoning tasks for those logics. This course will focus on
resolution, a proof method proposed by Robinson in the 1960s, which
has become one of the most widely implemented calculi, leading to
successful tools for Automated Reasoning in classical logics. In this
course, we will examine resolution-based proof methods for the basic
propositional modal logics K and E, and some of its extensions. After
introducing the basics of modal logics, we will review the proof
method proposed by Robinson for classical propositional logic. We will
then discuss how the method needs to be adapted to the non-classical
case. Finally, we will discuss some of the characteristics of
resolution calculi that may contribute to their efficient
implementation.
Pre-requisites: Elementary logic, as covered in the “Fundamentals of Metalogic” course.
**Lecturer**
Cláudia Nalon is a professor at the Department of
Computer Science at the University of Brasília, Brazil. She obtained
her PhD from the University of Liverpool, in the UK, where she was
working in proof methods for interacting logics of time and knowledge.
Cláudia is interested in both the theoretical foundations and
implementation of reasoning tools. She has worked on the design and
mechanisation of calculi for several families of normal and non-normal
modal logics, and also finitely many-valued logics.
## Barriers to Entailment (Gillian Russell)
**Abstract**
A barrier thesis is something which says that there are no valid arguments with premises all of one kind and a conclusion of another. A famous example in philosophy is Hume’s Law, which says that you can’t get an *ought* from an *is*, or that no set of purely descriptive sentences entails a normative one. That barrier is controversial, but there are also platitudinous cases. For example, no universal conclusions from particular premises, or no claims about the future from claims about the past. This course will look at how to use model theory for appropriate logics to formulate and prove a number of philosophically interesting barrier theses.
**Prerequisites**
First-order logic. We will use other logics too, but these will be introduced as we go.
**Lecturer**
Gillian Russell is a professor in the school of philosophy at the ANU as well as a professorial fellow at the Arché Research Center at the University of St Andrews in Scotland. She’s originally from the UK, but taught in the US for two decades before fleeing to Australia in 2022.
**Lecture notes and resources**
[Click here for Gillian’s course page](https://gillianrussell.net/teaching/anu-logic-summer-school-2/)
## Modal Type Theories and Logical Relations (Vineet Rajani)
**Abstract**
This series of lectures will explore the fascinating world of modal type theories and their applications to reason about safety and hypersafety properties of higher-order programs. The lectures will begin by exploring Moggi’s computational lambda calculus as an elegant way to reason about effects using monads. We will understand the semantics of computational lambda calculus using the framework of logical relations. After that we will generalize the computational lambda calculus with graded modalities which will allow us to reason about quantitative safety properties like bounds on resource consumption (both worst case and amortized). We will also look at graded-modal type theories to reason about hypersafety properties, in particular those relevant to information flow and declassification. Logical relations will be a unifying theme in these lectures which will allow us to define semantics of all these type theories.
**Lecturer**
Vineet Rajani is a Senior lecturer in the School of Computer Science and Engineering at the University of New South Wales (UNSW) Sydney. Before joining UNSW, Vineet was a Lecturer at the University of Kent where he was affiliated with both the Programming languages and the Cyber security groups. Vineet joined Kent after finishing his PostDoc and PhD from the Max Planck Institute for - Security and Privacy, and Software Systems, respectively. Vineet’s interest lies in the development of formal and provably correct methods to reason about properties of computation, especially those pertaining to security and quantitative resource bounds. His work on secure information flow has won distinguished paper awards at premier venues of security foundations (CSF’18) and programming languages (POPL’19) research. More information about him can be found at: <https://vineetrajani.github.io>.