Following the near-death of Aussie PL last decade I think we’ve gotten in the habit of thinking that Aussie PL is this tiny embattled community with only essential activities, but thinking about the environment in Scotland and comparing it, I don’t think there is actually much truth to that. Scotland has events like SPLV; we have (e.g.) the logic summer school. Scotland has the SPL seminar; We have SAPLING. SPLI applies for large CDT grants, we apply for large CoE grants (and both get rejected :). What’s missing is the network of folks in various places, who can advertise seminars when people are visiting, who can arrange visits and cross-institutional collaboration etc.

This network started in Scotland with the SPLS Zulip, which eventually evolved into the more formal organisation, the Scottish Programming Languages Institute. I think it would be nice to foster that kind of active cross-institutional community that has worked well in Scotland, and Zulip is a huge part of why the SPLI exists now.

To this end, I have started the AusPL Zulip, specifically targeting researchers and students in programming languages, formal methods, software engineering, and related areas in Australian institutions (and surrounding countries). Please consider signing up!

Join Here!

I have begun the redevelopment of Holbert I envisioned earlier, dubbed Holbert NG. The initial results are already on GitHub, implemented in a combination of ReScript and TypeScript — mostly ReScript. ReScript is essentially a dialect of OCaml designed to target JavaScript with fairly complete React bindings. The design is already significantly more flexible than the original Haskell design of Holbert, largely due to ReScript's full implementation of OCaml's module system. I've currently implemented a basic first order proof checker with textual formats, and a components library in TypeScript enabling multi-page documents and sychronisation to local storage.

What I haven't really started work on is the UI part. I'm letting this percolate for a while before I start tackling it. I was never happy with the rule editing UI in classic Holbert — it was always too clunky, and more cumbersome than just editing a text-based format. This is in stark contrast to the editor for proofs, which offered some advantages over text. As Holbert NG has text formats for everything, I currently haven't developed GUI editors, but this will eventually change.

Mostly this implementation effort has been a way for me to trial ReScript and its associated React ecosystem. My initial thoughts, as I posted on Mastodon, were:

1. Love ML modules despite their clunkiness. Quite handy for the Holbert-NG design where proof methods can be written as seperate plugins and integrated. Even the term language is swappable.
2. Dislike the tendency of the community (and the gearing of the language syntax) towards depending on type inference. Return types in particular usually omitted. In this respect I prefer Haskell syntax.
3. Related to 2, it really needs some kind of "dot" syntax. If I have an x : Foo.t and I go x->blah(..)->baz(..) it should try to desugar to x->Foo.blah(..)->Foo.baz(..). This is not feasible because the type of x would become too ambiguous because of 2. So Module.I Module.end Module.up Module.qualifying Module.everything...
4. ReScript in particular has a more "C" style syntax and gets rid of some of the traditional FP stuff from OCaml. I haven't found myself missing it hugely, but occasionally the JS API's available are annoyingly mutation-heavy. This is understandable for ReScript's aims (to generate readable JS) but it can be a pain to work around.

By writing a small JS module that uses Web Components and the exsurge library, I have developed a small patch that can be dropped into Forester themes to enable rendering of Gregorian chants.

It also supports In(g)line(he) score(ffedc~) (::) rendering (although I don't know how useful that is), and will reflow scores as the width of the window changes.

This is already used to keep my arrangements of the reproaches verses and the Easter Proclamation which I performed during the Paschal Triduum of 2025.

I wrote all my reviews for APLAS 2025 this week. APLAS was the first conference I ever attended, and I remain quite fond of the Asia-Pacific PL community. All of the papers I reviewed were interesting. I am also hopeful about our own submission: Selene, a PhD student of Christine Rizkallah, has been pursuing a research agenda with several collaborators relating the uniqueness types of, say, Cogent with the program-logic driven approaches of, say, Separation Logic, based on a short abstract I wrote and submitted with her to VIMPL 2023. This work has culminated in our APLAS submission.

Now that DECRA (an early-career research grant in Australia) assessments are back, I am busy working on my rejoinder. It really is a soul-crushing part of the job, but a lot of the feedback I got (from the unusually numerous 6 assessors!) was very positive. This will be the last time I can apply for the DECRA, as I will not be eligible in future and the DECRA may not exist.

In our weekly meeting, Yi Yao, Peter Höfner and I were examining a paper by Vincent Mathieu and Jules Desharnais about verification of pushdown systems using \omega -algebras with domain. One thing that we got hung up on was that the underlying algebra seems to insist that the underlying set be of mixed type, where control actions (i.e. the labels on transitions, or expected inputs to the automaton) are interleaved with stack actions (either pushing or popping symbols from the stack). The result is that a bunch of axioms must be added to deal with cancelling pushes and pops, and reordering actions to enable such cancellations.

Following a proposal from Peter Höfner, I formalised the following alternative algebra, which should work just as well as the algebra in the paper but avoids this extra complexity. Instead of having strings of mixed types of actions, we instead have our algebra consist of sets of triples, which includes a (possibly infinite) string of control actions, a (possibly infinite) initial stack, and a (possibly infinite) final stack. S \triangleq \mathcal {P}(A^\infty \times \Sigma ^\infty \times \Sigma ^\infty ) In our notation, A is the set of control actions, \Sigma is the set of stack symbols, and the {}^\infty superscript denotes both finite and infinite strings of elements, i.e. X^\infty = X^\ast \cup X^\omega .

These definitions are sufficient to show that (S, \cup ,\cdot , \emptyset , \mathbf {1}, {}^\ast ) is a Kleene algebra. Then, to extend this to an \omega -algebra, one needs only the {}^\omega operator.

One thing we noticed here is that it doesn't matter to the operators what the type of the stack is. Indeed, replace stacks with tapes and you'd get something describing actions on a turing machine. This gives us compelling directions to take this!

Suscépimus, Deus, misericórdiam tuam in médio templi tui: secúndum nomen tuum Deus, ita et laus tua in fines terræ: iustítia plena est déxtera tua.

While we were short on numbers, the choir of All Saints Ainslie performed the lovely We Wait for Thy Loving-kindness, O God by William McKie. I performed the brief tenor solo intonations. I notice as I write this that the text is the same as the introit for this Sunday, which I wrote above.

We wait for thy loving-kindness, O God, in the midst of thy temple.

Alleluia, Alleluia, Alleluia.

O God, according to thy name, so is thy praise unto the world's end.

Thy right hand is full of righteousness. Alleluia.

We wait for thy loving-kindness O God, in the midst of thy temple.

O Lord, send us now prosperity.

Amen.

As my parents were visiting I didn't end up making my way down to Manuka for Evensong today.