my forest
start weeknotes
+191
-1
+1
-1
trees/loc-0002.tree
+1
-1
trees/loc-0002.tree
···
11
11
\subtree{
12
12
\title{Secondary supervisions}
13
13
\ul{
14
-
\li{ [[yiyao]]: 2025-present. Computer science applications of group theory and Cayley graphs. Primary supervisor is [[hoefner]] at the [[anu]]. }
14
+
\li{ [[yiyao]]: 2025-present. Unifying algebraic models of automata and computation. Primary supervisor is [[hoefner]] at the [[anu]]. }
15
15
\li{ [[tudor]]: 2021–present. Formal verification of smart contracts. Primary supervisor is [[wadler]] at the [[uoe]]. }
16
16
\li{ [[mathieu]]: 2022–present. DSLs for compiler passes. Primary supervisor is [[tgrosser]] at the [[cam]]. }
17
17
}
+20
trees/loc-0014.tree
+20
trees/loc-0014.tree
···
1
+
\title{Progress in Holbert: ReScript}
2
+
\date{2025-07-03}
3
+
\author{liamoc}
4
+
\p{I have begun the [redevelopment of Holbert](loc-000V) I envisioned earlier, dubbed Holbert NG. The initial results are [already on GitHub](https://github.com/liamoc/holbert-ng), implemented in a combination of [ReScript](https://rescript-lang.org) 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.}
5
+
\p{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. }
6
+
\p{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:}
7
+
\ol{
8
+
\li{
9
+
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.
10
+
}
11
+
\li{
12
+
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.
13
+
}
14
+
\li{
15
+
Related to 2, it really needs some kind of "dot" syntax. If I have an \code{x : Foo.t} and I go \code{x->blah(..)->baz(..)} it should try to desugar to \code{x->Foo.blah(..)->Foo.baz(..)}. This is not feasible because the type of \code{x} would become too ambiguous because of 2. So \code{Module.}I \code{Module.}end \code{Module.}up \code{Module.}qualifying \code{Module.}everything...
16
+
}
17
+
\li{
18
+
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.
19
+
}
20
+
}
+10
trees/loc-0015.tree
+10
trees/loc-0015.tree
···
1
+
\import{gabc-macros}
2
+
\title{Gregorian Chants in Forester}
3
+
\date{2025-07-03}
4
+
\author{liamoc}
5
+
\p{By writing a small JS module that uses [Web Components](https://developer.mozilla.org/en-US/docs/Web/API/Web_components) and the [exsurge](http://frmatthew.github.io/exsurge/chant.html) library, I have developed a small patch that can be dropped into Forester themes to enable rendering of Gregorian chants.}
6
+
\put\gabc/annotation{Intr. (2)}
7
+
\gabc{(f3) CI(c)BÁ(efe)VIT(f) e(fhf)os(efe) *(,) ex(f) á(h)di(hhh)pe(f) fru(e)mén(egf/ge)ti,(c) (,) al(eh~)le(hghf)lú(fgf)ia:(f) (:) et(e) de(f) pe(hh)tra,(hi~) mel(ih~)le(hihh/fgf) (,) sa(f)tu(fi)rá(ih)vit(h!ij) e(ih)os,(h) (;) al(hi~)le(i)lú(ihi)ia,(f) (,) al(g!hwi)le(ih)lú(hf/gvFE)ia,(fe) (,) al(f!gwh)le(hvGF/gwh/ig/hg)lú(fg!hvGFg)ia.(gf) (::) }
8
+
\p{
9
+
It also supports \gabcinline{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.}
10
+
\p{This is already used to keep my arrangements of the [reproaches verses](loc-0013) and the [Easter Proclamation](loc-0012) which I performed during the [Paschal Triduum of 2025](loc-000O).}
+5
trees/loc-0016.tree
+5
trees/loc-0016.tree
···
1
+
\import{gabc-macros}
2
+
\title{Reviewing and Program Committees}
3
+
\date{2025-07-03}
4
+
\author{liamoc}
5
+
\p{I wrote all my reviews for [APLAS 2025](aplas25) 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](selene), a PhD student of [Christine Rizkallah](crizkallah), has been pursuing a research agenda with several collaborators relating the uniqueness types of, say, [Cogent](cogent) with the program-logic driven approaches of, say, Separation Logic, based on a [short abstract](oconnor-linares-rizkallah-2023) I wrote and submitted with her to [VIMPL 2023](vimpl23). This work has culminated in our APLAS submission. }
+4
trees/loc-0017.tree
+4
trees/loc-0017.tree
···
1
+
\date{2025-07-03}
2
+
\author{liamoc}
3
+
\title{DECRA, Grants, etc.}
4
+
\p{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](https://www.arc.gov.au/engage-us/consultations/policy-review-national-competitive-grants-program/faqs).}
+62
trees/loc-0018.tree
+62
trees/loc-0018.tree
···
1
+
\import{dt-macros}
2
+
\date{2025-07-03}
3
+
\author{liamoc}
4
+
\title{#{\omega}-Algebra for pushdown actions?}
5
+
\p{
6
+
In our weekly meeting, [[yiyao]], [[hoefner]] and I were examining a [paper](mathieu-desharnais-2005) by Vincent Mathieu and [[jdesharnais]] 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.
7
+
}
8
+
\p{Following a proposal from [[hoefner]], 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 \em{triples}, which includes a (possibly infinite) string of control actions, a (possibly infinite) \em{initial stack}, and a (possibly infinite) \em{final stack}. ##{S \triangleq \mathcal{P}(A^\infty \times \Sigma^\infty \times \Sigma^\infty) }
9
+
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}. }
10
+
\subtree{
11
+
\taxon{Definition}
12
+
\title{Multiplication}
13
+
\p{
14
+
We define a sequential composition operator for triples as follows: ##{ (w_1,s_1,s'_1)\ \mathit{seq}\ (w_2,s_2,s'_2) = \begin{cases} (w_1w_2, s_1, s'_2) & \text{if}\ s'_1 = s_2 \\ \text{undefined} & \text{otherwise} \end{cases} }
15
+
Note that for sequential composition to make sense, the initial stack of the second triple must match the final stack of the first triple. As the words #{w_1} and #{w_2} may be infinite, we define concatenation in the usual way, where #{w_1w_2 = w_1} when #{w_1} is infinite.
16
+
}
17
+
\p{Then, the definition of multiplication in our algebra is the straightforward lifting to sets:}
18
+
##{
19
+
S_1 \cdot S_2 = \Set{ x\ \mathit{seq}\ y \mid x \in S_1, y \in S_2, x\ \mathit{seq}\ y\ \text{defined}}
20
+
}
21
+
22
+
}
23
+
\subtree{
24
+
\taxon{Definition}
25
+
\title{The Unit Element}
26
+
\p{The 1 element for multiplication here just consists of all triples with an empty word that leave the stack unchanged:}
27
+
##{
28
+
\mathbf{1} = \Set{ (\varepsilon, s, s) \mid s \in \Sigma^\infty }
29
+
}
30
+
31
+
}
32
+
\subtree{
33
+
\taxon{Definition}
34
+
\title{The Kleene Star}
35
+
\p{Let #{S^n} denote the #{n}-times self-multiplication of #{S}, where #{S^0 = \mathbf{1}}. Then, the Kleene star for our algebra is:}
36
+
##{S^\ast \triangleq \bigcup_{n \in \mathbb{N}}\ S^n}
37
+
38
+
}
39
+
\p{
40
+
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.
41
+
42
+
\subtree{
43
+
\taxon{Definition}
44
+
\title{The Omega Operator}
45
+
\p{
46
+
We define the #{{}^\omega} operator as follows:
47
+
##{
48
+
S^\omega \triangleq \Set{ (w, s_1, s_2) \mid \exists \text{an infinite run for}\ w\ \text{in}\ S\ \text{starting with stack}\ s_1}
49
+
}
50
+
The above definition feels informal, so we will define momentarily a judgment or predicate #{S \vdash (w,s_1)\ \textbf{infinite} }, which means the same thing:}
51
+
##{
52
+
S^\omega \triangleq \Set{ (w, s_1, s_2) \mid S \vdash (w,s_1)\ \textbf{infinite}}
53
+
}
54
+
\p{Note that this definition places no constraint on #{s_2}, so any non-empty set #{S^\omega} will include all possible final stacks.}
55
+
\p{It remains to formalise our predicate. Formally, it is the largest (i.e. coinductive) predicate satisfying the following rule: }
56
+
##{\dfrac{w = xw' \quad (x,s_1,s_2) \in S \quad S \vdash (w',s_2)\ \textbf{infinite}}{S \vdash (w,s_1)\ \textbf{infinite}}}
57
+
\p{This means we can prove #{S \vdash (w,s_1)\ \textbf{infinite}} if we can find an infinite chain of moves in #{S} starting with stack #{s_1} that, when all combined, results in the word #{w}.}
58
+
\p{Note that while the run is infinitely long, the word #{w} need not be, due to the presence of #{\varepsilon}-moves. }
59
+
}
60
+
61
+
62
+
}
+30
trees/loc-0019.tree
+30
trees/loc-0019.tree
···
1
+
\import{table-macros}
2
+
\def\percent{\startverb%\stopverb
3
+
}
4
+
\parent{loc-000P}
5
+
\title{4th Sunday After Pentecost 2025}
6
+
\tag{cmc}
7
+
\date{2025-07-06}
8
+
\author{liamoc}
9
+
\quote{
10
+
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.
11
+
}
12
+
\p{While we were short on numbers, the choir of [All Saints Ainslie](https://allsaintsainslie.org.au), performed the lovely [We Wait for Thy Loving-kindness, O God](https://www.youtube.com/watch?v=YDB77SDWrII) 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.}
13
+
\quote{
14
+
\poem{
15
+
\line{
16
+
We wait for thy loving-kindness, O God, in the midst of thy temple.}
17
+
\line{
18
+
Alleluia, Alleluia, Alleluia.}
19
+
\line{
20
+
O God, according to thy name, so is thy praise unto the world's end.}
21
+
\line{
22
+
Thy right hand is full of righteousness. Alleluia.}
23
+
\line{
24
+
We wait for thy loving-kindness O God, in the midst of thy temple.}
25
+
\line{
26
+
O Lord, send us now prosperity.}
27
+
\line{
28
+
Amen.}
29
+
}
30
+
}
+7
trees/people/jdesharnais.tree
+7
trees/people/jdesharnais.tree
+7
trees/people/selene.tree
+7
trees/people/selene.tree
···
1
+
\title{Pilar Selene Linares Arévalo}
2
+
\taxon{Person}
3
+
\meta{external}{https://cis.unimelb.edu.au/research/computer-science/cs-graduate-researchers/computer-science/pilar-selene-linares-arevalo}
4
+
\meta{institution}{[[unimelb]]}
5
+
\meta{orcid}{0000-0001-8884-618X}
6
+
\meta{position}{PhD student}
7
+
\p{Supervised by [[crizkallah]].}
+4
trees/places/laval.tree
+4
trees/places/laval.tree
+7
trees/places/relmics05.tree
+7
trees/places/relmics05.tree
+7
trees/places/vimpl23.tree
+7
trees/places/vimpl23.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{Conference}
3
+
\title{\conf-name{VIMPL '23}{Value Independence in Modern Programming Languages}}
4
+
\date{2023-03}
5
+
\meta{venue}{Tokyo, Japan}
6
+
\meta{external}{https://2023.programming-conference.org/home/vimpl-2023}
7
+
\p{Colocated with the conference associated with [[programming-journal]] journal.}
+7
trees/refs/mathieu-desharnais-2005.tree
+7
trees/refs/mathieu-desharnais-2005.tree
+10
trees/refs/oconnor-linares-rizkallah-2023.tree
+10
trees/refs/oconnor-linares-rizkallah-2023.tree
···
1
+
\title{Uniqueness is Separation}
2
+
\taxon{Reference}
3
+
\meta{venue}{[[vimpl23]]}
4
+
\author{liamoc}
5
+
\author{selene}
6
+
\author{crizkallah}
7
+
\meta{external}{https://people.eng.unimelb.edu.au/rizkallahc/publications/vimpl-uniqueness-separation.pdf}
8
+
\p{Value independence is enormously beneficial for reasoning about software systems at scale. These benefits carry over into the world of formal verification. Reasoning about programs algebraically is a simple affair in a proof assistant, whereas programs with unconstrained mutation necessitate much more complex techniques, such as Separation Logic, where invariants about memory safety, aliasing, and state changes must be established by manual proof.}
9
+
10
+
\p{Uniqueness type systems allow programs to be compiled to code that uses mutation for efficiency, while retaining a semantics that enjoys value independence for reasoning. The restrictions of these type systems, however, are often too onerous for realistic software. Thus, most uniqueness type systems include some “escape hatch” where the benefits of value independence for reasoning are lost, but the restrictions of uniqueness types are lifted. To formally verify a system with such mixed guarantees, the value independence guarantees from uniqueness types must be expressed in terms of imperative, mutable semantics. In other words, we ought to express value independence as an assertion in Separation Logic.}
+10
trees/weeknotes/2025-W27.tree
+10
trees/weeknotes/2025-W27.tree
···
1
+
\title{Weeknotes 2025-W27}
2
+
\author{liamoc}
3
+
\date{2025-07-06}
4
+
\p{I decided to try out the Weeknotes idea, that I first saw from [[jonsterling]]. This was a pretty full week, ending with the somewhat devastating news that dozens of academic and professional positions will be gutted from, among others, the College of Arts and Social Sciences at the [[anu]]. I hear that Music will in particular be sorely affected. My heart goes out to all my colleagues and I hope that all of their futures are bright. }
5
+
\transclude{loc-0014}
6
+
\transclude{loc-0015}
7
+
\transclude{loc-0016}
8
+
\transclude{loc-0017}
9
+
\transclude{loc-0018}
10
+
\transclude{loc-0019}