2026 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.

Prerequisites

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.

Foundations (Plural) of Mathematics
(Ranald Clouston)

Abstract

A foundation of mathematics is a small collection of assumptions and inference rules from which general mathematics can be derived. Study of these foundations might be motivated by mathematical curiosity; concern about inconsistencies and paradoxes; a search for a fruitful language for thinking about mathematics with; interest in weaker or non-standard approaches to mathematics; or the expression of mathematics in a style that a computer can check, or even manipulate creatively. These diverse motivations have led to diverse suggestions for what a suitable foundation of mathematics might be. In this lecture series we encourage students to embrace the diversity, and celebrate the fact that mathematics can be viewed through many foundational prisms.

We will give a whistle stop tour through the axiomatic style of mathematics; Dedekind and Peano’s foundations of arithmetic; set theory; category theory and topoi; and type theory and other foundations for the software used for mechanised mathematics. We will prioritise flavor and breadth over depth and rigour, but will take time to admire the oddities and apparent paradoxes thrown up by this foundational research, such as the puzzles posed by the Axiom of Choice and the Continuum Hypothesis.

References

  • Bunn, Robert. “Developments in the Foundations of Mathematics, 1870–1910.” In Ivor Grattan-Guiness, ed. “From the Calculus to Set Theory, 1630-1910”, (1980): pp 220-255.
  • Cohen, Paul J. “Set Theory and the Continuum Hypothesis” (1966).
  • Goldblatt, Robert. “Topoi: the categorial analysis of logic”. Vol. 98 of “Studies of Logic and the Foundations of Mathematics”, (1984).
  • Hofmann, Martin. “Syntax and Semantics of Dependent Types”. In: Andrew M. Pitts and Peter Dybjer, eds. “Semantics and Logics of Computation”, (1997): pp 79-130.
  • Shulman, Michael. “Complementary foundations for mathematics: when do we choose?” Talk presented at the The Joint Mathematics Meetings (2022): (https://home.sandiego.edu/~shulman/papers/jmm2022-complementary.pdf).

Lecturer

Ranald Clouston attended the ANU Summer School as a student back in 2003 while studying at Victoria University of Wellington in New Zealand. Since then he has studied at the University of Cambridge and worked at Aarhus University and Australian National University, his current home. His research concerns types, proofs, and models of logic.

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.

Introduction to CTL Model Checking
(Peter Höfner)

Abstract

It is virtually impossible to guarantee correctness of a system, and in turn the absence of bugs by standard software engineering practice such as code review, systematic testing and good software design alone. The complexity of systems is typically too high to be manageable by informal reasoning or reasoning that is not tool supported. The formal methods community has developed various rigorous, mathematically sound techniques and tools that allow the automatic analysis of systems and software. The application of these fully automatic techniques is typically called algorithmic verification. The course will describe one famous automatic verification technique, the algorithms they are based on, and the tools that support them.

The topics covered by the lectures will educate students on the foundations of computation tree logic (CTL) and CTL model checking techniques and model checking tools.

Prerequisites

Familiarity with predicate logic.

Background reading

  • Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9
  • Edmund Clarke, Orna Grumberg and Doron Peled. Model Checking. MIT Press, 2000.
  • Michael Huth and Mark Ryan. Logic in Computer Science (2nd edition). Cambridge University Press, 2004.
  • Beatrice Berard et al. Systems and Software Verification: Model-Checking Techniques and Tools. Springer, 2001

Lecturer

Dr Peter Höfner is a Professor at the Australian National University (ANU), which he joined in February 2020. He regularly serves as Acting Head of the School of Computing. Before joining ANU, he worked for nearly a decade as a (Principal) Research Scientist at Data61, CSIRO (formerly NICTA). In parallel, he held concurrent appointments as Conjoint Associate Professor at the University of New South Wales (UNSW) and Honorary Senior Research Fellow at Macquarie University. Earlier in his career, he was a Postdoctoral Fellow at the University of Augsburg, Germany. Peter’s research vision is to fundamentally transform the way real-world software systems are built and engineered; ensuring their trustworthiness to the highest possible degree, backed by mathematical proof.

Infinite Ramsey Theory and Logic
(Natasha Dobrinen)

Abstract

Ramsey’s Theorem was originally proved to solve a problem of formal logic, and in fact, he proved the infinite version first and then deduced the finite version from it. Ramsey’s Theorem for pairs states that given any coloring of pairs of natural numbers into finitely many colors, there is an infinite set of natural numbers in which all pairs have the same color.

The aims of this course are to (1) Prove Ramsey’s Theorem, (2) Extend Ramsey’s Theorem to other countable linear orders such as the integers and the rationals, (3) Introduce Ramsey theory where infinite subsets of the natural numbers are colored. Topic (2) covers what is called ``big Ramsey degrees” and will include connections with some Ramsey theorems on trees and a question regarding the strength of the Axiom of Choice. Topic (3) will include how the Axiom of Choice creates a barrier to direct analogues of Ramsey’s Theorem for colorings of infinite sets, and the work-around using Borel sets. I will include some informal discussions of the method of forcing, and if time permits, we will give a proof of the Galvin-Prikry Theorem using combinatorial forcing.

Prerequisites

Countable ordinals, transfinite induction on countable ordinals, Axiom of Choice (to be delivered in Ranald Clouston’s week one lectures).

Lecturer

Natasha Dobrinen is a professor in the Mathematics Department at the University of Notre Dame. She is a set theorist whose work involves combinatorics, topology, and computability theory. Her development of new techniques to solve a longstanding open problem on Ramsey theory of the triangle-free Henson graph gave impetus to the current flourishing of the field of Big Ramsey Degrees and led to an invited address at the 2022 ICM. She is currently president of the Association for Symbolic Logic, a Coordinating Editor for the Annals of Pure and Applied Logic, and an Editor for the Notre Dame Journal of Formal Logic and the mathematics journal Order. Born and raised in San Francisco, she earned a bachelors from UC Berkeley in 1996 and a PhD from the University of Minnesota in 2001. She held postdocs at Penn State and at the KGRC in Vienna, and has spent cumulatively around a decade in various places in Europe.

Logical Relations: From Type Soundness to Compiler Correctness and Specification of ABIs
(Amal Ahmed)

Abstract

This series of lectures will introduce students to logical relations, a versatile proof method with a wide range of applications. We will begin by using logical relations to prove semantic type soundness for programming languages with increasingly advanced features, including recursive types, mutable references, and substructural types. These examples capture the essential ideas underlying the more sophisticated semantic models used to establish type soundness for languages such as ML and Rust.

We will then turn to using logical relations to establish compiler correctness. This requires first specifying a relation that captures semantic equivalence between terms in the compiler’s source and target languages, and then proving that the compiler preserves this relation.

Finally, we will explore a recent and perhaps less familiar application of logical relations: the formal specification of a language’s Application Binary Interface (ABI). An ABI specifies the interoperability rules for each of its target platforms, including properties such as data layout and calling conventions. Compliance with these rules is essential for safe execution and can also provide guarantees about resource usage. Unfortunately, ABIs are typically specified in prose, and while source-language type systems have grown considerably richer over the past several decades, ABI specifications have largely remained unchanged, lacking analogous advances in expressivity and semantic guarantees. We will discuss a novel methodology for formally specifying ABIs using realizability models – another instance of logical relations – that relate high-level source-language types to unwieldy, but well-behaved, low-level code. We will illustrate the approach through a case study, showing how it builds on two decades of progress in separation logics and semantic models to enable richer semantic ABIs that can capture properties such as resource ownership, borrowing, and sharing.

Lecturer

Amal’s research interests lie in correct and secure compilation across the software-hardware stack and safe language interoperability, including design of sound foreign-function interfaces (FFIs) and richly typed compiler intermediate languages to support safe mixing of code from different languages. Her work makes use of semantics and type systems for reasoning about imperative and probabilistic programming languages, multi-language systems, security, concurrency, compiler correctness, gradual typing, and provenance.

Proof Theory of Modal and Non-Classical Logics: the Method of Labelled Sequent Calculi
(Sara Negri)

Keywords

Proof theory; labelled sequent calculi; modal logic; intuitionistic logic; non-classical logics; Kripke and neighbourhood semantics; cut elimination; proof search, correspondence theory.

Abstract

The course introduces the proof-theoretic method of labelled sequent calculi, a uniform framework for developing analytic proof systems for modal and non-classical logics. We begin by examining the relationship between semantics and proof theory, showing how Kripke semantics can be internalized into sequent calculi by means of labels representing possible worlds and accessibility relations.

We then construct labelled calculi for the basic modal logic K and explain how semantic frame conditions can be systematically transformed into inference rules, yielding cut-free systems with strong structural properties. This methodology extends naturally to intuitionistic, intermediate, and other non-classical logics, providing a modular approach to proof search, countermodel construction, and completeness proofs.

Finally, we discuss recent developments that go beyond geometric frame conditions, including applications to epistemic, provability, and non-normal modal logics. Throughout the course, we emphasize how labelled calculi provide a common proof-theoretic language for studying analyticity, correspondence, decidability, and automated reasoning across a broad range of logical systems.

Prerequisites

Foundations of propositional and first-order logic. Prior knowledge of modal logic or proof theory is helpful but not required.

Lecturer

Sara Negri is Professor of Mathematical Logic at the University of Genoa and is internationally recognised for her contributions to proof theory, particularly in modal and non-classical logics. She is the author of the two monographs “Structural Proof Theory” and “Proof Analysis: A Contribution to Hilbert’s Last Problem” (both with Jan von Plato).

Before her current appointment, she served from 2015 as Professor of Theoretical Philosophy at the University of Helsinki and held research positions at the Academy of Finland and the Helsinki Collegium for Advanced Studies. Her visiting and postdoctoral appointments include the University of Amsterdam, Imperial College London, the Mittag-Leffler Institute in Stockholm, the University of Munich, the Hausdorff Research Institute for Mathematics in Bonn, the Scuola Normale Superiore in Pisa, and the University of Verona. She is a member of the Academia Europaea.

Proofs as Part of Programming
(K. Rustan M. Leino)

Abstract

These lectures show how specifications and proofs can be a natural part of programming. The main goal is to teach how to write and verify programs in a practical setting. Using the Dafny programming language, we will start with the basics of pre- and postconditions and invariants. As programs become more involved, we will need abstraction and proofs. I will show various styles of proofs. Going beyond executable programs, we will also see how the same proof setting extends to the formalization of models of systems.

Lecturer

K. Rustan M. Leino is known for his work on programming languages and programming methods and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.

Leino is a research engineer at Harmonic. Previously, he has been Senior Principal Applied Scientist at Amazon Web Services, co-instructor at MIT, Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and researcher at DEC/Compaq Systems Research Center (SRC). He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.

Leino hosts the Verification Corner channel on youtube. He is a multi-instrumentalist, he instructed group cardio and strength classes for many years, and he likes to cook.

Algorithmic Information Theory
(Rod Downey)

Abstract

Given a binary string σ how much information does it contain? How much can it be compressed? For infinite sequences, why do we think that 0101010101 . . . does not look random whereas others do, although both have the same probability of occurring, namely 0? How should we formalize such questions?

There is a deep and interesting of algorithmic information theory or algorithmic randomness where a notion of absolute randomness is abandoned and replaced by one which uses the theores of computation and of computational complexity to calibrate or quantify randomness. This leads to notions of randomness of individual strings and reals.

Questions include: What kinds of computational power does having access to random sources give us? What complexity is needed to construct an algorithmicially random source? Can I use a notion of randomness for individual objects to prove classical theorems in mathematics or computer science?

This course will deal with the basics of this theory. Some background reading might include delving into [LV93, Nie09, DH10, Dow08, DH19] or articles from my homepage.

References

[DH10] Rodney Downey and Denis Hirschfeldt. Algorithmic randomness and complexity. Theory and Applications of Computability. Springer, New York, 2010. [DH19] R. Downey and D. Hirschfeldt. Computability and randomness. Notices of the American Mathematical Society, 66(7):1001–1012, 2019. [Dow08] R. Downey. Five lectures on algorithmic randomness. In C. Chong, Q. Feng, T. Slaman, W. Woodin, and Y. Yang, editors, Computational Prospects of Infinity, Part I: Tutorials, pages 3–82. World Scientific, 2008. [LV93] Ming Li and Paul Vitanyi. An introduction to Kolmogorov Complexity and its Applications. Texts and Monographs in Computer Science. Springer-Verlag, 1993. [Nie09] André Nies. Computability and Randomness, volume 51 of Oxford Logic Guides. Oxford University Press, Oxford, 2009.

Lecturer

Professor Rod Downey is based in Victoria University, Wellington, New Zealand. He works in computational complexity and mathematical logic, particularly the theory of computation. With Mike Fellows, he is known for founding the area of parameterized complexity, and he is known for his work calibrating the computational aspects of algebra, analysis and algorithmic randomness. These are all areas whose roots go back to Turing’s seminal 1936 paper, so we see repercussions today. This direct line can be seen in Downey’s edited volume Turing’s Legacy. Downey has published some 300 research papers, 7 monographs and edits 7 journals. He has won many prizes for his work including a Rutherford Prize (New Zealand’s Premier Award), a Humboldt Research Prize, Barry Cooper Prize and most recently a Kalman Best Paper Prize. He has given and invited lecture at the International Congress of Mathematicians, is New Zealand’s only Fellow of the Association for Computing Machinery, and is a Fellow of several other academies including the American Mathematical Society, Australian Mathematical Society, and the New Zealand Royal Society.

bars magnifying-glass xmark