Weeknotes 2025-W45 [2025-W45]

This week was mostly occupied with various administrative catchups after my two weeks of leave.

Some nice sunsets near the Lyneham wetlands.

ITP course at the ANU Logic Summer School [loc-0028]

As I previously mentioned, I am teaching at the ANU Logic Summer School this year, on an introduction to interactive theorem proving using the proof assistant Isabelle. Here's the course blurb as found on the website:

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. Simplifier, rewriting, function definitions, other definitions.
  3. Structural induction, inductive definitions, induction tactics.
  4. Structured proofs in Isar, calculational proofs.
  5. 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

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.

I will also make the course notes available on this forest, as they are completed.

Syntax Highlighting in Forester for Isabelle (and More) [loc-0029]

Similar to my theme plugin for Gregorian Chants, I've implemented a simple plugin for syntax highlighted blocks using the Shiki library. Unlike the chant plugin, it doesn't self-host all the required JS but instead loads from a CDN. If this becomes problematic later I will investigate self-hosting it, but it seems that self-hosting Shiki is somewhat complicated.

I didn't use any other syntax-highlighting gizmos for Forester because I plan to write lecture notes for my upcoming course at the LSS and this would require me to support Isabelle code. The advantage of Shiki is that it supports textMate grammars, and Gerwin Klein made one for Isabelle.

Like the chant plugin, it consists of a single drop-in module of JavaScript, some changes to the stylesheet and a macro definition tree. As can be seen below, the results are quite nice:

theory Main imports Pure begin typedecl bool judgment Trueprop :: ‹bool ⇒ prop› ("(_)" 5) axiomatization False :: ‹bool› and True :: ‹bool› and conj :: ‹bool ⇒ bool ⇒ bool› (infixr "∧" 35) and disj :: ‹bool ⇒ bool ⇒ bool› (infixr "∨" 30) and implies :: ‹bool ⇒ bool ⇒ bool› (infixr "⟶" 25) and not :: ‹bool ⇒ bool› ("¬ _" [40] 40) where (* Conjunction *) conjI : "⟦ A ; B ⟧ ⟹ (A ∧ B)" and conjunct1 : "A ∧ B ⟹ A" and conjunct2 : "A ∧ B ⟹ B" end

(If it doesn't display correctly, you may need to clear your browser cache.)

Church Music Corner › 22nd Sunday after Pentecost 2025 [loc-0027]

Intret orátio mea in conspéctu tuo: inclína aurem tuam ad precem meam Dómine.

This Sunday I directed our choir at All Saints Ainslie for Purcell's Thou Knowest, Lord:

Thou knowest, Lord, the secrets of our hearts:
Shut not, shut not thy merciful ears unto our prayer,
But spare us, Lord. Spare us, Lord most holy.
O God! O God most mighty! O holy and merciful Saviour,
Thou most worthy judge eternal,
Suffer us not, suffer us not at our last hour,
For any pains of death to fall from thee.
Amen.

We also had a brief meeting yesterday morning to discuss our future plans for the choir. We have some exciting music ahead, and some of us agreed to sing at a special service at Goodwin Retirement Living for the residents there during Advent. Next year at the church, we plan to have semi-regular concerts, and I will also be forming a small group to sing regular Evensong services.

References

    Reference. Type Systems For Systems Types [oconnor-thesis-2019]

    Context

      Liam O'Connor › Weeknotes [loc-001B]