my forest
adding ifip note, pushing old weeknotes.
+191
-3
assets/vdc01.jpeg
assets/vdc01.jpeg
This is a binary file and will not be displayed.
assets/vdc02.jpeg
assets/vdc02.jpeg
This is a binary file and will not be displayed.
assets/vdc03.jpeg
assets/vdc03.jpeg
This is a binary file and will not be displayed.
assets/vdc04.jpeg
assets/vdc04.jpeg
This is a binary file and will not be displayed.
assets/vdc05.jpeg
assets/vdc05.jpeg
This is a binary file and will not be displayed.
assets/vdc06.jpeg
assets/vdc06.jpeg
This is a binary file and will not be displayed.
assets/vdc07.jpeg
assets/vdc07.jpeg
This is a binary file and will not be displayed.
assets/vdc08.jpeg
assets/vdc08.jpeg
This is a binary file and will not be displayed.
assets/vdc09.jpeg
assets/vdc09.jpeg
This is a binary file and will not be displayed.
+1
-1
trees/loc-0002.tree
+1
-1
trees/loc-0002.tree
···
29
29
\title{Bachelors students}
30
30
\ul{
31
31
\li{[[miowu]]: 2025-2026, [[anu]]. \em{Pattern Unification in the Next Generation of the Holbert Proof Assistant}}
32
-
\li{[[joshbrown]]: 2025-2026, [[anu]]. \em{The Next Generation of the Holbert Proof Assistant}}
32
+
\li{[[joshbrown]]: 2025-2026, [[anu]]. \em{String Unification in the Next Generation of the Holbert Proof Assistant}}
33
33
\li{[[jackb]]: 2025, [[anu]] Semester Project. \em{A File Format for Holbert Proofs.}}
34
34
\li{[[sandwichman]]: 2023-2024, [[uoe]]. \em{Concurrent Games in Agda.}}
35
35
\li{[[sandwichman]]: 2023, [[uoe]] LFCS Internship Project. \em{Branching Bisimulation Games in Agda.}}
+1
-1
trees/loc-0003.tree
+1
-1
trees/loc-0003.tree
···
2
2
\parent{loc-0004}
3
3
4
4
\ul{
5
-
\li{ Observer, [[wg21]], 2024–present.}
5
+
\li{ Member, [[wg21]], 2025–present (observer from 2024–2025).}
6
6
\li{ Organiser, [[icfpc25]], 2025. }
7
7
\li{ Editor (Social Media), [[jfp]], 2020–present. }
8
8
\li{ Member at Large, [[tyde]] Steering Committee, 2022–2024. }
+1
trees/loc-001B.tree
+1
trees/loc-001B.tree
+23
trees/loc-001T.tree
+23
trees/loc-001T.tree
···
1
+
\date{2025-08-31}
2
+
\author{liamoc}
3
+
\import{table-macros}
4
+
\def\percent{\startverb%\stopverb
5
+
}
6
+
\parent{loc-000P}
7
+
\title{12th Sunday after Pentecost 2025}
8
+
\tag{cmc}
9
+
\quote{
10
+
Miserére mihi Dómine, quóniam ad te clamávi tota die: quia tu Dómine suávis ac mitis es, et copiósus in misericórdia ómnibus invocántibus te.
11
+
}
12
+
\p{Today our choir at [All Saints Ainslie](https://allsaintsainslie.org.au) were about two to a part for Palestrina's well-known [Sicut Cervus](https://www.youtube.com/watch?v=dU7k-hiiVjw):}
13
+
\quote{
14
+
\table{
15
+
\tr{
16
+
\td{Sicut cervus desíderat ad fontes aquárum:}
17
+
\td{Like as the hart desireth the waterbrooks:}
18
+
}\tr{
19
+
\td{ita desíderat ánima mea ad te, Deus.}
20
+
\td{So longeth my soul after thee, O God.}
21
+
}
22
+
}
23
+
}
+33
trees/loc-001U.tree
+33
trees/loc-001U.tree
···
1
+
\import{table-macros}
2
+
\date{2025-09-16T11:06:37Z}
3
+
\author{liamoc}
4
+
\title{IFIP WG2.1 Meeting \startverb #\stopverb83}
5
+
\figure{
6
+
\<html:img>[width]{200px}[src]{\route-asset{assets/vdc01.jpeg}}{}
7
+
\<html:img>[width]{200px}[src]{\route-asset{assets/vdc02.jpeg}}{}
8
+
\<html:img>[width]{200px}[src]{\route-asset{assets/vdc03.jpeg}}{}
9
+
% \figcaption{The squawking cockatoos on the walk from my lecture theatre.}
10
+
}
11
+
\p{Last week I attended the meeting of [[wg21]] in Viana do Castelo, Portugal. I think all members and observers agreed that it was a good meeting, with (perhaps overly) abundant food and good company. Thanks in particular to [[jno]] for organising the meeting and to [[hoefner]] for serving as chair of [WG2.1](wg21) for the last six years.
12
+
}
13
+
\p{Because this was my third meeting as an observer, I was eligible to be selected as an ongoing member of the group, and I'm happy to say that I was invited to become a member at the conclusion of this meeting. }
14
+
\p{I presented some new work my student [Rayhana](rayhana) and I did with [[rvg]], classifying monitorability classes topologically.}
15
+
\transclude{oconnor-2025-wg21}
16
+
\p{This was the sequel of sorts to my [prior WG2.1 talk](oconnor-2024-wg21-2) on LTL properties within finite time, which was in turn presenting work from [our EXPRESS/SOS paper](amjad-vanglabbeek-oconnor-2024) last year. The topological connection was realised thanks to [[nickwu]], also a WG2.1 member, who pointed out in [the Canberra meeting](oconnor-2024-wg21-2) that the work I was presenting had distinct notes of [domain theory](dt-001Y). The topological connection was more that of [Alpern and Schneider](alpern-schneider-1985) than [Scott](danascott), but that was the spark that drove this later work, which will hopefully be included in our forthcoming Information and Computation paper. }
17
+
\figure{
18
+
\<html:img>[width]{230px}[src]{\route-asset{assets/vdc04.jpeg}}{}
19
+
\<html:img>[width]{230px}[src]{\route-asset{assets/vdc05.jpeg}}{}
20
+
\figcaption{Views of Spain from the Camarido Beach.}
21
+
}
22
+
\p{The excursion of the meeting included several stops, including two interesting Viana museums, an archaelogical site on the nearby mountaintop, and a memorable trip to Camarido Beach, at the northernmost tip of Portugal, with Spanish Galicia just to the north along the road from Portugal to Santiago de Compostela.}
23
+
\figure{
24
+
\<html:img>[width]{202px}[src]{\route-asset{assets/vdc07.jpeg}}{}
25
+
\<html:img>[width]{202px}[src]{\route-asset{assets/vdc06.jpeg}}{}
26
+
\<html:img>[width]{202px}[src]{\route-asset{assets/vdc08.jpeg}}{}
27
+
\figcaption{The climb and the Santuario church.}
28
+
}
29
+
\p{After the meeting had formally concluded, [[okmij]], [[henglein]], [[matija]], [[tsewell]], [[xnning]] and I climbed to Santuario de Santa Luzia. We took the arduous stairs rather than the funicular, as Matija's wife had forbidden him from Portuguese funiculars after the recent [Ascensor da Glória derailment](https://en.wikipedia.org/wiki/Ascensor_da_Glória_derailment), which led to me overdoing it and nearly fainting, but in recompense Matija bought me a beer at the top of the mountain which made it (mostly) worth it! }
30
+
\p{Hopefully I can make it to the next meeting in Estonia next year!}
31
+
\figure{
32
+
\<html:img>[width]{240px}[src]{\route-asset{assets/vdc09.jpeg}}{}
33
+
}
+9
-1
trees/news.tree
+9
-1
trees/news.tree
···
4
4
\p{See also [Weeknotes](loc-001B)}
5
5
\table{
6
6
\tr{
7
+
\th{ 25.09.12 }
8
+
\td{I have been made a member of [[wg21]]. }
9
+
}
10
+
\tr{
11
+
\th{ 25.09.08 }
12
+
\td{The [[icfpc25]] has successfully concluded. }
13
+
}
14
+
\tr{
7
15
\th{ 25.08.22 }
8
-
\td{[[xinloi]] starts her PhD with me [[hoefner]] today. }
16
+
\td{[[xinloi]] starts her PhD with me and [[hoefner]] today. }
9
17
}
10
18
\tr{
11
19
\th{ 25.07.22 }
+4
trees/people/alpern.tree
+4
trees/people/alpern.tree
+10
trees/people/henglein.tree
+10
trees/people/henglein.tree
+10
trees/people/jno.tree
+10
trees/people/jno.tree
+10
trees/people/matija.tree
+10
trees/people/matija.tree
+6
trees/people/nickwu.tree
+6
trees/people/nickwu.tree
+10
trees/people/okmij.tree
+10
trees/people/okmij.tree
+6
trees/people/schneider.tree
+6
trees/people/schneider.tree
+10
trees/people/xnning.tree
+10
trees/people/xnning.tree
+5
trees/places/diku.tree
+5
trees/places/diku.tree
+4
trees/places/imperial.tree
+4
trees/places/imperial.tree
+4
trees/places/ljubljana.tree
+4
trees/places/ljubljana.tree
+4
trees/places/minho.tree
+4
trees/places/minho.tree
+4
trees/places/tohoku.tree
+4
trees/places/tohoku.tree
+4
trees/places/utoronto.tree
+4
trees/places/utoronto.tree
+7
trees/refs/alpern-schneider-1985.tree
+7
trees/refs/alpern-schneider-1985.tree
+9
trees/refs/oconnor-2024-wg21-2.tree
+9
trees/refs/oconnor-2024-wg21-2.tree
···
1
+
\title{I don't have all day: Examining linear-time temporal {Properties, Logic} within finite time}
2
+
\taxon{Reference}
3
+
\meta{venue}{[[wg21]] Meeting, Canberra, Australia}
4
+
\author{liamoc}
5
+
\date{2024-11-29}
6
+
\tag{talk}
7
+
\tag{temporal-logic}
8
+
\tag{semantics}
9
+
\p{We define a proper inductive semantics for LTL which includes those finite partial traces for which a definitive answer can be given: the “definitive prefixes” of the property. Sets of definitive prefixes are called definitive sets. Defining a semantics for LTL in terms of definitive sets gives us something equivalent to LTL3, a formulation popular in runtime verification. Our theory of definitive sets is sufficient to give a neat characterisation of (co-)safety and (co-)liveness properties, allowing us to straightforwardly prove Alpern and Schneider’s result that every property is the intersection of a safety and liveness property by simpler means.}
+9
trees/refs/oconnor-2025-wg21.tree
+9
trees/refs/oconnor-2025-wg21.tree
···
1
+
\title{Runtime monitoring via topology}
2
+
\taxon{Reference}
3
+
\meta{venue}{[[wg21]] Meeting, Viana do Castelo, Portugal}
4
+
\author{liamoc}
5
+
\date{2025-09-10}
6
+
\tag{talk}
7
+
\tag{temporal-logic}
8
+
\tag{semantics}
9
+
\p{The literature on runtime “verification” (the activity of monitoring a running process to ensure compliance with a given specification) offers many different definitions of “monitorability” for properties. In a linear-time temporal setting, properties take the form of sets of behaviours (infinite sequences of states). In this talk, I will arrange the various monitorability classes found in the literature into a hierarchy along with well-known classes of properties such as safety and guarantee properties. I then give each of these monitorability classes neat topological characterisations within the topology induced by the "guarantee kernel" interior operator. Lastly, I show that the metric space used by [Alpern and Schneider](alpern-schneider-1985) coincides with our topology.}
+7
trees/weeknotes/2025-W35.tree
+7
trees/weeknotes/2025-W35.tree
···
1
+
\import{table-macros}
2
+
\title{Weeknotes 2025-W35}
3
+
\author{liamoc}
4
+
\date{2025-08-31}
5
+
\p{This week included my aforementioned [move to Dickson](loc-001O). I'm really liking my new place, even though I haven't unpacked everything yet. Having a reasonably authentic bánh mì shop nearby is a huge relief after trying the mostly poor-quality bánh mì sold at most other Canberra locations (let alone the pathetic excuses for bánh mì sold in Edinburgh). Also the walking routes to both church and the university are, while a bit longer than what I'm used to, very full of natural beauty and mostly quiet and free of traffic noise. }
6
+
\p{Work-wise, this week was mostly [[icfpc25]] preparation, as well as preparing for my upcoming trip to Portugal. }
7
+
\transclude{loc-001T}