2025 Program

Week 1

Week 2


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

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

For links to resources for the Beagle theorem prover, see Peter’s homepage.

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.

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.

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

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

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

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

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

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

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.

bars search times arrow-up