my forest
update to latest forester-5.0-dev
+278
-270
+2
-1
forest.toml
+2
-1
forest.toml
+2
-2
trees/dm-0000.tree
+2
-2
trees/dm-0000.tree
···
1
-
\taxon{definition}
1
+
\taxon{Definition}
2
2
\author{liamoc}
3
-
\title{partial order}
3
+
\title{Partial order}
4
4
\p{A binary relation #{(\sqsubseteq) \subseteq X \times X} is a \em{partial order} if it is, for all #{x, y, z \in X}:
5
5
\ul{
6
6
\li{ [reflexive](dm-0001): #{x \sqsubseteq x}, }
+2
-2
trees/dm-0001.tree
+2
-2
trees/dm-0001.tree
+2
-2
trees/dm-0002.tree
+2
-2
trees/dm-0002.tree
···
1
-
\taxon{definition}
1
+
\taxon{Definition}
2
2
\author{liamoc}
3
-
\title{transitivity}
3
+
\title{Transitivity}
4
4
\p{A binary relation #{\mathcal{R} \subseteq X \times X} is \em{transitive} iff, for all #{x, y, z \in X}, if #{x\ \mathcal{R}\ y} and #{y\ \mathcal{R}\ z} then #{x\ \mathcal{R}\ z}.}
+2
-2
trees/dm-0003.tree
+2
-2
trees/dm-0003.tree
+4
-4
trees/dm-0004.tree
+4
-4
trees/dm-0004.tree
···
1
-
\taxon{definition}
1
+
\taxon{Definition}
2
2
\author{liamoc}
3
-
\title{poset}
4
-
\p{A partially ordered set, or \em{poset} for short, is a pair #{(X, \sqsubseteq)} of a set #{X} equipped with a [[dm-0000]] #{(\sqsubseteq) \subseteq X \times X}.}
5
-
\p{ Sometimes, when [[dm-0000]] is arbitrary or clear from context, the set #{X} itself may be referred to as a poset.}
3
+
\title{Poset}
4
+
\p{A partially ordered set, or \em{poset} for short, is a pair #{(X, \sqsubseteq)} of a set #{X} equipped with a [partial order](dm-0000) #{(\sqsubseteq) \subseteq X \times X}.}
5
+
\p{ Sometimes, when the [ordering](dm-0000) is arbitrary or clear from context, the set #{X} itself may be referred to as a poset.}
+2
-2
trees/dm-0005.tree
+2
-2
trees/dm-0005.tree
+2
-2
trees/dm-0006.tree
+2
-2
trees/dm-0006.tree
+2
-2
trees/dt-0000.tree
+2
-2
trees/dt-0000.tree
+2
-2
trees/dt-0001.tree
+2
-2
trees/dt-0001.tree
+1
-1
trees/dt-0002.tree
+1
-1
trees/dt-0002.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
3
\taxon{Remark}
4
-
\p{The choices semantic domain and valuation function is, essentially, arbitrary: we choose objects that reflect those aspects of our programs that we are interested in. For most of the simple languages we will examine, we are only concerned with the \em{results} of the computation, which is a semantics suitable for reasoning about program behaviour and correctness. However, there also exist denotational \em{cost models} that compositionally assign a measure of program performance to syntax. This measure is just another kind of [[dt-0001]].}
4
+
\p{The choices semantic domain and valuation function is, essentially, arbitrary: we choose objects that reflect those aspects of our programs that we are interested in. For most of the simple languages we will examine, we are only concerned with the \em{results} of the computation, which is a semantics suitable for reasoning about program behaviour and correctness. However, there also exist denotational \em{cost models} that compositionally assign a measure of program performance to syntax. This measure is just another kind of [denotational semantics](dt-0001).}
+1
-1
trees/dt-0003.tree
+1
-1
trees/dt-0003.tree
···
1
1
\import{dt-macros}
2
-
\title{denotational semantics}
2
+
\title{Denotational semantics}
3
3
\author{liamoc}
4
4
\p{In this course we are concerned with programming languages, which, as with natural languages, consist of a \em{syntax} and \em{semantics}.
5
5
The syntax of a language is, for our purposes, merely an inductively-defined tree structure (i.e. abstract syntax).}
+2
-2
trees/dt-0004.tree
+2
-2
trees/dt-0004.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{[[dt-0001]] for [[dt-0000]]}
4
-
\taxon{example}
3
+
\title{[Denotational semantics](dt-0001) for [the \cal{C} language (without loops)](dt-0000)}
4
+
\taxon{Example}
5
5
\p{We shall first select a semantic domain for each syntactic class:
6
6
##{
7
7
\begin{array}{lcl}
+1
-1
trees/dt-0006.tree
+1
-1
trees/dt-0006.tree
+4
-4
trees/dt-0007.tree
+4
-4
trees/dt-0007.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{recursively defined semantic domains}
3
+
\title{Recursively defined semantic domains}
4
4
5
5
\p{Suppose we extend our notion of expressions in [the \cal{C} language](dt-0000) with parameterless \em{higher-order} procedures:
6
6
##{
···
11
11
}}
12
12
\subtree{
13
13
\taxon{Example}
14
-
\title{using higher-order procedures}
14
+
\title{Using higher-order procedures}
15
15
\p{We can store procedures in variables, so the program:
16
16
##{\mathit{inc} := (\mathsf{proc}\ a := a + 1); \mathit{inc}; \mathit{inc}}
17
17
has the same effects on the variable #{a} as the program:
18
18
##{a := a + 1; a := a + 1}
19
19
}
20
20
}
21
-
\p{For our [[dt-0001]], our domains now take this form (#{\textcolor{blue}{\text{blue}}} parts are new vs. \ref{dt-0004}), where #{\uplus} denotes \em{disjoint union}:
21
+
\p{For our [denotational semantics](dt-0001), our domains now take this form (#{\textcolor{blue}{\text{blue}}} parts are new vs. \ref{dt-0004}), where #{\uplus} denotes \em{disjoint union}:
22
22
##{
23
23
\begin{array}{lcl}
24
24
\mathbf{E} & \triangleq & \Sigma \rightarrow \mathbb{Z}\textcolor{blue}{\ \uplus\ \mathbf{C}}\\
···
32
32
##{\mathbf{C} \; = \; (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C})) \rightarrow (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C}))}
33
33
Such equations have \em{no} set-theoretic solution, even if we weaken equality to mere \em{set isomorphism} (here notated #{\simeq}).
34
34
}
35
-
\subtree{\taxon{example}\title{A simpler equation with no solution}
35
+
\subtree{\taxon{Example}\title{A simpler equation with no solution}
36
36
\p{Consider the recursive equation #{X = X \rightarrow \mathbb{B}}. Cantor's theorem says that there is no set #{X} such that #{X \simeq \pow{X}} (where #{\pow{X}} is the [[dm-0006]] of #{X}), and seeing as #{\pow{X} \simeq (X \rightarrow \mathbb{B})} it follows that #{X = X \rightarrow \mathbb{B}} has no solution.}
37
37
}
38
38
\p{Any kind of \em{higher-order} construct leads to such recursive domain equations.}
+2
-2
trees/dt-0008.tree
+2
-2
trees/dt-0008.tree
+3
-3
trees/dt-0009.tree
+3
-3
trees/dt-0009.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{flat domains and information ordering}
3
+
\title{Flat domains and information ordering}
4
4
\transclude{dt-000A}
5
5
\transclude{dt-0008}
6
6
\transclude{dt-000B}
···
9
9
\put\transclude/toc{false}
10
10
\put\transclude/numbered{false}
11
11
\subtree{
12
-
\taxon{warning}
13
-
\p{Don't confuse the [[dt-000B]] on numbers, i.e. #{\sqsubseteq} on #{\mathbb{Z}_\bot}, with the \em{numerical} ordering #{\leq} on #{\mathbb{Z}}. We know #{0 \leq 1}, but #{0} and #{1} are not comparable in our flat [[dt-000B]].}
12
+
\taxon{Warning}
13
+
\p{Don't confuse the [information ordering](dt-000B) on numbers, i.e. #{\sqsubseteq} on #{\mathbb{Z}_\bot}, with the \em{numerical} ordering #{\leq} on #{\mathbb{Z}}. We know #{0 \leq 1}, but #{0} and #{1} are not comparable in our flat [information ordering](dt-000B).}
14
14
}
15
15
}
+1
-1
trees/dt-000A.tree
+1
-1
trees/dt-000A.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{the bottom value}
3
+
\title{The bottom value}
4
4
\p{Following [Scott](danascott), we introduce a special \em{bottom} value #{\bot} to our semantic domains.
5
5
##{\bot\ \text{represents}\ \begin{cases}\text{an undefined value;}\\\text{an error value;}\\\text{a \emph{non-terminating} computation.} \end{cases}}}
+4
-4
trees/dt-000B.tree
+4
-4
trees/dt-000B.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{information ordering}
4
-
\taxon{definition}
5
-
\p{An information ordering is a [[dm-0000]] on denotations, written #{a \sqsubseteq b}. This indicates that #{b} is \em{approximated by}, or carries \em{more information} than, or is \em{more well-defined} than #{a}.
6
-
Naturally, [[dt-000A]], being totally uninformative, is always the least element in this ordering.}
3
+
\title{Information ordering}
4
+
\taxon{Definition}
5
+
\p{An information ordering is a [partial order](dm-0000) on denotations, written #{a \sqsubseteq b}. This indicates that #{b} is \em{approximated by}, or carries \em{more information} than, or is \em{more well-defined} than #{a}.
6
+
Naturally, [the bottom value](dt-000A), being totally uninformative, is always the least element in this ordering.}
+3
-3
trees/dt-000C.tree
+3
-3
trees/dt-000C.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{example}
4
-
\title{information ordering for flat domains}
5
-
\p{Consider a [[dt-0008]] #{X_\bot}. There is a natural [[dt-000B]] #{\sqsubseteq} on #{X_\bot}:}
3
+
\taxon{Example}
4
+
\title{Information ordering for flat domains}
5
+
\p{Consider a [flat domain](dt-0008) #{X_\bot}. There is a natural [information ordering](dt-000B) #{\sqsubseteq} on #{X_\bot}:}
6
6
\figure{\tex{\usepackage{tikz}}{\begin{tikzpicture}
7
7
\node (d1) at (-1,0) {$\cdots$};
8
8
\node (d2) at (4,0) {$\cdots$};
+2
-2
trees/dt-000D.tree
+2
-2
trees/dt-000D.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\title{combining domains}
3
+
\title{Combining domains}
4
4
\p{Some of our semantics may depend on the combination of multiple domains, i.e. semantic functions of multiple arguments. As an example, the semantics of an
5
-
\syn{if} statement combines the semantics of the condition and the semantics of each of the two branches. In such scenarios, our domains are no longer flat — we must generalise to [[dt-000G]]s.}
5
+
\syn{if} statement combines the semantics of the condition and the semantics of each of the two branches. In such scenarios, our domains are no longer flat — we must generalise to [pointed poset](dt-000G)s.}
6
6
\transclude{dt-000G}
7
7
\transclude{dt-000E}
8
8
\transclude{dt-000F}
+4
-4
trees/dt-000E.tree
+4
-4
trees/dt-000E.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{construction}
4
-
\title{product of two pointed posets}
5
-
\p{Given two [[dt-000G]]s #{X} and #{Y}, the [product](dm-0005) [[dm-0004]] #{X \times Y} is ordered as follows:
3
+
\taxon{Construction}
4
+
\title{Product of two pointed posets}
5
+
\p{Given two [pointed poset](dt-000G)s #{X} and #{Y}, the [product](dm-0005) [poset](dm-0004) #{X \times Y} is ordered as follows:
6
6
##{ (x,y) \sqsubseteq_{X \times Y} (x',y') \quad \text{iff} \quad x \sqsubseteq_X x' \land y \sqsubseteq_Y y' }
7
7
Intuitively, this says that "the information content of a pair of values is increased by increasing the information of either or both of its component values".}
8
-
\p{This [product](dm-0005) [[dm-0004]] is also pointed, with bottom value #{\bot_{X \times Y}} being #{(\bot_A, \bot_B)}.}
8
+
\p{This [product](dm-0005) [poset](dm-0004) is also pointed, with bottom value #{\bot_{X \times Y}} being #{(\bot_A, \bot_B)}.}
+3
-3
trees/dt-000F.tree
+3
-3
trees/dt-000F.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{example}
4
-
\title{the domain #{\mathbb{B}_\bot \times \mathbb{B}_\bot}}
3
+
\taxon{Example}
4
+
\title{The domain #{\mathbb{B}_\bot \times \mathbb{B}_\bot}}
5
5
\figure{\tex{\usepackage{tikz}}{
6
6
\begin{tikzpicture}
7
7
\node (ff) at (0,1) {$(F,F)$};
···
27
27
(tb.north) -- (tf);
28
28
\end{tikzpicture}
29
29
}}
30
-
\p{As can be seen above, the domain #{\mathbb{B}_\bot \times \mathbb{B}_\bot} is not flat, but it is still a [[dt-000G]].}
30
+
\p{As can be seen above, the domain #{\mathbb{B}_\bot \times \mathbb{B}_\bot} is not flat, but it is still a [pointed poset](dt-000G).}
+3
-3
trees/dt-000G.tree
+3
-3
trees/dt-000G.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{definition}
4
-
\title{pointed poset}
5
-
\p{A \em{pointed [[dm-0004]]} is a [partially ordered set](dm-0004) with a [bottom value](dt-000A).}
3
+
\taxon{Definition}
4
+
\title{Pointed poset}
5
+
\p{A \em{pointed [poset](dm-0004)} is a [partially ordered set](dm-0004) with a [bottom value](dt-000A).}
+2
-2
trees/dt-000H.tree
+2
-2
trees/dt-000H.tree
···
1
1
\import{dt-macros}
2
2
\title{Monotonic Functions}
3
3
\author{liamoc}
4
-
\p{If we model our semantic domains for values with [[dt-000G]]s, then programs are modelled by functions between such [[dm-0004]]s. But, not all functions are suitable:}
4
+
\p{If we model our semantic domains for values with [pointed poset](dt-000G)s, then programs are modelled by functions between such [poset](dm-0004)s. But, not all functions are suitable:}
5
5
\transclude{dt-000I}
6
6
\p{It stands to reason that the amount of information we get out of our functions should grow as we increase the amount of information we put into them.
7
7
Such functions are called \em{monotonic} with respect to our information ordering.}
···
11
11
\put\transclude/toc{false}
12
12
\put\transclude/numbered{false}
13
13
\subtree{
14
-
\taxon{thesis}
14
+
\taxon{Thesis}
15
15
\p{Computable functions are [monotonic](dt-000J) (observe that #{H} is not). }
16
16
}
17
17
}
+2
-2
trees/dt-000I.tree
+2
-2
trees/dt-000I.tree
···
1
1
\import{dt-macros}
2
-
\taxon{example}
2
+
\taxon{Example}
3
3
\author{liamoc}
4
-
\title{the halting query}
4
+
\title{The halting query}
5
5
\p{The function #{H : \mathbb{B}_\bot \rightarrow \mathbb{B}_\bot} seems to let us solve the halting problem, assuming #{\bot} represents non-termination:
6
6
##{
7
7
H(v) \; = \; \begin{cases} F & \text{if}\ v = \bot \\ T & \text{otherwise} \end{cases}
+3
-3
trees/dt-000J.tree
+3
-3
trees/dt-000J.tree
···
1
1
\import{dt-macros}
2
-
\taxon{definition}
2
+
\taxon{Definition}
3
3
\author{liamoc}
4
-
\title{monotonicity}
5
-
\p{A function #{f : X \rightarrow Y} between [[dm-0004]]s #{X} and #{Y} is \em{monotone} (or \em{monotonic}) if, for all #{x, y \in X}:
4
+
\title{Monotonicity}
5
+
\p{A function #{f : X \rightarrow Y} between [poset](dm-0004)s #{X} and #{Y} is \em{monotone} (or \em{monotonic}) if, for all #{x, y \in X}:
6
6
##{ x \sqsubseteq y\; \text{implies}\; f(x) \sqsubseteq f(y) }}
+3
-3
trees/dt-000K.tree
+3
-3
trees/dt-000K.tree
···
1
1
\import{dt-macros}
2
2
\author{liamoc}
3
-
\taxon{definition}
4
-
\title{strictness}
5
-
\p{A function #{f : X \rightarrow Y} on pointed posets #{X} and #{Y} is \em{strict} if it preserves [[dt-000A]], i.e. #{f(\bot_X) = \bot_Y}. }
3
+
\taxon{Definition}
4
+
\title{Strictness}
5
+
\p{A function #{f : X \rightarrow Y} on pointed posets #{X} and #{Y} is \em{strict} if it preserves [the bottom value](dt-000A), i.e. #{f(\bot_X) = \bot_Y}. }
+1
-1
trees/dt-000N.tree
+1
-1
trees/dt-000N.tree
+1
-1
trees/dt-000O.tree
+1
-1
trees/dt-000O.tree
···
1
1
\import{dt-macros}
2
-
\taxon{exercise}
2
+
\taxon{Exercise}
3
3
\author{liamoc}
4
4
\p{Let #{\mathbf{K}_K} denote the chain of values #{x_1, x_2, x_3, \dots, x_K} where #{a \leq b} implies #{x_a \sqsubseteq x_b}. There is one [monotonic](dt-000J) function #{\mathbf{K}_1 \rightarrow \mathbf{K}_1}:}
5
5
\figure{\tex{\usepackage{tikz}}{
+1
-1
trees/dt-000P.tree
+1
-1
trees/dt-000P.tree
+3
-3
trees/dt-000Q.tree
+3
-3
trees/dt-000Q.tree
···
1
1
\import{dt-macros}
2
-
\taxon{exercise}
2
+
\taxon{Exercise}
3
3
\author{liamoc}
4
4
\ol{
5
-
\li{Give an example of a [[dm-0004]] #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} \em{doesn't} have a [[dt-000S]].}
6
-
\li{Give an example of a [[dm-0004]] #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} has \em{multiple} [[dt-000S]]s.}
5
+
\li{Give an example of a [poset](dm-0004) #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} \em{doesn't} have a [fixed point](dt-000S).}
6
+
\li{Give an example of a [poset](dm-0004) #{A} and a [monotonic](dt-000J) function #{f : A \rightarrow A} such that #{f} has \em{multiple} [fixed point](dt-000S)s.}
7
7
}
+1
-1
trees/dt-000R.tree
+1
-1
trees/dt-000R.tree
···
18
18
\end{cases}
19
19
\end{array}
20
20
}
21
-
Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain #{X \in \mathbf{C}} such that #{f(X) = X}. In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a [[dt-000S]] for \em{non-recursive} higher-order functions.
21
+
Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain #{X \in \mathbf{C}} such that #{f(X) = X}. In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a [fixed point](dt-000S) for \em{non-recursive} higher-order functions.
22
22
}
+2
-2
trees/dt-000S.tree
+2
-2
trees/dt-000S.tree
+2
-2
trees/dt-000T.tree
+2
-2
trees/dt-000T.tree
···
4
4
\scope{
5
5
\put\transclude/toc{false}
6
6
\put\transclude/numbered{false}
7
-
\subtree{\taxon{problem}
8
-
\p{Not all [monotonic](dt-000J) functions on [[dm-0004]]s have [[dt-000S]], and some have \em{multiple} [[dt-000S]]s!}
7
+
\subtree{\taxon{Problem}
8
+
\p{Not all [monotonic](dt-000J) functions on [posets](dm-0004) have [fixed points](dt-000S), and some have \em{multiple} [fixed point](dt-000S)s!}
9
9
}}
10
10
\p{So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists. }
11
11
\p{Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.}
+8
-31
trees/loc-0001.tree
+8
-31
trees/loc-0001.tree
···
1
1
\import{refs-datalog}
2
-
\title{works of [[liamoc]]}
3
-
\taxon{bibliography}
2
+
\title{Works of [[liamoc]]}
3
+
\taxon{Bibliography}
4
4
\author{liamoc}
5
5
6
+
\transclude{loc-000F}
7
+
\transclude{loc-000G}
8
+
\transclude{loc-000H}
9
+
\transclude{loc-000I}
10
+
\transclude{loc-000J}
6
11
7
-
\subtree{
8
-
\title{refereed papers}
9
-
\query\datalog{
10
-
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{refereed}}
11
-
}
12
-
}
13
12
14
13
15
14
\subtree{
16
-
\title{invited papers}
17
-
\query\datalog{
18
-
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{invited}}
19
-
}
20
-
}
21
-
22
-
23
-
\subtree{
24
-
\title{notable talks (not associated with papers)}
25
-
\query\datalog{
26
-
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{talk}}
27
-
}
28
-
}
29
-
30
-
\subtree{
31
-
\title{workshop papers}
32
-
\query\datalog{
33
-
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{workshop}}
34
-
}
35
-
}
36
-
37
-
\subtree{
38
-
\title{theses and dissertations}
15
+
\title{Theses and dissertations}
39
16
\query\datalog{
40
17
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{thesis}}
41
18
}
+5
-5
trees/loc-0002.tree
+5
-5
trees/loc-0002.tree
···
1
-
\title{students}
1
+
\title{Students}
2
2
\author{liamoc}
3
3
\subtree{
4
-
\title{doctoral students}
4
+
\title{Doctoral students}
5
5
\ul{
6
6
\li{ [[rayhana]]: 2023–present. Linear Temporal Logic with finite observations. Jointly supervised with [[rvg]] at the [[uoe]]. }
7
7
}
8
8
\scope{
9
9
\put\transclude/toc{false}
10
10
\subtree{
11
-
\title{secondary supervisions}
11
+
\title{Secondary supervisions}
12
12
\ul{
13
13
\li{ [[tudor]]: 2021–present, primary supervisor is [[wadler]] at the [[uoe]]. }
14
14
\li{ [[mathieu]]: 2022–present, primary supervisor is [[tgrosser]] at the [[cam]]. }
···
17
17
}
18
18
19
19
\subtree{
20
-
\title{masters students}
20
+
\title{Masters students}
21
21
\ul{
22
22
\li{ Shaonan Li: 2022, [[uoe]]. \em{Exploring the 8-bit demoscene.}}
23
23
}
24
24
}
25
25
26
26
\subtree{
27
-
\title{bachelors students}
27
+
\title{Bachelors students}
28
28
\ul{
29
29
\li{[[jackb]]: 2025, [[anu]] Semester Project. \em{A File Format for Holbert Proofs.}}
30
30
\li{[[sandwichman]]: 2023-2024, [[uoe]]. \em{Concurrent Games in Agda.}}
+3
-3
trees/loc-0003.tree
+3
-3
trees/loc-0003.tree
···
1
-
\title{academic community roles}
1
+
\title{Academic community roles}
2
2
\author{liamoc}
3
3
4
4
\ul{
···
12
12
}
13
13
14
14
\subtree{
15
-
\title{program committees}
15
+
\title{Program committees}
16
16
\ul{
17
17
\li{[[haskell25]]}
18
18
\li{[[fproper25]]}
···
29
29
}
30
30
31
31
\subtree{
32
-
\title{other reviewing}
32
+
\title{Other reviewing}
33
33
\ul{
34
34
\li{External Review, [[tase23]]}
35
35
\li{External Review, [[esop22]]}
+4
-4
trees/loc-0004.tree
+4
-4
trees/loc-0004.tree
···
1
-
\title{curriculum vitæ}
1
+
\title{Curriculum vitæ}
2
2
\author{liamoc}
3
3
\transclude{loc-0008}
4
4
\transclude{loc-0005}
5
5
\transclude{loc-0006}
6
-
\transclude{loc-0001/0}
7
-
\transclude{loc-0001/1}
8
-
\transclude{loc-0001/2}
6
+
\transclude{loc-000F}
7
+
\transclude{loc-000G}
8
+
\transclude{loc-000H}
9
9
\transclude{loc-0007}
10
10
\transclude{loc-0002}
11
11
\transclude{loc-0003}
+1
-1
trees/loc-0005.tree
+1
-1
trees/loc-0005.tree
+1
-1
trees/loc-0006.tree
+1
-1
trees/loc-0006.tree
+3
-3
trees/loc-0007.tree
+3
-3
trees/loc-0007.tree
···
1
1
\import{table-macros}
2
-
\title{teaching}
2
+
\title{Teaching}
3
3
\author{liamoc}
4
-
\p{The following teaching engagements were/are all at [[anu]]:}
4
+
\p{The following teaching engagements were/are all at the [[anu]]:}
5
5
\table{
6
6
\tr{\td{2025}\td{ [[COMP1100]]. Lecturer.}}
7
7
}
8
-
\p{The following teaching engagements were all at [[uoe]]:}
8
+
\p{The following teaching engagements were all at the [[uoe]]:}
9
9
\table{
10
10
\tr{\td{2024}\td{ [[typesig-dt]] (15 students). Invited Lecturer.}}
11
11
\tr{\td{}\td{ [[mcs]] (30 students). Lecturer Convenor, Tutor.}}
+1
-1
trees/loc-0008.tree
+1
-1
trees/loc-0008.tree
···
1
-
\title{research themes}
1
+
\title{Research themes}
2
2
\author{liamoc}
3
3
\p{I specialise in the intersection of programming languages and formal methods, with a particular emphasis on type systems, test frameworks and other connections between specification and implementation.}
4
4
\p{I enjoy applying theory to practice: developing programming languages and tools based on established theoretical models and techniques.}
+1
-1
trees/loc-0009.tree
+1
-1
trees/loc-0009.tree
···
1
-
\title{contact}
1
+
\title{Contact}
2
2
\author{liamoc}
3
3
\p{I am generally available via email, at \code{me@} this domain. I may also be found on Discord (\code{liamoc}), various Zulips (SPLS, Lean, Agda), the [cogent-club slack](https://cogent-club.slack.com/), [bluesky](https://bsky.app/profile/liamoc.net), [the types.pl mastodon instance](https://types.pl/@liamoc), and inexplicably still [twitter](https://twitter.com/kamatsu8). My office is Room N213 in the Skaidrite Darius Building (CSIT) 108 on the [ANU](anu) Campus. The office door is open to the public so feel free to pop over if you want to visit me. To ensure my availability, it may be wise to first contact me via other means to make an appointment.}
4
4
\p{If you are a student or a colleague, please contact me via my [ANU](anu) email (\code{liam.oconnor} at \code{anu.edu.au}), or on the appropriate course forum (e.g. Ed).}
+1
-1
trees/loc-000A.tree
+1
-1
trees/loc-000A.tree
···
1
1
\import{refs-datalog}
2
-
\title{property-based testing}
2
+
\title{Property-based testing}
3
3
\taxon{Research Theme}
4
4
\author{liamoc}
5
5
\p{I'm interested in bringing more formal methods techniques into the world of testing and traditional software engineering via the avenue of property-based testing.}
+1
-1
trees/loc-000B.tree
+1
-1
trees/loc-000B.tree
···
1
1
\import{refs-datalog}
2
-
\title{temporal logic}
2
+
\title{Temporal logic}
3
3
\taxon{Research Theme}
4
4
\author{liamoc}
5
5
\p{As one of the most common ways to specify reactive systems, temporal logic hasn't gotten as much attention as it deserves. I hope to expand on the theory of temporal logics as well as put them into more practical software engineering tools.}
+1
-1
trees/loc-000C.tree
+1
-1
trees/loc-000C.tree
+6
trees/loc-000F.tree
+6
trees/loc-000F.tree
+6
trees/loc-000G.tree
+6
trees/loc-000G.tree
+6
trees/loc-000H.tree
+6
trees/loc-000H.tree
+6
trees/loc-000I.tree
+6
trees/loc-000I.tree
+6
trees/loc-000J.tree
+6
trees/loc-000J.tree
+11
-11
trees/news.tree
+11
-11
trees/news.tree
···
3
3
\author{liamoc}
4
4
\table{
5
5
\tr{
6
-
\th{ 2025-03-22 }
6
+
\th{ 25.03.22 }
7
7
\td{I have joined the PC for [[haskell25]]. }
8
8
}
9
9
\tr{
10
-
\th{ 2025-03-13 }
10
+
\th{ 25.03.13 }
11
11
\td{I have joined the PC for [[fproper25]]. }
12
12
}
13
13
\tr{
14
-
\th{ 2025-02-04 }
14
+
\th{ 25.02.04 }
15
15
\td{ [[jackb]] has joined me for a semester project working on [Holbert](oconnor-amjad-2022). }
16
16
}
17
17
\tr{
18
-
\th{ 2025-01-08 }
18
+
\th{ 25.01.08 }
19
19
\td{I have joined the PC for [[aplas25]]. }
20
20
}
21
21
\tr{
22
-
\th{ 2024-11-05 }
22
+
\th{ 24.11.05 }
23
23
\td{I have joined the PC for [[icfp25]]. }
24
24
}
25
25
\tr{
26
-
\th{ 2024-10-22 }
26
+
\th{ 24.10.22 }
27
27
\td{I have joined the PC for [[pldi25]]. }
28
28
}
29
29
\tr{
30
-
\th{ 2024-09-17 }
30
+
\th{ 24.09.17 }
31
31
\td{I have agreed to organise the [[icfpc25]]. }
32
32
}
33
33
\tr{
34
-
\th{2024-09-30 }
34
+
\th{24.09.30 }
35
35
\td{I was delighted to spend a week with the [WG2.1](wg21) folks here at the [ANU](anu).}
36
36
}
37
37
\tr{
38
-
\th{ 2024-09-09 }
39
-
\td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek-oconnor-2024]] at [EXPRESS/SOS](expresssos24). }
38
+
\th{ 24.09.09 }
39
+
\td{Our student [[rayhana]] has published her first paper, [[amjad-vanglabbeek.oconnor-24]] at [EXPRESS/SOS](expresssos24). }
40
40
}
41
41
\tr{
42
-
\th{ 2024-07-30 }
42
+
\th{ 24.07.30 }
43
43
\td{I have taken a new position as a Senior Lecturer at the [[anu]]. }
44
44
}
45
45
+1
-1
trees/people/amblafont.tree
+1
-1
trees/people/amblafont.tree
+1
-1
trees/people/aria.tree
+1
-1
trees/people/aria.tree
+1
-1
trees/people/ccm.tree
+1
-1
trees/people/ccm.tree
+1
-1
trees/people/chak.tree
+1
-1
trees/people/chak.tree
+1
-1
trees/people/craigmcl.tree
+1
-1
trees/people/craigmcl.tree
+1
-1
trees/people/crizkallah.tree
+1
-1
trees/people/crizkallah.tree
+1
-1
trees/people/danascott.tree
+1
-1
trees/people/danascott.tree
+1
-1
trees/people/gckeller.tree
+1
-1
trees/people/gckeller.tree
+1
-1
trees/people/gklein.tree
+1
-1
trees/people/gklein.tree
+1
-1
trees/people/heiser.tree
+1
-1
trees/people/heiser.tree
+1
-1
trees/people/hoefner.tree
+1
-1
trees/people/hoefner.tree
+1
-1
trees/people/jackb.tree
+1
-1
trees/people/jackb.tree
+1
-1
trees/people/jcb.tree
+1
-1
trees/people/jcb.tree
+1
-1
trees/people/kaie.tree
+1
-1
trees/people/kaie.tree
+1
-1
trees/people/keshen.tree
+1
-1
trees/people/keshen.tree
+1
-1
trees/people/lcheung.tree
+1
-1
trees/people/lcheung.tree
+3
-3
trees/people/liamoc.tree
+3
-3
trees/people/liamoc.tree
···
1
1
\import{table-macros}
2
2
\title{Liam O'Connor}
3
-
\taxon{person}
3
+
\taxon{Person}
4
4
\meta{external}{https://liamoc.net}
5
5
\meta{institution}{[[anu]]}
6
6
\meta{orcid}{0000-0003-2765-4269}
7
7
\meta{position}{Senior Lecturer}
8
8
\<html:img>[class]{portrait}[src]{\route-asset{assets/me.jpeg}}
9
9
\p{I am a Senior Lecturer in Foundations at the [[anu]] School of Computing, on [[loc-000D]]. I'm also an Honorary Fellow at the [[uoe]] Laboratory for Foundations of Computer Science, where I worked until 2024.}
10
-
\p{Lately, my research has been focused on [[loc-000A]], [[loc-000C]] and [[loc-000B]], but I have very broad research interests. See my [personal bibliography](loc-0001) for a full list of my work.}
10
+
\p{Lately, my research has been focused on [property-based testing](loc-000A), [semantics](loc-000C) and [temporal logic](loc-000B), but I have very broad research interests. See my [personal bibliography](loc-0001) for a full list of my work.}
11
11
\p{Previously, I lectured courses at [[unsw]], where I did my PhD with [[gckeller]] and the Trustworthy Systems Team lead by [[heiser]], focusing on the [[cogent]] project.}
12
12
13
-
\p{More details about me can be found on my [[loc-0004]].}
13
+
\p{More details about me can be found on my [curriculum vitæ](loc-0004).}
+1
-1
trees/people/mathieu.tree
+1
-1
trees/people/mathieu.tree
+1
-1
trees/people/msteuwer.tree
+1
-1
trees/people/msteuwer.tree
+1
-1
trees/people/ohad.tree
+1
-1
trees/people/ohad.tree
+1
-1
trees/people/owickstrom.tree
+1
-1
trees/people/owickstrom.tree
+1
-1
trees/people/rayhana.tree
+1
-1
trees/people/rayhana.tree
+1
-1
trees/people/rvg.tree
+1
-1
trees/people/rvg.tree
+1
-1
trees/people/sandwichman.tree
+1
-1
trees/people/sandwichman.tree
+1
-1
trees/people/tgrosser.tree
+1
-1
trees/people/tgrosser.tree
+1
-1
trees/people/tobym.tree
+1
-1
trees/people/tobym.tree
+1
-1
trees/people/tsewell.tree
+1
-1
trees/people/tsewell.tree
+1
-1
trees/people/tudor.tree
+1
-1
trees/people/tudor.tree
+1
-1
trees/people/vjackson.tree
+1
-1
trees/people/vjackson.tree
+1
-1
trees/people/wadler.tree
+1
-1
trees/people/wadler.tree
+1
-1
trees/people/yutakang.tree
+1
-1
trees/people/yutakang.tree
+1
-1
trees/people/zilinc.tree
+1
-1
trees/people/zilinc.tree
+1
-1
trees/places/anu.tree
+1
-1
trees/places/anu.tree
+1
-1
trees/places/asplos16.tree
+1
-1
trees/places/asplos16.tree
+1
-1
trees/places/asplos19.tree
+1
-1
trees/places/asplos19.tree
+1
-1
trees/places/cam.tree
+1
-1
trees/places/cam.tree
+1
-1
trees/places/cmu.tree
+1
-1
trees/places/cmu.tree
+1
-1
trees/places/core.tree
+1
-1
trees/places/core.tree
+1
-1
trees/places/cpp18.tree
+1
-1
trees/places/cpp18.tree
+1
-1
trees/places/cpp22.tree
+1
-1
trees/places/cpp22.tree
+1
-1
trees/places/csf19.tree
+1
-1
trees/places/csf19.tree
+1
-1
trees/places/csiro.tree
+1
-1
trees/places/csiro.tree
+1
-1
trees/places/data61.tree
+1
-1
trees/places/data61.tree
+1
-1
trees/places/esop22.tree
+1
-1
trees/places/esop22.tree
+1
-1
trees/places/expresssos24.tree
+1
-1
trees/places/expresssos24.tree
+1
-1
trees/places/fossacs21.tree
+1
-1
trees/places/fossacs21.tree
+1
-1
trees/places/fproper25.tree
+1
-1
trees/places/fproper25.tree
+1
-1
trees/places/google-syd.tree
+1
-1
trees/places/google-syd.tree
+1
-1
trees/places/haskell25.tree
+1
-1
trees/places/haskell25.tree
+1
-1
trees/places/hatra22.tree
+1
-1
trees/places/hatra22.tree
+1
-1
trees/places/icfp14.tree
+1
-1
trees/places/icfp14.tree
+1
-1
trees/places/icfp15.tree
+1
-1
trees/places/icfp15.tree
+1
-1
trees/places/icfp16.tree
+1
-1
trees/places/icfp16.tree
+1
-1
trees/places/icfp18.tree
+1
-1
trees/places/icfp18.tree
+1
-1
trees/places/icfp21.tree
+1
-1
trees/places/icfp21.tree
+1
-1
trees/places/icfp25.tree
+1
-1
trees/places/icfp25.tree
+1
-1
trees/places/icfpc25.tree
+1
-1
trees/places/icfpc25.tree
+1
-1
trees/places/icfpsrc21.tree
+1
-1
trees/places/icfpsrc21.tree
+1
-1
trees/places/iohk.tree
+1
-1
trees/places/iohk.tree
+1
-1
trees/places/isola18.tree
+1
-1
trees/places/isola18.tree
+1
-1
trees/places/itp16.tree
+1
-1
trees/places/itp16.tree
+1
-1
trees/places/itp17.tree
+1
-1
trees/places/itp17.tree
+1
-1
trees/places/jfp.tree
+1
-1
trees/places/jfp.tree
···
1
1
\title{Journal of Functional Programming}
2
-
\taxon{journal}
2
+
\taxon{Journal}
3
3
\meta{external}{https://www.cambridge.org/core/journals/journal-of-functional-programming}
4
4
5
5
\p{Journal of Functional Programming is an Open Access journal and is the only journal devoted solely to the design, implementation, and application of functional programming languages, spanning the range from mathematical theory to industrial practice. Topics covered include functional languages and extensions, implementation techniques, reasoning and proof, program transformation and synthesis, type systems, type theory, language-based security, memory management, parallelism and applications. Special tracks are devoted to tools and applications, commercial uses and education; pearl-type papers are encouraged.}
+1
-1
trees/places/ml16.tree
+1
-1
trees/places/ml16.tree
+1
-1
trees/places/nicta.tree
+1
-1
trees/places/nicta.tree
+1
-1
trees/places/nott.tree
+1
-1
trees/places/nott.tree
+1
-1
trees/places/ntu.tree
+1
-1
trees/places/ntu.tree
+1
-1
trees/places/ox.tree
+1
-1
trees/places/ox.tree
+1
-1
trees/places/pepm24.tree
+1
-1
trees/places/pepm24.tree
+1
-1
trees/places/philtransA.tree
+1
-1
trees/places/philtransA.tree
···
1
1
\title{Philosophical Transactions of the Royal Society A}
2
-
\taxon{journal}
2
+
\taxon{Journal}
3
3
\meta{external}{https://royalsocietypublishing.org/journal/rsta}
4
4
5
5
\p{Philosophical Transactions is a (very!) long-standing, refereed, open access journal published by the Royal Society. It contains influential themed journal issues across the physical, mathematical and engineering sciences. }
+1
-1
trees/places/pldi22.tree
+1
-1
trees/places/pldi22.tree
+1
-1
trees/places/pldi25.tree
+1
-1
trees/places/pldi25.tree
+1
-1
trees/places/plos13.tree
+1
-1
trees/places/plos13.tree
+1
-1
trees/places/plos17.tree
+1
-1
trees/places/plos17.tree
+1
-1
trees/places/polytechnique.tree
+1
-1
trees/places/polytechnique.tree
+1
-1
trees/places/popl15.tree
+1
-1
trees/places/popl15.tree
+1
-1
trees/places/popl16.tree
+1
-1
trees/places/popl16.tree
+1
-1
trees/places/popl22.tree
+1
-1
trees/places/popl22.tree
+1
-1
trees/places/popl23.tree
+1
-1
trees/places/popl23.tree
+1
-1
trees/places/popl24.tree
+1
-1
trees/places/popl24.tree
+1
-1
trees/places/programming-journal.tree
+1
-1
trees/places/programming-journal.tree
···
1
1
\title{The Art, Science, and Engineering of Programming}
2
-
\taxon{journal}
2
+
\taxon{Journal}
3
3
\meta{external}{https://programming-journal.org}
4
4
5
5
\p{The Art, Science, and Engineering of Programming was created with the goal of placing the wonderful art of programming in the map of scholarly works. Many academic journals and conferences exist that publish research related to programming, starting with programming languages, software engineering, and expanding to the whole Computer Science field. Yet, many of us feel that, as the field of Computer Science expanded, programming, in itself, has been neglected to a secondary role not worthy of scholarly attention. That is a serious gap, as much of the progress in Computer Science lies on the basis of computer programs, the people who write them, and the concepts and tools available to them to express computational tasks.}
+1
-1
trees/places/qmul.tree
+1
-1
trees/places/qmul.tree
+1
-1
trees/places/sblp22.tree
+1
-1
trees/places/sblp22.tree
+1
-1
trees/places/sblp24.tree
+1
-1
trees/places/sblp24.tree
+1
-1
trees/places/sinica.tree
+1
-1
trees/places/sinica.tree
+1
-1
trees/places/sle22.tree
+1
-1
trees/places/sle22.tree
+1
-1
trees/places/spli.tree
+1
-1
trees/places/spli.tree
+1
-1
trees/places/tase23.tree
+1
-1
trees/places/tase23.tree
+1
-1
trees/places/toposinstitute.tree
+1
-1
trees/places/toposinstitute.tree
+1
-1
trees/places/tu-berlin.tree
+1
-1
trees/places/tu-berlin.tree
+1
-1
trees/places/tweag.tree
+1
-1
trees/places/tweag.tree
+1
-1
trees/places/tyde16.tree
+1
-1
trees/places/tyde16.tree
+1
-1
trees/places/tyde17.tree
+1
-1
trees/places/tyde17.tree
+1
-1
trees/places/tyde19.tree
+1
-1
trees/places/tyde19.tree
+1
-1
trees/places/typesig.tree
+1
-1
trees/places/typesig.tree
+1
-1
trees/places/uiuc.tree
+1
-1
trees/places/uiuc.tree
+1
-1
trees/places/unimelb.tree
+1
-1
trees/places/unimelb.tree
+1
-1
trees/places/unsw.tree
+1
-1
trees/places/unsw.tree
+1
-1
trees/places/uoe.tree
+1
-1
trees/places/uoe.tree
+1
-1
trees/places/uu.tree
+1
-1
trees/places/uu.tree
+1
-1
trees/places/wg21.tree
+1
-1
trees/places/wg21.tree
···
1
1
\title{IFIP Working Group 2.1: Algorithmic Languages and Calculi}
2
-
\taxon{institution}
2
+
\taxon{Institution}
3
3
\meta{external}{https://ifipwg21wiki.cs.kuleuven.be/}
4
4
\p{
5
5
IFIP Working Group 2.1 on Algorithmic Languages and Calculi is a working group of the International Federation for Information Processing (IFIP). Its scope includes:
+1
-1
trees/refs/amani-hcrcobnlstkmkh-2016.tree
+1
-1
trees/refs/amani-hcrcobnlstkmkh-2016.tree
+1
-1
trees/refs/amjad-vanglabbeek-oconnor-2024.tree
+1
-1
trees/refs/amjad-vanglabbeek-oconnor-2024.tree
+1
-1
trees/refs/chen-lokmjr-2023.tree
+1
-1
trees/refs/chen-lokmjr-2023.tree
+1
-1
trees/refs/chen-okkh-2017.tree
+1
-1
trees/refs/chen-okkh-2017.tree
+1
-1
trees/refs/chen-roskhk-2022.tree
+1
-1
trees/refs/chen-roskhk-2022.tree
+1
-1
trees/refs/cheung-oconnor-rizkallah-2022.tree
+1
-1
trees/refs/cheung-oconnor-rizkallah-2022.tree
+1
-1
trees/refs/keller-maocrkh-2013.tree
+1
-1
trees/refs/keller-maocrkh-2013.tree
+1
-1
trees/refs/klein-akmmo-2017.tree
+1
-1
trees/refs/klein-akmmo-2017.tree
+1
-1
trees/refs/nagashima-oconnor-2016.tree
+1
-1
trees/refs/nagashima-oconnor-2016.tree
+1
-1
trees/refs/oconnor-2022-plmw.tree
+1
-1
trees/refs/oconnor-2022-plmw.tree
+1
-1
trees/refs/oconnor-2024-compsoc.tree
+1
-1
trees/refs/oconnor-2024-compsoc.tree
+1
-1
trees/refs/oconnor-2024-wg21.tree
+1
-1
trees/refs/oconnor-2024-wg21.tree
+1
-1
trees/refs/oconnor-amjad-2022.tree
+1
-1
trees/refs/oconnor-amjad-2022.tree
+1
-1
trees/refs/oconnor-cralmnsk-2016.tree
+1
-1
trees/refs/oconnor-cralmnsk-2016.tree
+1
-1
trees/refs/oconnor-crjakmsk-2021.tree
+1
-1
trees/refs/oconnor-crjakmsk-2021.tree
+1
-1
trees/refs/oconnor-csrkk-2018.tree
+1
-1
trees/refs/oconnor-csrkk-2018.tree
+1
-1
trees/refs/oconnor-kamkcr-2014.tree
+1
-1
trees/refs/oconnor-kamkcr-2014.tree
+1
-1
trees/refs/oconnor-thesis-2019.tree
+1
-1
trees/refs/oconnor-thesis-2019.tree
+1
-1
trees/refs/oconnor-tyde-2016.tree
+1
-1
trees/refs/oconnor-tyde-2016.tree
+1
-1
trees/refs/oconnor-tyde-2019.tree
+1
-1
trees/refs/oconnor-tyde-2019.tree
+1
-1
trees/refs/oconnor-ug-thesis-2012.tree
+1
-1
trees/refs/oconnor-ug-thesis-2012.tree
+1
-1
trees/refs/oconnor-ugproject-2012.tree
+1
-1
trees/refs/oconnor-ugproject-2012.tree
+1
-1
trees/refs/oconnor-vanglabbeek-2023-compsoc.tree
+1
-1
trees/refs/oconnor-vanglabbeek-2023-compsoc.tree
+1
-1
trees/refs/oconnor-wickstrom-2022.tree
+1
-1
trees/refs/oconnor-wickstrom-2022.tree
+1
-1
trees/refs/qin-oconnor-steuwer-2023.tree
+1
-1
trees/refs/qin-oconnor-steuwer-2023.tree
+1
-1
trees/refs/qin-ovghks-2024.tree
+1
-1
trees/refs/qin-ovghks-2024.tree