2022 Program
Week 1
- Fundamentals of Metalogic, Michael Norrish
- Computability and Incompleteness, John Slaney
- Modal Logic, Jim de Groot
- Logic for Verification, Nisansala Yatapanage
Week 2
- Information Security and Probabilistic Programming, Annabelle McIver
- Interactive Theorem Provers and Cryptography, Thomas Haines
- Propositions and Types, Proofs and Programs, Ranald Clouston
- Category Theory and Categorical Logic, Dirk Pattinson (added)
- Sequent Calculi: Positive and Negative Results in Universal Proof Theory, Rosalie Iemhoff
- Verification via Temporal Logic: an Introduction, Mark Reynolds (cancelled)
Fundamentals of Metalogic
(Michael Norrish)
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 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
Computability and Incompleteness
(John Slaney)
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 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.
Slides
Modal Logic (Jim de Groot)
Keywords Normal modal logic, possible-world semantics, bisimulations, Hennessy-Milner theorem, Van Benthem characterisation theorem.
Abstract Modal logic lies in between propositional logic and first order logic. It is widely used in mathematics, philosophy and computer science. On the one hand it can be used to reason about more complex statements concerning necessity, knowledge and obligation, while on the other hand it is simple enough to still be decidable.
The goal of this course is to explore modal logic, and to characterise the precise relation between modal logic and first-order logic. We do so by taking a semantic point of view, interpreting formulae in so-called possible world semantics. We then introduce bisimulations, which can be used to identify worlds in which precisely the same formulae are true. Ultimately we prove the Van Benthem characterisation theorem, which (intuitively) states that modal logic is the bisimulation-invariant fragment of first-order logic.
Pre-requisites Mathematical maturity and some familiarity with propositional and first-order logic.
Background reading I’ll use parts of “Modal Logic” by Blackburn, de Rijke and Venema. I can indicate more precisely which parts later.
Lecturer My name is Jim and I’ll be telling you about modal logic in the summerschool. I was born and raised in Amsterdam, and studied mathematics there. Recently I submitted my PhD in mathematical logic here at the ANU, and I’m now trying to learn about (the logic behind) protocol verification. In my spare time I like to go hiking and camping in the beautiful national parks surrounding Canberra.
Slides
Logic for Verification (Nisansala Yatapanage)
Keywords
Abstract This course will give students an introduction to using logic for program verification. Verification is essential, in order to ensure that a program is correct according to its specification. Verification allows us to prove the absence of errors, unlike testing. This course covers two main approaches for verification: temporal logic and program reasoning.
The topic of temporal logic covers linear time and branching time logics (LTL, CTL and CTL*), transition systems and model checking. Model checking will be demonstrated using an interesting case study. The program reasoning part of the course covers Hoare logic and Rely/Guarantee reasoning, which is a useful method for reasoning about concurrency.
Pre-requisites Students should be comfortable with first-order logic.
Lecturer Nisansala Yatapanage is a lecturer at ANU. Her research interests are in formal methods for the verification of concurrent and safety-critical systems. She started research in formal methods in 2004 on a joint project with The University of Queensland and Griffith University, working on using Behavior Tree specifications and model checking to perform failure analyses on safety-critical systems. She loved it so much that she continued the topic for her PhD and also worked on an industry project applying the techniques to an air-traffic control system. She then worked in the U.K. at Newcastle University researching concurrency verification using rely/guarantee reasoning, and was a lecturer at De Montfort University in Leicester, before returning to Australia to work at ANU. More details can be found on her website: https://users.cecs.anu.edu.au/~u1102274/
Slides Available here.
Modelling and analysis of information security using probabilistic programming (Annabelle McIver)
Keywords
Abstract Security systems that access confidential information often incorporate mechanisms in their design to control information “leaks”. For many applications though it has been found that qualitative formal specifications of these controls are too strong (i.e. they cannot be satisfied on real implementations). Quantitative specifications which allow “insignificant leaks” are appropriate in these circumstances.
In these lectures a model for quantitative information flow will be introduced, and its mathematical properties explored. The topics covered will include information leakage measurements, robustness theorems, security partial orders. This information flow model can be used to provide a “security aware” formal semantics for programming languages enabling formal analysis and diagnosis of information breaches in programs.
Pre-requisites
Background reading
Lecturer
Slides
Interactive Theorem Provers and Cryptography
(Thomas Haines)
Keywords cryptography, interactive theorem provers; easycrypt; encryption; commitments
Abstract This course will introduce several fundamental cryptographic primitives and examples of situations in which they are useful. We will rigorously define what the primitives are and what it means for them to be secure in the interactive theorem prover easycrypt. We will then code various instantiations of these primitives and prove to the interactive theorem prover that they are secure. The main primitives analysed will be commitment schemes and encryption schemes. The aim of this course is to give a basic understanding of how cryptography can provide formal security guarantees and how those guarantees can be checked by interactive theorem provers.
Pre-requisites Basic abstract algebra
Background reading D. Boneh and V. Shoup, A Graduate Course in Applied Cryptography
Lecturer Thomas Haines is an applied cryptographer specialising in the security of distributed systems. After completing his PhD in 2017, he worked as a research and development manager at Polyas GmbH in Berlin. While at Polyas he was responsible for development of electronic voting solutions, including design, implementation, documentation and certification. Thomas was a research fellow at the Norwegian university of Science and Technology before joining ANU in 2021. He has been involved with auditing over a dozen different electronic voting systems.
Sequent Calculi: Positive and negative results in universal proof theory (Rosalie Iemhoff)
Abstract Sequent calculi are a particular form of proof systems that are important both from a conceptual and a technical point of view. They give insight in the reasoning that can be carried out in the logic corresponding to the calculus, and they can be an important tool is establishing that a logic has certain properties, such as decidability or interpolation. As such, they occur in various areas in logic, mathematics, philosophy, computer science, and linguistics.
This course consists of (1) a brief introduction into sequent calculi, (2) ex- amples of the many positive results showing that various well-known logics have sequent calculi with good properties, followed by (3) the negative results in the area, in which methods to establish that certain logics do not have certain good sequent calculi will be discussed, and one particular method will be developed in some detail.
Part (2) and (3) clearly depend on what is considered a “good” calculus, which again depends on the applications that one has in mind for the proof system, an issue that will be addressed during the course as well.
Lecturer https://www.uu.nl/staff/RIemhoff/
Slides
Verification via Temporal Logic: an Introduction (Mark Reynolds)
Keywords
Abstract In this series of five lectures we have a look at how temporal logic has been used in formal verification of the behaviour of systems. We introduce some simple propositional temporal logics, linear time LTL and branching time CTL, and consider algorithms for determining satisfiability and model checking. If time permits we will have a quick look at some extensions.
Pre-requisites
Background reading
Lecturer Mark Reynolds obtained his Bachelors degree at The University of Western Australia (UWA) with honours in Pure Mathematics and Statistics, his PhD at Imperial College London (IC) in Computing and a Diploma in Education from UWA. After lecturing at Kings College London, he moved back to Perth and then to UWA as an Associate Professor. He is currently the head of the School of Physics, Mathematics and Computing. His research interests include AI, Machine Learning, Logic, Formal methods in Software Engineering and Optimisation. (See https://research-repository.uwa.edu.au/en/persons/mark-reynolds)
Slides
Propositions and Types, Proofs and Programs (Ranald Clouston)
Keywords Intuitionistic logic; Natural deduction; Curry-Howard isomorphism; Type theory; Lambda calculus
Abstract Intuitionism is an approach to logic that began with some renegade ideas in the philosophy of mathematics, but has since been enthusiastically adopted by computer scientists. We begin with an introduction to intuitionistic propositional logic, including its possible world semantics, then show that we can reason with it in a structured way via ‘natural deduction’. We briefly discuss the relationship between natural deduction and sequent calculus. We then unveil the Curry-Howard isomorphism, also known as propositions-as-types, which makes a surprising connection between logic and the simply typed lambda calculus, a functional programming language. We discuss some of the major features of this programming language / proof system, such as subject reduction, strong normalisation, and the subformula property. We see how the Curry-Howard isomorphism can be pushed further into more powerful logics and programming language features, such as arithmetic, polymorphism, and dependent types.
Pre-requisites Michael Norrish and Jim de Groot’s courses in week 1
Background reading
Phillip Wadler, ‘Propositions as Types’ https://dl.acm.org/doi/10.1145/2699407; Jean-Yves Girard, ‘Proofs and Types’ https://www.paultaylor.eu/stable/Proofs+Types
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 completed his PhD at the University of Cambridge and worked at Aarhus University and Australian National University, his current home. He researches in the areas of type theory and proof theory, which are to some extent the same thing, with occasional splashes of category theory.
Slides
- Part I: Intuitionistic Logic
- Part II: Natural Deduction
- Part III: Lambda Calculus
- Part IV: Curry-Howard (updated)
- Part V: Extensions