my forest
major start
+2024
-18
assets/applications.pdf
assets/applications.pdf
This is a binary file and will not be displayed.
assets/deferring.pdf
assets/deferring.pdf
This is a binary file and will not be displayed.
assets/gentzen.pdf
assets/gentzen.pdf
This is a binary file and will not be displayed.
assets/me.jpeg
assets/me.jpeg
This is a binary file and will not be displayed.
assets/reportb.pdf
assets/reportb.pdf
This is a binary file and will not be displayed.
+7
-3
forest.toml
+7
-3
forest.toml
···
1
1
[forest]
2
-
trees = ["trees" ] # The directories in which your trees are stored
3
-
assets = ["assets"] # The directories in which your assets are stored
4
-
theme = "theme" # The directory in which your theme is stored
2
+
host = "liamoc"
3
+
trees = ["trees"] # The directories in which your trees are stored
4
+
assets = ["assets"] # The directories in which your assets are stored
5
+
theme = "theme" # The directory in which your theme is stored
6
+
7
+
[renderer]
8
+
home = "index"
+12
trees/cogent.tree
+12
trees/cogent.tree
···
1
+
\import{refs-datalog}
2
+
\title{Cogent}
3
+
\author{liamoc}
4
+
\taxon{Research Theme}
5
+
\meta{external}{https://trustworthy.systems/projects/OLD/cogent}
6
+
\p{Originally part of my [doctorate](loc-0005/0) and, for a time, as ongoing research work, I designed the Cogent programming language, and I was for many years a contributor to its associated verification framework and compiler.}
7
+
\p{This project was part of the long-term vision of the Trustworthy Systems team lead by [[heiser]] (formerly at [[nicta]], now at [[unsw]]), to reduce the cost and effort required to make formally verified systems.}
8
+
\p{In the past I have also worked with the Trustworthy Systems team on the l4.verified project and tools for the Isabelle theorem prover.}
9
+
10
+
\query\datalog{
11
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{cogent}}
12
+
}
+5
trees/courses/COMP1100.tree
+5
trees/courses/COMP1100.tree
+5
trees/courses/COMP1911.tree
+5
trees/courses/COMP1911.tree
+5
trees/courses/COMP1927.tree
+5
trees/courses/COMP1927.tree
+8
trees/courses/COMP2111.tree
+8
trees/courses/COMP2111.tree
+5
trees/courses/COMP2911.tree
+5
trees/courses/COMP2911.tree
+8
trees/courses/COMP3141.tree
+8
trees/courses/COMP3141.tree
···
1
+
\taxon{Course}
2
+
\title{Software System Design and Implementation}
3
+
\author{liamoc}
4
+
\author{gckeller}
5
+
\author{chak}
6
+
\meta{venue}{[[unsw]]}
7
+
\meta{external}{https://www.cse.unsw.edu.au/~cs3141}
8
+
\p{functional programming, denotational design and property based testing.}
+7
trees/courses/COMP3151.tree
+7
trees/courses/COMP3151.tree
+7
trees/courses/COMP3153.tree
+7
trees/courses/COMP3153.tree
+7
trees/courses/COMP3161.tree
+7
trees/courses/COMP3161.tree
+6
trees/courses/COMP6752.tree
+6
trees/courses/COMP6752.tree
+7
trees/courses/SENG2011.tree
+7
trees/courses/SENG2011.tree
+5
trees/courses/dmp.tree
+5
trees/courses/dmp.tree
+5
trees/courses/inf1a.tree
+5
trees/courses/inf1a.tree
+7
trees/courses/itcs.tree
+7
trees/courses/itcs.tree
+7
trees/courses/mcs.tree
+7
trees/courses/mcs.tree
+7
trees/courses/typesig-dt.tree
+7
trees/courses/typesig-dt.tree
···
1
+
\taxon{Course}
2
+
\title{Domain Theory ([[typesig]])}
3
+
\meta{venue}{[[uoe]]}
4
+
\author{liamoc}
5
+
\meta{external}{https://typesig.pl/resources/domain-theory}
6
+
\p{I ran this course as an opt-in invited lecture series with [[typesig]] at [[uoe]]. Suprisingly, around 15 students consistently showed up throughout.}
7
+
\p{Topics include denotational semantics, fixed points, categories and constructions, PCF, scott domains, recursive domains, and powerdomains.}
+10
trees/dm-0000.tree
+10
trees/dm-0000.tree
···
1
+
\taxon{definition}
2
+
\author{liamoc}
3
+
\title{partial order}
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
+
\ul{
6
+
\li{ [reflexive](dm-0001): #{x \sqsubseteq x}, }
7
+
\li{ [transitive](dm-0002): #{x \sqsubseteq y} and #{y \sqsubseteq z} implies #{x \sqsubseteq z},}
8
+
\li{ [antisymmetric](dm-0003): #{x \sqsubseteq y} and #{y \sqsubseteq x} implies #{x = y}. }
9
+
}
10
+
}
+4
trees/dm-0001.tree
+4
trees/dm-0001.tree
+4
trees/dm-0002.tree
+4
trees/dm-0002.tree
+4
trees/dm-0003.tree
+4
trees/dm-0003.tree
+5
trees/dm-0004.tree
+5
trees/dm-0004.tree
···
1
+
\taxon{definition}
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.}
+4
trees/dm-0005.tree
+4
trees/dm-0005.tree
+5
trees/dm-0006.tree
+5
trees/dm-0006.tree
+15
trees/dt-0000.tree
+15
trees/dt-0000.tree
···
1
+
\import{dt-macros}
2
+
\title{the \cal{C} Language (without loops)}
3
+
\taxon{definition}
4
+
\author{liamoc}
5
+
\p{ Using notation similar to \em{Backus-Naur Form} (BNF):
6
+
##{
7
+
\begin{array}{lcl}
8
+
\cal{E} & \Coloneqq & n \mid x \mid \cal{E}_1 + \cal{E}_2 \mid \cal{E}_1 - \cal{E}_2\\
9
+
\cal{B} & \Coloneqq & \syn{false} \mid \syn{true} \mid \neg \cal{B} \mid \cal{E}_1 = \cal{E}_2\\
10
+
\cal{C} & \Coloneqq & \syn{skip} \mid x := \cal{E} \mid \cal{C}_1 ; \cal{C}_2 \mid \syn{if}\ \cal{B}\ \syn{then}\ \cal{C}_1\ \syn{else}\ \cal{C}_2\\
11
+
x & \in & \cal{V}\; \textit{(variables)}\\
12
+
n & \in & \nat
13
+
\end{array}
14
+
}
15
+
}
+10
trees/dt-0001.tree
+10
trees/dt-0001.tree
···
1
+
\import{dt-macros}
2
+
\taxon{definition}
3
+
\title{denotational semantics}
4
+
\author{liamoc}
5
+
\p{A \em{denotational semantics} consists of, for each syntactic class \cal{X} in a language:
6
+
\ol{
7
+
\li{A \em{semantic domain} #{D} which can be any set of mathematical objects (although, as we will see later, it is helpful if it obeys certain properties).}
8
+
\li{A \em{valuation function} #{\sems{\cdot} : \cal{X} \rightarrow D}. We require that this function be a \em{homomorphism}, that is that it is \em{compositional}. This means that the valuation (or \em{denotation}) of an expression should be made from the denotation of its components. In other words, for each syntactic constructor #{C(e_1,e_2,\dots)}, we should have a mathematical operation #{f(x_1,x_2,\dots)} such that the denotation of #{C} can be defined as: ##{\sems{C(e_1, e_2, \dots)} = f(\sems{e_1}, \sems{e_2}, \dots)}}
9
+
}
10
+
}
+4
trees/dt-0002.tree
+4
trees/dt-0002.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
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]].}
+10
trees/dt-0003.tree
+10
trees/dt-0003.tree
···
1
+
\import{dt-macros}
2
+
\title{denotational semantics}
3
+
\author{liamoc}
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
+
The syntax of a language is, for our purposes, merely an inductively-defined tree structure (i.e. abstract syntax).}
6
+
\transclude{dt-0000}
7
+
\p{In the language above, there are three \em{syntactic classes}: \cal{E}, \cal{B}, and \cal{C}.}
8
+
\transclude{dt-0001}
9
+
\transclude{dt-0002}
10
+
\transclude{dt-0004}
+53
trees/dt-0004.tree
+53
trees/dt-0004.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{[[dt-0001]] for [[dt-0000]]}
4
+
\taxon{example}
5
+
\p{We shall first select a semantic domain for each syntactic class:
6
+
##{
7
+
\begin{array}{lcl}
8
+
\mathbf{E} & \triangleq & \Sigma \rightarrow \mathbb{Z} \\
9
+
\mathbf{B} & \triangleq & \Sigma \rightarrow \mathbb{B} \\
10
+
\mathbf{C} & \triangleq & \Sigma \rightarrow \Sigma \\
11
+
\end{array}
12
+
}
13
+
Here, #{\Sigma} represents the set of \em{states}, which contains the values assigned to all variables:
14
+
##{\Sigma \;\triangleq\; \mathcal{V} \rightarrow \mathbb{Z}}
15
+
}
16
+
\p{Now, we define our \em{valuation functions},
17
+
#{
18
+
\llbracket\cdot\rrbracket_\mathcal{E} : \mathcal{E} \rightarrow \mathbf{E}
19
+
}:
20
+
##{
21
+
\begin{array}{lcl}
22
+
\llbracket n \rrbracket_\mathcal{E}\ \sigma & = & n \\
23
+
\llbracket x \rrbracket_\mathcal{E}\ \sigma & = & \sigma(x) \\
24
+
\llbracket e_1 + e_2 \rrbracket_\mathcal{E}\ \sigma & = & \llbracket e_1 \rrbracket_\mathcal{E}\ \sigma + \llbracket e_2 \rrbracket_\mathcal{E}\ \sigma\\
25
+
\llbracket e_1 - e_2 \rrbracket_\mathcal{E}\ \sigma & = & \llbracket e_1 \rrbracket_\mathcal{E}\ \sigma - \llbracket e_2 \rrbracket_\mathcal{E}\ \sigma\\[2em]
26
+
\end{array}
27
+
}
28
+
and #{\llbracket\cdot\rrbracket_\mathcal{B} : \mathcal{B} \rightarrow \mathbf{B}}:
29
+
##{
30
+
\begin{array}{lcl}
31
+
\llbracket \mathsf{false} \rrbracket_\mathcal{B}\ \sigma & = & F \\
32
+
\llbracket \mathsf{true} \rrbracket_\mathcal{B}\ \sigma & = & T \\
33
+
\llbracket \neg b \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}F & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
34
+
T & \text{otherwise}
35
+
\end{cases}
36
+
\\[1.1em]
37
+
\llbracket e_1 = e_2 \rrbracket_\mathcal{B}\ \sigma & = & \begin{cases}T & \text{if}\ \llbracket e_1 \rrbracket_\mathcal{E}\ \sigma = \llbracket e_2 \rrbracket_\mathcal{E}\ \sigma \\
38
+
F & \text{otherwise}
39
+
\end{cases}
40
+
\end{array}
41
+
}
42
+
and #{\llbracket\cdot\rrbracket_\mathcal{C} : \mathcal{C} \rightarrow \mathbf{C}}:
43
+
##{
44
+
\begin{array}{lcl}
45
+
\llbracket \mathsf{skip} \rrbracket_\mathcal{C}\ \sigma & = & \sigma \\
46
+
\llbracket x := e \rrbracket_\mathcal{C}\ \sigma & = & \sigma\left(x \mapsto \llbracket e \rrbracket_\mathcal{E}\right) \\
47
+
\llbracket c_1 ; c_2 \rrbracket_\mathcal{C}\ \sigma & = & \llbracket c_2 \rrbracket_\mathcal{C}\ \left(\llbracket c_1 \rrbracket_\mathcal{C}\ \sigma\right) \\[0.3em]
48
+
\llbracket \textsf{if}\ b\ \textsf{then}\ c_1\ \textsf{else}\ c_2 \rrbracket_\mathcal{C}\ \sigma & = & \begin{cases}\llbracket c_1 \rrbracket_\mathcal{C}\ \sigma & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
49
+
\llbracket c_2 \rrbracket_\mathcal{C}\ \sigma & \text{otherwise}
50
+
\end{cases}
51
+
\end{array}
52
+
}
53
+
}
+11
trees/dt-0005.tree
+11
trees/dt-0005.tree
···
1
+
\import{dt-macros}
2
+
\title{First Steps into Domains}
3
+
\taxon{Lecture}
4
+
\author{liamoc}
5
+
\p{This lecture is based on material from [[haskellhutt]], [[danascott]], [[jstoy]], [[cgunter]], and [[gwinskel]].}
6
+
\transclude{dt-0003}
7
+
\transclude{dt-000L}
8
+
\transclude{dt-0009}
9
+
\transclude{dt-000D}
10
+
\transclude{dt-000H}
11
+
\transclude{dt-000U}
+33
trees/dt-0006.tree
+33
trees/dt-0006.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{recursively defined programs}
4
+
\p{
5
+
Suppose we extended [the \cal{C} language](dt-0000) with a while loop construct:
6
+
##{
7
+
\mathcal{C}\; \Coloneqq\; \cdots \mid \mathsf{while}\ \mathcal{B}\ \mathsf{do}\ \mathcal{C}\ \mathsf{od}
8
+
}
9
+
The intuitive way to assign a semantics would be to use a \em{recursive function}:
10
+
##{
11
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
12
+
\sigma & \text{otherwise}
13
+
\end{cases}
14
+
}
15
+
However, such an equation is not a good definition. If we consider the trivial infinite loop program #{L \triangleq \mathsf{while}\ \mathsf{true}\ \mathsf{do}\ \mathsf{skip}\ \mathsf{od}}, and compute its semantics, we end up with:
16
+
##{
17
+
\llbracket \mathsf{while}\ \mathsf{true}\ \mathsf{do}\ \mathsf{skip}\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma \; = \; \llbracket \mathsf{while}\ \mathsf{true}\ \mathsf{do}\ \mathsf{skip}\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma
18
+
}
19
+
This equation is satisfied by \em{any} function #{\Sigma \rightarrow \Sigma},
20
+
so it doesn't tell us which function corresponds to the program #{L}.}
21
+
\p{More generally, allowing our functions to be (generally) recursive causes these issues. The loop program #{L} gives rise to the recursive equation #{\ell(x) = \ell(x)}, which has an infinite number of solutions. }
22
+
23
+
\p{If we add recursion to our programming language, we could have programs that give rise to more complex recursive equations like #{f(x) = f(x) + 1}. By contrast to #{\ell(x)}, #{f(x)} \em{has no solutions} (assuming #{f(x)} operates on integers). }
24
+
\scope{
25
+
\put\transclude/toc{false}
26
+
\put\transclude/numbered{false}
27
+
\subtree{
28
+
\taxon{Upshot}
29
+
\p{
30
+
We need an \em{explicit} notion of "non-termination" on the semantics level, to properly deal with general recursion (or iteration).
31
+
}
32
+
}
33
+
}
+48
trees/dt-0007.tree
+48
trees/dt-0007.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{recursively defined semantic domains}
4
+
5
+
\p{Suppose we extend our notion of expressions in [the \cal{C} language](dt-0000) with parameterless \em{higher-order} procedures:
6
+
##{
7
+
\begin{array}{l}
8
+
\mathcal{E}\; \Coloneqq \; \cdots \mid \mathsf{proc}\ \mathcal{C}\\
9
+
\mathcal{C}\; \Coloneqq \; \cdots \mid x
10
+
\end{array}
11
+
}}
12
+
\subtree{
13
+
\taxon{Example}
14
+
\title{using higher-order procedures}
15
+
\p{We can store procedures in variables, so the program:
16
+
##{\mathit{inc} := (\mathsf{proc}\ a := a + 1); \mathit{inc}; \mathit{inc}}
17
+
has the same effects on the variable #{a} as the program:
18
+
##{a := a + 1; a := a + 1}
19
+
}
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}:
22
+
##{
23
+
\begin{array}{lcl}
24
+
\mathbf{E} & \triangleq & \Sigma \rightarrow \mathbb{Z}\textcolor{blue}{\ \uplus\ \mathbf{C}}\\
25
+
\mathbf{B} & \triangleq & \Sigma \rightarrow \mathbb{B} \\
26
+
\mathbf{C} & \triangleq & \Sigma \rightarrow \Sigma \\[0.2em]
27
+
\Sigma & \triangleq & \mathcal{V} \rightarrow \mathbb{Z}\textcolor{blue}{\ \uplus\ \mathbf{C}}
28
+
\end{array}
29
+
}
30
+
\transclude{dt-000P}
31
+
Unfolding the definition of #{\Sigma}, we end up with a recursive equation for the definition of #{\mathbf{C}}:
32
+
##{\mathbf{C} \; = \; (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C})) \rightarrow (\mathcal{V} \rightarrow (\mathbb{Z} \uplus \mathbf{C}))}
33
+
Such equations have \em{no} set-theoretic solution, even if we weaken equality to mere \em{set isomorphism} (here notated #{\simeq}).
34
+
}
35
+
\subtree{\taxon{example}\title{A simpler equation with no solution}
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
+
}
38
+
\p{Any kind of \em{higher-order} construct leads to such recursive domain equations.}
39
+
\scope{
40
+
\put\transclude/toc{false}
41
+
\put\transclude/numbered{false}
42
+
\subtree{
43
+
\taxon{Upshot}
44
+
\p{
45
+
There are no (nontrivial) set-theoretic solutions to the recursive domain equations that arise from \em{higher-order} language constructs.
46
+
}
47
+
}
48
+
}
+5
trees/dt-0008.tree
+5
trees/dt-0008.tree
+15
trees/dt-0009.tree
+15
trees/dt-0009.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{flat domains and information ordering}
4
+
\transclude{dt-000A}
5
+
\transclude{dt-0008}
6
+
\transclude{dt-000B}
7
+
\transclude{dt-000C}
8
+
\scope{
9
+
\put\transclude/toc{false}
10
+
\put\transclude/numbered{false}
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]].}
14
+
}
15
+
}
+5
trees/dt-000A.tree
+5
trees/dt-000A.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{the bottom value}
4
+
\p{Following [Scott](danascott), we introduce a special \em{bottom} value #{\bot} to our semantic domains.
5
+
##{\bot\ \text{represents}\ \begin{cases}\text{an undefined value;}\\\text{an error value;}\\\text{a \emph{non-terminating} computation.} \end{cases}}}
+6
trees/dt-000B.tree
+6
trees/dt-000B.tree
···
1
+
\import{dt-macros}
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.}
+23
trees/dt-000C.tree
+23
trees/dt-000C.tree
···
1
+
\import{dt-macros}
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}:}
6
+
\figure{\tex{\usepackage{tikz}}{\begin{tikzpicture}
7
+
\node (d1) at (-1,0) {$\cdots$};
8
+
\node (d2) at (4,0) {$\cdots$};
9
+
\node (d4) at (3.5,-1) {$\cdots$};
10
+
\node (d4) at (-0.5,-1) {$\cdots$};
11
+
\node[anchor=west] (d3) at (5,-2) {(bottom)};
12
+
\node[anchor=west] (d3) at (5,0) {(elements of $X$)};
13
+
\node (a1) at (0,0) {$\bullet$} ;
14
+
\node (a2) at (1,0) {$\bullet$} ;
15
+
\node (a3) at (2,0) {$\bullet$} ;
16
+
\node (a4) at (3,0) {$\bullet$} ;
17
+
\node (bot) at (1.5,-2) {$\bot$};
18
+
\draw[ thick] (bot) -- (a1);
19
+
\draw[ thick] (bot) -- (a2);
20
+
\draw[ thick] (bot) -- (a3);
21
+
\draw[ thick] (bot) -- (a4);
22
+
\end{tikzpicture}}}
23
+
\p{Formally, we say #{x \sqsubseteq y} iff #{(x = y \lor x = \bot)}.}
+8
trees/dt-000D.tree
+8
trees/dt-000D.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{combining domains}
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.}
6
+
\transclude{dt-000G}
7
+
\transclude{dt-000E}
8
+
\transclude{dt-000F}
+8
trees/dt-000E.tree
+8
trees/dt-000E.tree
···
1
+
\import{dt-macros}
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:
6
+
##{ (x,y) \sqsubseteq_{X \times Y} (x',y') \quad \text{iff} \quad x \sqsubseteq_X x' \land y \sqsubseteq_Y y' }
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)}.}
+30
trees/dt-000F.tree
+30
trees/dt-000F.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\taxon{example}
4
+
\title{the domain #{\mathbb{B}_\bot \times \mathbb{B}_\bot}}
5
+
\figure{\tex{\usepackage{tikz}}{
6
+
\begin{tikzpicture}
7
+
\node (ff) at (0,1) {$(F,F)$};
8
+
\node (ft) at (1.5,1) {$(F,T)$};
9
+
\node (tf) at (3,1) {$(T,F)$};
10
+
\node (tt) at (4.5,1) {$(T,T)$};
11
+
\node (fb) at (0,-1) {$(F,\bot)$};
12
+
\node (bt) at (1.5,-1) {$(\bot,T)$};
13
+
\node (bf) at (3,-1) {$(\bot,F)$};
14
+
\node (tb) at (4.5,-1) {$(T,\bot)$};
15
+
\node (bb) at (2.25,-3) {$(\bot,\bot)$};
16
+
\draw[thick] (bb) -- (fb)
17
+
(bb) -- (bt)
18
+
(bb) -- (bf)
19
+
(bb) -- (tb)
20
+
(fb.north) -- (ft)
21
+
(fb.north) -- (ff)
22
+
(bt.north) -- (tt)
23
+
(bt.north) -- (ft);
24
+
\draw[thick,preaction={draw, line width=5pt, white}] (bf.north) -- (ff)
25
+
(bf.north) -- (tf)
26
+
(tb.north) -- (tt)
27
+
(tb.north) -- (tf);
28
+
\end{tikzpicture}
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]].}
+5
trees/dt-000G.tree
+5
trees/dt-000G.tree
+20
trees/dt-000H.tree
+20
trees/dt-000H.tree
···
1
+
\import{dt-macros}
2
+
\title{Monotonic Functions}
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:}
5
+
\transclude{dt-000I}
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
+
Such functions are called \em{monotonic} with respect to our information ordering.}
8
+
\transclude{dt-000J}
9
+
\transclude{dt-000K}
10
+
\scope{
11
+
\put\transclude/toc{false}
12
+
\put\transclude/numbered{false}
13
+
\subtree{
14
+
\taxon{thesis}
15
+
\p{Computable functions are [monotonic](dt-000J) (observe that #{H} is not). }
16
+
}
17
+
}
18
+
19
+
\transclude{dt-000N}
20
+
\transclude{dt-000O}
+8
trees/dt-000I.tree
+8
trees/dt-000I.tree
···
1
+
\import{dt-macros}
2
+
\taxon{example}
3
+
\author{liamoc}
4
+
\title{the halting query}
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
+
##{
7
+
H(v) \; = \; \begin{cases} F & \text{if}\ v = \bot \\ T & \text{otherwise} \end{cases}
8
+
}}
+6
trees/dt-000J.tree
+6
trees/dt-000J.tree
···
1
+
\import{dt-macros}
2
+
\taxon{definition}
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}:
6
+
##{ x \sqsubseteq y\; \text{implies}\; f(x) \sqsubseteq f(y) }}
+5
trees/dt-000K.tree
+5
trees/dt-000K.tree
+12
trees/dt-000L.tree
+12
trees/dt-000L.tree
···
1
+
\import{dt-macros}
2
+
\author{liamoc}
3
+
\title{Recursion}
4
+
\p{So far, our semantic domains have just been (functions of) \em{sets}. While these have the advantage of being mathematically simple and intuitive, two language features make these sets insufficient for our purposes:
5
+
\ol{
6
+
\li{\em{Recursively defined programs}, for dealing with recursion and loops, and}
7
+
\li{\em{Recursively defined semantic domains}, for dealing with \em{higher-order} programs.}
8
+
}
9
+
}
10
+
\transclude{dt-0006}
11
+
\transclude{dt-0007}
12
+
\p{We will return to this problem later on! For now, let's focus on representing non-termination.}
+5
trees/dt-000M.tree
+5
trees/dt-000M.tree
+4
trees/dt-000N.tree
+4
trees/dt-000N.tree
+49
trees/dt-000O.tree
+49
trees/dt-000O.tree
···
1
+
\import{dt-macros}
2
+
\taxon{exercise}
3
+
\author{liamoc}
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
+
\figure{\tex{\usepackage{tikz}}{
6
+
\begin{tikzpicture}
7
+
\node (a) at (0,0) {$\bullet$};
8
+
\node (b) at (1,0) {$\bullet$};
9
+
\draw[->,thick] (a) edge[bend left] (b);
10
+
\end{tikzpicture}}}
11
+
\p{And there are three monotonic functions #{\mathbf{K}_2 \rightarrow \mathbf{K}_2}:}
12
+
\figure{
13
+
\tex{\usepackage{tikz}}{
14
+
\begin{tikzpicture}
15
+
\node (a) at (0,0) {$\bullet$};
16
+
\node (b) at (1,0) {$\bullet$};
17
+
\node (a1) at (0,1) {$\bullet$};
18
+
\node (b1) at (1,1) {$\bullet$};
19
+
\draw[->,thick] (a) edge (b);
20
+
\draw[thick] (b) edge (b1);
21
+
\draw[thick] (a) edge (a1);
22
+
\draw[->,thick] (a1) edge (b1);
23
+
\end{tikzpicture}$\quad$
24
+
\begin{tikzpicture}
25
+
\node (a) at (0,0) {$\bullet$};
26
+
\node (b) at (1,0) {$\bullet$};
27
+
\node (a1) at (0,1) {$\bullet$};
28
+
\node (b1) at (1,1) {$\bullet$};
29
+
\draw[thick] (b) edge (b1);
30
+
\draw[->,thick] (a) edge (b);
31
+
\draw[thick] (a) edge (a1);
32
+
\draw[->,thick] (a1) edge (b);
33
+
\end{tikzpicture}$\quad$
34
+
\begin{tikzpicture}
35
+
\node (a) at (0,0) {$\bullet$};
36
+
\node (b) at (1,0) {$\bullet$};
37
+
\node (a1) at (0,1) {$\bullet$};
38
+
\node (b1) at (1,1) {$\bullet$};
39
+
\draw[->,thick] (a) edge (b1);
40
+
\draw[thick] (a) edge (a1);
41
+
\draw[thick] (b) edge (b1);
42
+
\draw[->,thick] (a1) edge (b1);
43
+
\end{tikzpicture}
44
+
}
45
+
}
46
+
\ol{
47
+
\li{ Write down the monotonic functions #{\mathbf{K}_3 \rightarrow \mathbf{K}_3}.}
48
+
\li{ Write a simple recursive program to calculate the number of monotonic functions #{\mathbf{K}_n \rightarrow \mathbf{K}_m}.}
49
+
}
+9
trees/dt-000P.tree
+9
trees/dt-000P.tree
+7
trees/dt-000Q.tree
+7
trees/dt-000Q.tree
···
1
+
\import{dt-macros}
2
+
\taxon{exercise}
3
+
\author{liamoc}
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.}
7
+
}
+22
trees/dt-000R.tree
+22
trees/dt-000R.tree
···
1
+
\import{dt-macros}
2
+
\title{From recursion to fixed points}
3
+
\author{liamoc}
4
+
\p{
5
+
Consider our recursive \syn{while} loop semantics from \ref{dt-0006}:
6
+
7
+
##{
8
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ \sigma\; = \; \begin{cases} \llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
9
+
\sigma & \text{otherwise}
10
+
\end{cases}
11
+
}
12
+
How do we ensure that solutions exist for such recursive equations? And, if multiple solutions exist, how do we decide which one to pick? To address these questions, let's factor out everything in our definition except the recursion into a separate (higher-order) function:
13
+
##{
14
+
\begin{array}{l}
15
+
\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C} = f(\llbracket \mathsf{while}\ b\ \mathsf{do}\ c\ \mathsf{od} \rrbracket_\mathcal{C}) \\[0.5em]
16
+
\qquad \text{where}\; f(X)\ \sigma\; \triangleq \; \begin{cases} X\ (\llbracket c \rrbracket_\mathcal{C}\ \sigma) & \text{if}\ \llbracket b \rrbracket_\mathcal{B}\ \sigma = T \\
17
+
\sigma & \text{otherwise}
18
+
\end{cases}
19
+
\end{array}
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.
22
+
}
+6
trees/dt-000S.tree
+6
trees/dt-000S.tree
+11
trees/dt-000T.tree
+11
trees/dt-000T.tree
···
1
+
\import{dt-macros}
2
+
\title{Monotonicity is insufficient}
3
+
\author{liamoc}
4
+
\scope{
5
+
\put\transclude/toc{false}
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!}
9
+
}}
10
+
\p{So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists. }
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.}
+7
trees/dt-000U.tree
+7
trees/dt-000U.tree
+5
trees/dt-macros.tree
+5
trees/dt-macros.tree
+8
-10
trees/index.tree
+8
-10
trees/index.tree
···
1
1
\author{liamoc}
2
-
\title{Hello, World!}
3
-
\p{
4
-
Welcome to your first tree! This tree is the root of your forest.
5
-
\ul{
6
-
\li{[Build and view your forest for the first time](http://www.jonmsterling.com/jms-007D.xml)}
7
-
\li{[Overview of the Forester markup language](http://www.jonmsterling.com/jms-007N.xml)}
8
-
\li{[Creating new trees](http://www.jonmsterling.com/jms-007H.xml)}
9
-
\li{[Creating your personal biographical tree](http://www.jonmsterling.com/jms-007K.xml)}
10
-
}
11
-
}
2
+
\meta{author}{false}
3
+
\title{Liam O'Connor}
4
+
\scope{
5
+
\put\transclude/toc{false}
6
+
\put\transclude/heading{false}
12
7
\transclude{liamoc}
8
+
\put\transclude/heading{true}
9
+
\transclude{news}
10
+
}
+42
trees/loc-0001.tree
+42
trees/loc-0001.tree
···
1
+
\import{refs-datalog}
2
+
\title{works of [[liamoc]]}
3
+
\taxon{bibliography}
4
+
\author{liamoc}
5
+
6
+
7
+
\subtree{
8
+
\title{refereed papers}
9
+
\query\datalog{
10
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{refereed}}
11
+
}
12
+
}
13
+
14
+
15
+
\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}
39
+
\query\datalog{
40
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{thesis}}
41
+
}
42
+
}
+39
trees/loc-0002.tree
+39
trees/loc-0002.tree
···
1
+
\title{students}
2
+
\author{liamoc}
3
+
\subtree{
4
+
\title{doctoral students}
5
+
\ul{
6
+
\li{ [[rayhana]]: 2023–present. Linear Temporal Logic with finite observations. Jointly supervised with [[rvg]] at the [[uoe]]. }
7
+
}
8
+
\scope{
9
+
\put\transclude/toc{false}
10
+
\subtree{
11
+
\title{secondary supervisions}
12
+
\ul{
13
+
\li{ [[tudor]]: 2021–present, primary supervisor is [[wadler]] at the [[uoe]]. }
14
+
\li{ [[mathieu]]: 2022–present, primary supervisor is [[tgrosser]] at the [[cam]]. }
15
+
}
16
+
}}
17
+
}
18
+
19
+
\subtree{
20
+
\title{masters students}
21
+
\ul{
22
+
\li{ Shaonan Li: 2022, [[uoe]]. \em{Exploring the 8-bit demoscene.}}
23
+
}
24
+
}
25
+
26
+
\subtree{
27
+
\title{bachelors students}
28
+
\ul{
29
+
\li{[[jackb]]: 2025, [[anu]] Semester Project. \em{A File Format for Holbert Proofs.}}
30
+
\li{[[sandwichman]]: 2023-2024, [[uoe]]. \em{Concurrent Games in Agda.}}
31
+
\li{[[sandwichman]]: 2023, [[uoe]] LFCS Internship Project. \em{Branching Bisimulation Games in Agda.}}
32
+
\li{[[aria]]: 2023-2024, [[uoe]]. \em{Candelabra: Efficient selection of ideal container implementations.}}
33
+
\li{Scott Maxwell: 2023-2024, [[uoe]]. \em{Metamorphosis: An automatic collection implementation selector.}}
34
+
\li{[[keshen]]: 2022-2023, [[uoe]]. \em{Formal Verification of Partition Refinement Algorithms.}}
35
+
\li{[[rayhana]]: 2021-2022, [[uoe]]. \em{Equality and Rewriting in the Holbert Proof Assistant.}}
36
+
\li{Chris Perceval-Maxwell: 2021-2022, [[uoe]]. \em{Elimination and Induction in the Holbert Proof Assistant.}}
37
+
\li{Yining Liu: 2021-2022, [[uoe]]. \em{Textbook Features in the Holbert Proof Assistant.}}
38
+
}
39
+
}
+49
trees/loc-0003.tree
+49
trees/loc-0003.tree
···
1
+
\title{academic community roles}
2
+
\author{liamoc}
3
+
4
+
\ul{
5
+
\li{ Observer, [[wg21]], 2024–present.}
6
+
\li{ Organiser, [[icfpc25]], 2025. }
7
+
\li{ Editor (Social Media), [[jfp]], 2020–present. }
8
+
\li{ Member at Large, [[tyde]] Steering Committee, 2022–2024. }
9
+
\li{ Publicity Chair, [[spli]], 2022–2024. }
10
+
\li{ Organiser and Designer, [[typesig]] Advent of Proof, 2023. }
11
+
\li{ Problem Designer, [[typesig]] Advent of Proof, 2024. }
12
+
}
13
+
14
+
\subtree{
15
+
\title{program committees}
16
+
\ul{
17
+
\li{[[haskell25]]}
18
+
\li{[[fproper25]]}
19
+
\li{[[aplas25]]}
20
+
\li{[[icfp25]]}
21
+
\li{[[pldi25]]}
22
+
\li{[[sblp24]]}
23
+
\li{[[pepm24]]}
24
+
\li{[[aplas23]]}
25
+
\li{[[sblp22]]}
26
+
\li{[[icfpsrc21]]}
27
+
\li{[[tyde17]]}
28
+
}
29
+
}
30
+
31
+
\subtree{
32
+
\title{other reviewing}
33
+
\ul{
34
+
\li{External Review, [[tase23]]}
35
+
\li{External Review, [[esop22]]}
36
+
\li{External Review, [[fossacs21]]}
37
+
\li{External Review, [[jfp]], 2020}
38
+
\li{External Review, [[cpp18]]}
39
+
\li{External Review, [[popl16]]}
40
+
\li{Artifact Evaluation, [[icfp18]]}
41
+
\li{Subreviewer, [[csf19]]}
42
+
\li{Subreviewer, [[asplos19]]}
43
+
\li{Subreviewer, [[itp17]]}
44
+
\li{Subreviewer, [[icfp15]]}
45
+
\li{Subreviewer, [[popl15]]}
46
+
\li{Subreviewer, [[icfp14]]}
47
+
\li{Subreviewer, [[aplas13]]}
48
+
}
49
+
}
+11
trees/loc-0004.tree
+11
trees/loc-0004.tree
+27
trees/loc-0005.tree
+27
trees/loc-0005.tree
···
1
+
\import{table-macros}
2
+
\title{education}
3
+
\author{liamoc}
4
+
5
+
\scope{
6
+
\put\transclude/toc{false}
7
+
\subtree{
8
+
\title{Doctor of Philosophy (Computer Science), [[unsw]]}
9
+
\meta{venue}{[[unsw]]}
10
+
\ul{
11
+
\li{ \em{Thesis:} [[oconnor-thesis-2019]]. \br Winner of the [[core]] John Makepeace Bennett Dissertation Award. \br Project received the [[nicta]] Impact Award. \br Nominated for the [[unsw]] Malcolm Chaikin Prize. }
12
+
\li{ \em{Primary Advisor:} [[gckeller]]. \br \em{Secondary Advisors:} [[heiser]], [[crizkallah]]. }
13
+
}
14
+
}
15
+
16
+
\subtree{
17
+
\title{Bachelor of Science (Hons), Computer Science, [[unsw]]}
18
+
\meta{venue}{[[unsw]]}
19
+
\ul{
20
+
\li{ Honours First Class. Dean's List. \br
21
+
Winner of the CSE Undergraduate Performance Award in 2012, 2011 and 2008.\br
22
+
Winner of the Macquarie Bank Performance Award, 2008 }
23
+
\li{ \em{Thesis:} [[oconnor-ug-thesis-2012]]. }
24
+
\li{ \em{Advisor:} [[chak]]. }
25
+
}
26
+
}
27
+
}
+14
trees/loc-0006.tree
+14
trees/loc-0006.tree
···
1
+
\import{table-macros}
2
+
\title{professional history}
3
+
\author{liamoc}
4
+
\ul{
5
+
\li{2024–present: \strong{Senior Lecturer}, [[anu]]\br
6
+
\em{Foundations Cluster}\br
7
+
Foundations Computing Facilities Representative (2024–present)}
8
+
\li{2020–2024: \strong{Lecturer}, [[uoe]] \br \em{Laboratory for Foundations of Computer Science (LFCS)} \br LFCS Postgraduate Research Coordinator (2022–2024), LFCS EDI Representative (2021–2022)}
9
+
\li{2019–2020: \strong{Senior Research Officer}, [[unsw]].}
10
+
\li{2009–2020: \strong{Casual Academic} (Teaching), [[unsw]].}
11
+
\li{2013–2014: \strong{Research Engineer}, [[nicta]].}
12
+
\li{2011–2013: \strong{Research Assistant}, [[nicta]].}
13
+
\li{2009–2010: \strong{Software Engineer} (Internship), [[google-syd]].}
14
+
}
+60
trees/loc-0007.tree
+60
trees/loc-0007.tree
···
1
+
\import{table-macros}
2
+
\title{teaching}
3
+
\author{liamoc}
4
+
\p{The following teaching engagements were/are all at [[anu]]:}
5
+
\table{
6
+
\tr{\td{2025}\td{ [[COMP1100]]. Lecturer.}}
7
+
}
8
+
\p{The following teaching engagements were all at [[uoe]]:}
9
+
\table{
10
+
\tr{\td{2024}\td{ [[typesig-dt]] (15 students). Invited Lecturer.}}
11
+
\tr{\td{}\td{ [[mcs]] (30 students). Lecturer Convenor, Tutor.}}
12
+
\tr{\td{2023} \td{[[itcs]] (40 students). Lecturer Convenor.}}
13
+
\tr{\td{}\td{ [[dmp]]. Tutor.}}
14
+
\tr{ \td{2022} \td{[[itcs]] (20 students). Lecturer Convenor.}}
15
+
\tr{ \td{} \td{[[inf1a]]. Tutor.}}
16
+
\tr{ \td{2021} \td{[[itcs]] (35 students). Lecturer, Tutor.}}
17
+
\tr{ \td{} \td{[[inf1a]]. Tutor.}}
18
+
\tr{ \td{2020} \td{[[inf1a]]. Tutor Supervisor.}}
19
+
}
20
+
21
+
\p{The following teaching engagements were all at [[unsw]]:
22
+
\table{
23
+
\tr{\td{2020}\td{ [[COMP3161]] (190 students). Lecturer.}}
24
+
\tr{\td{}\td{ [[COMP3151]] (28 students). Lecturer Convenor.}}
25
+
\tr{\td{}\td{ [[COMP3141]] (308 students). Lecturer Convenor. }}
26
+
\tr{\td{}\td{ [[COMP3153]] (18 students). Lecturer Convenor. }}
27
+
\tr{\td{}\td{ [[COMP2111]]. Course Administrator.}}
28
+
\tr{\td{2019}\td{ [[COMP3161]] (111 students). \br \small{#{100\%} teacher satisfaction. #{95.1\%} course satisfaction.} }}
29
+
\tr{\td{}\td{ [[COMP3141]] (196 students). Lecturer Convenor. \br \small{ #{97.3\%} teacher satisfaction. #{93.9\%} course satisfaction.}}}
30
+
\tr{\td{2018}\td{ [[COMP3161]] (96 students). Lecturer Convenor, Tutor. \br \small{#{98.1\%} teacher satisfaction. #{100\%} course satisfaction.}}}
31
+
\tr{\td{}\td{ [[COMP2111]]. Tutor (6 tutorials), Relief Lecturer.}}
32
+
\tr{\td{}\td{ \small{#{94.1\%} teacher satisfaction.}}}
33
+
\tr{\td{}\td{ [[COMP3141]]. Course Designer and Administrator.}}
34
+
\tr{\td{}\td{ [[COMP6752]]. Tutor (1 tutorial).}}
35
+
\tr{\td{2017}\td{ [[COMP3151]]. Tutor (3 tutorials), Relief Lecturer.}}
36
+
\tr{\td{}\td{ [[COMP3141]]. Course Administrator.}}
37
+
\tr{\td{}\td{ [[COMP3161]]. Tutor (4 tutorials), Relief Lecturer.}}
38
+
\tr{\td{}\td{ [[COMP2111]]. Tutor (5 tutorials), Relief Lecturer.}}
39
+
\tr{\td{2016}\td{ [[COMP3141]]. Course Administrator, Relief Lecturer.}}
40
+
\tr{\td{}\td{ [[COMP3161]]. Tutor (3 tutorials), Relief Lecturer.}}
41
+
\tr{\td{}\td{ [[COMP2111]]. Tutor (4 tutorials), Relief Lecturer.}}
42
+
\tr{\td{2015}\td{ [[COMP3141]]. Course Administrator, Relief Lecturer.}}
43
+
\tr{\td{}\td{ [[COMP3161]]. Tutor (3 tutorials), Relief Lecturer.}}
44
+
\tr{\td{}\td{ [[COMP2111]]. Tutor (3 tutorials).}}
45
+
\tr{\td{}\td{ [[SENG2011]]. Tutor (3 tutorials).}}
46
+
\tr{\td{2014}\td{ [[COMP3161]]. Tutor (3 tutorials), Relief Lecturer.}}
47
+
\tr{\td{}\td{ [[SENG2011]]. Tutor (3 tutorials).}}
48
+
\tr{\td{}\td{ [[COMP1927]]. Tutor (2 tute/labs), Relief Lecturer.}}
49
+
\tr{\td{2013}\td{ [[COMP3161]]. Tutor (2 tutorials), Relief Lecturer.}}
50
+
\tr{\td{}\td{ [[COMP3151]]. Tutor (2 tutorials), Relief Lecturer.}}
51
+
\tr{\td{2012}\td{ [[COMP1927]]. Tutor (2 tute/labs), Relief Lecturer, Developing Assignments.}}
52
+
\tr{\td{2011}\td{ [[COMP3161]]. Tutor (2 tutorials), Developing Assignments.}}
53
+
\tr{\td{}\td{ [[COMP3141]]. Tutor (1 disabled student).}}
54
+
\tr{\td{}\td{ [[COMP1927]]. Tutor (2 tute/labs).}}
55
+
\tr{\td{2010}\td{ [[COMP3161]]. Tutor (3 tutorials).}}
56
+
\tr{\td{}\td{ [[COMP2911]]. Tutor (2 tutorials, 2 consultation hours).}}
57
+
\tr{\td{2009}\td{ [[COMP1927]]. Tutor (1 tute/lab, 3 consultation hours), Developing Assignments.}}
58
+
\tr{\td{}\td{ [[COMP1911]]. Tutor (1 tute/lab).}}
59
+
}
60
+
}
+5
trees/loc-0008.tree
+5
trees/loc-0008.tree
···
1
+
\title{research themes}
2
+
\author{liamoc}
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
+
\p{I enjoy applying theory to practice: developing programming languages and tools based on established theoretical models and techniques.}
5
+
\p{I also enjoy applying \em{practice} to \em{theory}, that is, developing new theoretical understanding motivated by practical needs.}
+5
trees/loc-0009.tree
+5
trees/loc-0009.tree
···
1
+
\title{contact}
2
+
\author{liamoc}
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
+
\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).}
5
+
\p{If you are in posession of my telephone number, please avoid calling unless absolutely necessary.}
+8
trees/loc-000A.tree
+8
trees/loc-000A.tree
···
1
+
\import{refs-datalog}
2
+
\title{property-based testing}
3
+
\taxon{Research Theme}
4
+
\author{liamoc}
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.}
6
+
\query\datalog{
7
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{pbt}}
8
+
}
+8
trees/loc-000B.tree
+8
trees/loc-000B.tree
···
1
+
\import{refs-datalog}
2
+
\title{temporal logic}
3
+
\taxon{Research Theme}
4
+
\author{liamoc}
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.}
6
+
\query\datalog{
7
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{temporal-logic}}
8
+
}
+10
trees/loc-000C.tree
+10
trees/loc-000C.tree
···
1
+
\import{refs-datalog}
2
+
\title{semantics}
3
+
\author{liamoc}
4
+
\taxon{Research Theme}
5
+
\p{While I haven't had much opportunity to do research purely in semantics, I am fascinated by the field and eager to work on problems in that area.}
6
+
\p{This can range from denotational semantics of programming languages, to concurrency semantics, to the semantics of logics.}
7
+
8
+
\query\datalog{
9
+
?X -: {\rel/my-references ?X} {\rel/has-tag ?X '{semantics}}
10
+
}
+5
trees/loc-000D.tree
+5
trees/loc-000D.tree
···
1
+
\title{Ngunnawal and Ngambri country}
2
+
\author{liamoc}
3
+
\p{The Ngunnawal (/ŋʌnəwəl/) and Ngambri (/ŋæmbɾi/) peoples are the original inhabitants and custodians of the land on which Canberra, the capital city of Australia, is built. They lived here for over 20,000 years before white settler colonisation.}
4
+
\p{The National Museum of Australia shares some of their [community stories](https://www.nma.gov.au/learn/encounters-education/community-stories/canberra).}
5
+
\p{The indigenous inhabitants of Australia had their land taken from them. The least we can do is pay our respects to them and their elders, past and present. }
+47
trees/news.tree
+47
trees/news.tree
···
1
+
\import{table-macros}
2
+
\title{News}
3
+
\author{liamoc}
4
+
\table{
5
+
\tr{
6
+
\th{ 2025-03-22 }
7
+
\td{I have joined the PC for [[haskell25]]. }
8
+
}
9
+
\tr{
10
+
\th{ 2025-03-13 }
11
+
\td{I have joined the PC for [[fproper25]]. }
12
+
}
13
+
\tr{
14
+
\th{ 2025-02-04 }
15
+
\td{ [[jackb]] has joined me for a semester project working on [Holbert](oconnor-amjad-2022). }
16
+
}
17
+
\tr{
18
+
\th{ 2025-01-08 }
19
+
\td{I have joined the PC for [[aplas25]]. }
20
+
}
21
+
\tr{
22
+
\th{ 2024-11-05 }
23
+
\td{I have joined the PC for [[icfp25]]. }
24
+
}
25
+
\tr{
26
+
\th{ 2024-10-22 }
27
+
\td{I have joined the PC for [[pldi25]]. }
28
+
}
29
+
\tr{
30
+
\th{ 2024-09-17 }
31
+
\td{I have agreed to organise the [[icfpc25]]. }
32
+
}
33
+
\tr{
34
+
\th{2024-09-30 }
35
+
\td{I was delighted to spend a week with the [WG2.1](wg21) folks here at the [ANU](anu).}
36
+
}
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). }
40
+
}
41
+
\tr{
42
+
\th{ 2024-07-30 }
43
+
\td{I have taken a new position as a Senior Lecturer at the [[anu]]. }
44
+
}
45
+
46
+
47
+
}
+6
trees/people/amblafont.tree
+6
trees/people/amblafont.tree
+6
trees/people/aria.tree
+6
trees/people/aria.tree
+6
trees/people/ccm.tree
+6
trees/people/ccm.tree
+5
trees/people/cgunter.tree
+5
trees/people/cgunter.tree
+5
trees/people/chak.tree
+5
trees/people/chak.tree
+6
trees/people/craigmcl.tree
+6
trees/people/craigmcl.tree
+6
trees/people/crizkallah.tree
+6
trees/people/crizkallah.tree
+5
trees/people/danascott.tree
+5
trees/people/danascott.tree
+6
trees/people/gklein.tree
+6
trees/people/gklein.tree
+5
trees/people/gwinskel.tree
+5
trees/people/gwinskel.tree
+6
trees/people/haskellhutt.tree
+6
trees/people/haskellhutt.tree
+6
trees/people/heiser.tree
+6
trees/people/heiser.tree
+10
trees/people/hoefner.tree
+10
trees/people/hoefner.tree
+4
trees/people/jackb.tree
+4
trees/people/jackb.tree
+6
trees/people/jcb.tree
+6
trees/people/jcb.tree
+4
trees/people/jstoy.tree
+4
trees/people/jstoy.tree
+3
trees/people/kaie.tree
+3
trees/people/kaie.tree
+4
trees/people/keshen.tree
+4
trees/people/keshen.tree
+6
trees/people/lcheung.tree
+6
trees/people/lcheung.tree
+6
-5
trees/people/liamoc.tree
+6
-5
trees/people/liamoc.tree
···
1
+
\import{table-macros}
1
2
\title{Liam O'Connor}
2
3
\taxon{person}
3
4
\meta{external}{https://liamoc.net}
4
5
\meta{institution}{[[anu]]}
5
6
\meta{orcid}{0000-0003-2765-4269}
6
7
\meta{position}{Senior Lecturer}
8
+
\<html:img>[class]{portrait}[src]{\route-asset{assets/me.jpeg}}
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.}
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.}
7
12
8
-
\p{I am a Senior Lecturer in Foundations at the [[anu]] School of Computing, and Honorary Fellow at the [[uoe]] Laboratory for Foundations of Computer Science. Previously, I lectured courses at [[unsw]], where I did my PhD with [[gckeller]].}
9
-
10
-
11
-
12
-
13
+
\p{More details about me can be found on my [[loc-0004]].}
+6
trees/people/mathieu.tree
+6
trees/people/mathieu.tree
+6
trees/people/msteuwer.tree
+6
trees/people/msteuwer.tree
+10
trees/people/ohad.tree
+10
trees/people/ohad.tree
+5
trees/people/owickstrom.tree
+5
trees/people/owickstrom.tree
+8
trees/people/rayhana.tree
+8
trees/people/rayhana.tree
+6
trees/people/rvg.tree
+6
trees/people/rvg.tree
+6
trees/people/sandwichman.tree
+6
trees/people/sandwichman.tree
···
1
+
\title{Amy Yin}
2
+
\taxon{person}
3
+
\meta{external}{https://github.com/yinamy}
4
+
\meta{institution}{[[cam]]}
5
+
\meta{position}{Masters Student}
6
+
\p{Former student of [[liamoc]] at the [[uoe]], now pursuing a masters at the [[cam]] before embarking on a PhD either at the [[cam]] or the [[uoe]]. Co-founder of [[typesig]].}
+6
trees/people/tgrosser.tree
+6
trees/people/tgrosser.tree
+6
trees/people/tobym.tree
+6
trees/people/tobym.tree
+6
trees/people/tsewell.tree
+6
trees/people/tsewell.tree
+6
trees/people/tudor.tree
+6
trees/people/tudor.tree
+6
trees/people/vjackson.tree
+6
trees/people/vjackson.tree
+6
trees/people/wadler.tree
+6
trees/people/wadler.tree
+6
trees/people/yutakang.tree
+6
trees/people/yutakang.tree
+6
trees/people/zilinc.tree
+6
trees/people/zilinc.tree
+1
trees/places/anu.tree
+1
trees/places/anu.tree
+6
trees/places/aplas13.tree
+6
trees/places/aplas13.tree
+7
trees/places/aplas23.tree
+7
trees/places/aplas23.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{APLAS '23}{21st Asian Symposium on Programming Languages and Systems}}
3
+
\taxon{Conference}
4
+
\meta{external}{https://conf.researchr.org/home/aplas-2023}
5
+
\meta{doi}{10.1007/978-981-99-8311-7}
6
+
\date{2025-10}
7
+
\meta{venue}{[[sinica]]}
+6
trees/places/aplas25.tree
+6
trees/places/aplas25.tree
+7
trees/places/asplos16.tree
+7
trees/places/asplos16.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2872362}
4
+
\title{\conf-name{ASPLOS '16}{Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems}}
5
+
\date{2016-03}
6
+
\meta{venue}{Atlanta, Georgia, USA}
7
+
\meta{external}{https://research.ece.cmu.edu/~calcm/asplos2016/}
+7
trees/places/asplos19.tree
+7
trees/places/asplos19.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3297858}
4
+
\title{\conf-name{ASPLOS '19}{24th International Conference on Architectural Support for Programming Languages and Operating Systems}}
5
+
\date{2019-04}
6
+
\meta{venue}{Providence, Rhode Island, USA}
7
+
\meta{external}{https://asplos-conference.org/asplos2019/index.html}
+4
trees/places/cam.tree
+4
trees/places/cam.tree
+4
trees/places/cmu.tree
+4
trees/places/cmu.tree
+1
trees/places/conf-name-macros.tree
+1
trees/places/conf-name-macros.tree
···
1
+
\def\conf-name[short][long]{\em{\short}: \long}
+7
trees/places/core.tree
+7
trees/places/core.tree
···
1
+
\title{CORE}
2
+
\taxon{institution}
3
+
\meta{venue}{Australia}
4
+
\meta{external}{https://www.core.edu.au/}
5
+
\p{
6
+
The Computing Research and Education Association of Australasia, CORE Inc., is an association of university departments of computer science in Australia and New Zealand.
7
+
}
+8
trees/places/cpp18.tree
+8
trees/places/cpp18.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3176245}
4
+
\title{\conf-name{CPP '18}{7th ACM SIGPLAN International Conference on Certified Programs and Proofs}}
5
+
\date{2018-01}
6
+
\meta{venue}{Los Angeles, California, USA}
7
+
\meta{external}{https://popl18.sigplan.org/track/CPP-2018}
8
+
\p{Colocated with POPL'18.}
+9
trees/places/cpp22.tree
+9
trees/places/cpp22.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3497775}
4
+
\title{\conf-name{CPP '22}{11th ACM SIGPLAN International Conference on Certified Programs and Proofs}}
5
+
\date{2022-01}
6
+
\meta{venue}{Philadelphia, Pennsylvania, USA}
7
+
\meta{external}{https://popl22.sigplan.org/home/CPP-2022}
8
+
9
+
\p{Colocated with POPL'22.}
+7
trees/places/csf19.tree
+7
trees/places/csf19.tree
+7
trees/places/csiro.tree
+7
trees/places/csiro.tree
···
1
+
\title{CSIRO}
2
+
\taxon{institution}
3
+
\meta{venue}{Australia}
4
+
\meta{external}{https://www.csiro.au/en/}
5
+
\p{
6
+
The Commonwealth Scientific and Industrial Research Organisation (CSIRO) is an Australian Government agency that is responsible for scientific research and its commercial and industrial applications.
7
+
}
+7
trees/places/data61.tree
+7
trees/places/data61.tree
+8
trees/places/esop22.tree
+8
trees/places/esop22.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{ESOP '22}{31st European Symposium on Programming}}
4
+
\date{2022-04}
5
+
\meta{venue}{Munich, Germany}
6
+
\meta{doi}{10.1007/978-3-030-99336-8}
7
+
\meta{external}{https://etaps.org/2022/esop}
8
+
\p{ Held as Part of the European Joint Conferences on Theory and Practice of Software.}
+8
trees/places/expresssos24.tree
+8
trees/places/expresssos24.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2872362}
4
+
\title{\conf-name{EXPRESS/SOS '24}{Combined 31st International Workshop on Expressiveness in Concurrency and 21st Workshop on Structural Operational Semantics}}
5
+
\date{2024-11}
6
+
\meta{venue}{Calgary, Canada}
7
+
\meta{external}{https://express-sos2022.github.io/}
8
+
\p{Colocated with CONCUR'24.}
+8
trees/places/fossacs21.tree
+8
trees/places/fossacs21.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{FoSSaCS '21}{24th International Conference on Foundations of Software Science and Computation Structures}}
4
+
\date{2021-03}
5
+
\meta{venue}{Luxembourg}
6
+
\meta{doi}{10.1007/978-3-030-71995-1}
7
+
\meta{external}{https://etaps.org/2021/fossacs.html}
8
+
\p{ Held as Part of the European Joint Conferences on Theory and Practice of Software.}
+6
trees/places/fproper25.tree
+6
trees/places/fproper25.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{FProPer '25}{2nd ACM SIGPLAN Workshop on Functional Programming for Productivity and Performance}}
4
+
\date{2025-10}
5
+
\meta{venue}{Singapore}
6
+
\meta{external}{https://conf.researchr.org/home/icfp-splash-2025/fproper-2025}
+4
trees/places/google-syd.tree
+4
trees/places/google-syd.tree
+6
trees/places/haskell25.tree
+6
trees/places/haskell25.tree
+6
trees/places/hatra22.tree
+6
trees/places/hatra22.tree
+7
trees/places/icfp14.tree
+7
trees/places/icfp14.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{ICFP '14}{19th ACM SIGPLAN International Conference on Functional Programming}}
4
+
\date{2014-09}
5
+
\meta{doi}{10.1145/2628136}
6
+
\meta{venue}{Gothenburg, Sweden}
7
+
\meta{external}{https://icfpconference.org/icfp2014/}
+7
trees/places/icfp15.tree
+7
trees/places/icfp15.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{ICFP '15}{20th ACM SIGPLAN International Conference on Functional Programming}}
4
+
\date{2015-09}
5
+
\meta{doi}{10.1145/2784731}
6
+
\meta{venue}{Vancouver, British Columbia, Canada}
7
+
\meta{external}{https://icfpconference.org/icfp2015/}
+7
trees/places/icfp16.tree
+7
trees/places/icfp16.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2951913}
4
+
\title{\conf-name{ICFP '16}{21st ACM SIGPLAN International Conference on Functional Programming}}
5
+
\date{2016-09}
6
+
\meta{venue}{Nara, Japan}
7
+
\meta{external}{https://conf.researchr.org/home/icfp-2016}
+6
trees/places/icfp18.tree
+6
trees/places/icfp18.tree
+6
trees/places/icfp21.tree
+6
trees/places/icfp21.tree
+6
trees/places/icfp25.tree
+6
trees/places/icfp25.tree
+6
trees/places/icfpc25.tree
+6
trees/places/icfpc25.tree
+7
trees/places/icfpsrc21.tree
+7
trees/places/icfpsrc21.tree
+4
trees/places/iohk.tree
+4
trees/places/iohk.tree
+8
trees/places/isola18.tree
+8
trees/places/isola18.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1007/978-3-030-03418-4}
4
+
\title{\conf-name{ISoLA '18}{8th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation}}
5
+
\date{2018-11}
6
+
\meta{venue}{Limassol, Cyprus}
7
+
\meta{external}{https://2018.isola-conference.org/}
8
+
\p{ISoLA is an invited papers only conference on formal methods.}
+7
trees/places/itp16.tree
+7
trees/places/itp16.tree
+7
trees/places/itp17.tree
+7
trees/places/itp17.tree
+5
trees/places/jfp.tree
+5
trees/places/jfp.tree
···
1
+
\title{Journal of Functional Programming}
2
+
\taxon{journal}
3
+
\meta{external}{https://www.cambridge.org/core/journals/journal-of-functional-programming}
4
+
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.}
+8
trees/places/ml16.tree
+8
trees/places/ml16.tree
+6
trees/places/nicta.tree
+6
trees/places/nicta.tree
+4
trees/places/nott.tree
+4
trees/places/nott.tree
+4
trees/places/ntu.tree
+4
trees/places/ntu.tree
+4
trees/places/ox.tree
+4
trees/places/ox.tree
+8
trees/places/pepm24.tree
+8
trees/places/pepm24.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{PEPM '24}{ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation}}
4
+
\date{2024-01}
5
+
\meta{venue}{London, United Kingdom}
6
+
\meta{doi}{10.1145/3635800}
7
+
\meta{external}{https://popl24.sigplan.org/home/pepm-2024}
8
+
\p{Colocated with [[popl24]].}
+6
trees/places/philtransA.tree
+6
trees/places/philtransA.tree
···
1
+
\title{Philosophical Transactions of the Royal Society A}
2
+
\taxon{journal}
3
+
\meta{external}{https://royalsocietypublishing.org/journal/rsta}
4
+
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. }
6
+
+7
trees/places/pldi22.tree
+7
trees/places/pldi22.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2525528}
4
+
\title{\conf-name{PLDI '22}{43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation}}
5
+
\date{2022-06}
6
+
\meta{venue}{San Diego, California, USA}
7
+
\meta{external}{https://pldi22.sigplan.org/}
+6
trees/places/pldi25.tree
+6
trees/places/pldi25.tree
+8
trees/places/plos13.tree
+8
trees/places/plos13.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2525528}
4
+
\title{\conf-name{PLOS '13}{Seventh Workshop on Programming Languages and Operating Systems}}
5
+
\date{2013-11}
6
+
\meta{venue}{Farmington, Pennsylvania}
7
+
\meta{external}{https://sigops.org/s/conferences/sosp/2013/plos.html}
8
+
\p{Colocated with SOSP'13.}
+8
trees/places/plos17.tree
+8
trees/places/plos17.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3144555}
4
+
\title{\conf-name{PLOS '17}{Ninth Workshop on Programming Languages and Operating Systems}}
5
+
\date{2017-10}
6
+
\meta{venue}{Shanghai, China}
7
+
\meta{external}{https://plos-workshop.org/2017/}
8
+
\p{Colocated with SOSP'17.}
+4
trees/places/polytechnique.tree
+4
trees/places/polytechnique.tree
+9
trees/places/popl15.tree
+9
trees/places/popl15.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL '15}{42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}}
3
+
\taxon{conference}
4
+
\date{2015-01}
5
+
\meta{doi}{10.1145/2676726}
6
+
\meta{venue}{Mumbai, India}
7
+
\meta{external}{https://popl.mpi-sws.org/2015/}
8
+
9
+
\p{The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.}
+9
trees/places/popl16.tree
+9
trees/places/popl16.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL '16}{43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}}
3
+
\taxon{conference}
4
+
\date{2016-01}
5
+
\meta{doi}{10.1145/2837614}
6
+
\meta{venue}{St. Petersburg, Florida, USA}
7
+
\meta{external}{https://popl16.sigplan.org/}
8
+
9
+
\p{The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.}
+8
trees/places/popl22.tree
+8
trees/places/popl22.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL '22}{49th ACM SIGPLAN Symposium on Principles of Programming Languages}}
3
+
\taxon{conference}
4
+
\date{2022-01}
5
+
\meta{venue}{Philadelphia, Pennsylvania, USA}
6
+
\meta{external}{https://popl22.sigplan.org/}
7
+
8
+
\p{The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.}
+8
trees/places/popl23.tree
+8
trees/places/popl23.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL '23}{50th ACM SIGPLAN Symposium on Principles of Programming Languages}}
3
+
\taxon{conference}
4
+
\date{2023-01}
5
+
\meta{venue}{Boston, Massachusetts, USA}
6
+
\meta{external}{https://popl23.sigplan.org/}
7
+
8
+
\p{The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.}
+8
trees/places/popl24.tree
+8
trees/places/popl24.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL ’24}{51st ACM SIGPLAN Symposium on Principles of Programming Languages}}
3
+
\taxon{conference}
4
+
\date{2024-01}
5
+
\meta{venue}{London, United Kingdom}
6
+
\meta{external}{https://popl24.sigplan.org/}
7
+
8
+
\p{The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementation or application of programming languages.}
+6
trees/places/programming-journal.tree
+6
trees/places/programming-journal.tree
···
1
+
\title{The Art, Science, and Engineering of Programming}
2
+
\taxon{journal}
3
+
\meta{external}{https://programming-journal.org}
4
+
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.}
6
+
\p{The Art, Science, and Engineering of Programming aims at closing this gap by focusing primarily on programming: the art itself (programming styles, pearls, models, languages), the emerging science of understanding what works and what doesn’t work in general and in specific contexts, as well as more established engineering and mathematical perspectives.}
+4
trees/places/qmul.tree
+4
trees/places/qmul.tree
+7
trees/places/sblp22.tree
+7
trees/places/sblp22.tree
+6
trees/places/sblp24.tree
+6
trees/places/sblp24.tree
+4
trees/places/sinica.tree
+4
trees/places/sinica.tree
+7
trees/places/sle22.tree
+7
trees/places/sle22.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3567512}
4
+
\title{\conf-name{SLE '22}{15th ACM SIGPLAN International Conference on Software Language Engineering}}
5
+
\date{2022-12}
6
+
\meta{venue}{Auckland, New Zealand}
7
+
\meta{external}{https://2022.splashcon.org/home/sle-2022}
+4
trees/places/spli.tree
+4
trees/places/spli.tree
+7
trees/places/tase23.tree
+7
trees/places/tase23.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\title{\conf-name{TASE '23}{17th International Symposium on Theoretical Aspects of Software Engineering}}
4
+
\date{2023-07}
5
+
\meta{venue}{Bristol, United Kingdom}
6
+
\meta{doi}{10.1007/978-3-031-35257-7}
7
+
\meta{external}{https://plrg-bristol.github.io/tase2023/index.html}
+8
trees/places/toposinstitute.tree
+8
trees/places/toposinstitute.tree
···
1
+
\title{Topos Institute}
2
+
\taxon{institution}
3
+
\meta{external}{https://topos.institute/}
4
+
5
+
\blockquote{
6
+
\p{We shape technology for public benefit by advancing sciences of connection and integration.}
7
+
\p{Our goal is a world where the systems that surround us benefit us all.}
8
+
}
+4
trees/places/tu-berlin.tree
+4
trees/places/tu-berlin.tree
+4
trees/places/tweag.tree
+4
trees/places/tweag.tree
+6
trees/places/tyde.tree
+6
trees/places/tyde.tree
···
1
+
\taxon{Conference Series}
2
+
\meta{doi}{10.1145/3331554}
3
+
\title{Workshop on Type-Driven Development}
4
+
\meta{external}{https://tydeworkshop.org/}
5
+
6
+
\p{The workshop on Type-driven Development aims to show how static type information may be used effectively in the development of computer programs. Colocated with ICFP, this workshop brings together leading researchers and practitioners who are using or exploring types as a means of program development.}
+9
trees/places/tyde16.tree
+9
trees/places/tyde16.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/2976022}
4
+
\title{\conf-name{TyDe '16}{1st ACM SIGPLAN International Workshop on Type-Driven Development}}
5
+
\date{2016-09}
6
+
\meta{venue}{Nara, Japan}
7
+
\meta{external}{https://tydeworkshop.org/2016}
8
+
9
+
\p{Colocated with [ICFP'16](icfp16). An instance of the [[tyde]].}
+9
trees/places/tyde17.tree
+9
trees/places/tyde17.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3122975}
4
+
\title{\conf-name{TyDe '17}{2nd ACM SIGPLAN International Workshop on Type-Driven Development}}
5
+
\date{2017-09}
6
+
\meta{venue}{[[ox]]}
7
+
\meta{external}{https://tydeworkshop.org/2017}
8
+
9
+
\p{Colocated with ICFP'17. An instance of the [[tyde]].}
+9
trees/places/tyde19.tree
+9
trees/places/tyde19.tree
···
1
+
\import{conf-name-macros}
2
+
\taxon{conference}
3
+
\meta{doi}{10.1145/3331554}
4
+
\title{\conf-name{TyDe '19}{4th ACM SIGPLAN International Workshop on Type-Driven Development}}
5
+
\date{2019-08}
6
+
\meta{venue}{Berlin, Germany}
7
+
\meta{external}{https://icfp19.sigplan.org/home/tyde-2019}
8
+
9
+
\p{Colocated with ICFP'19. An instance of the [[tyde]].}
+4
trees/places/typesig.tree
+4
trees/places/typesig.tree
+4
trees/places/uiuc.tree
+4
trees/places/uiuc.tree
+4
trees/places/unimelb.tree
+4
trees/places/unimelb.tree
+1
trees/places/unsw.tree
+1
trees/places/unsw.tree
+1
trees/places/uoe.tree
+1
trees/places/uoe.tree
+1
trees/places/uu.tree
+1
trees/places/uu.tree
+13
trees/places/wg21.tree
+13
trees/places/wg21.tree
···
1
+
\title{IFIP Working Group 2.1: Algorithmic Languages and Calculi}
2
+
\taxon{institution}
3
+
\meta{external}{https://ifipwg21wiki.cs.kuleuven.be/}
4
+
\p{
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:
6
+
\ul{
7
+
\li{Study of calculation of programs from specifications}
8
+
\li{Design of notations for such calculation}
9
+
\li{Formulation of algorithm theories, using such notations}
10
+
\li{Investigation of software support for program derivation}
11
+
\li{Continuing responsibility for ALGOL 60 and ALGOL 68}
12
+
}
13
+
}
+4
trees/refs-datalog.tree
+4
trees/refs-datalog.tree
+26
trees/refs/amani-hcrcobnlstkmkh-2016.tree
+26
trees/refs/amani-hcrcobnlstkmkh-2016.tree
···
1
+
\title{Cogent: Verifying High-assurance File System Implementations}
2
+
\taxon{reference}
3
+
\meta{venue}{[[asplos16]]}
4
+
\author/literal{Sidney Amani}
5
+
\author/literal{Alex Hixon}
6
+
\author{zilinc}
7
+
\author{crizkallah}
8
+
\author/literal{Peter Chubb}
9
+
\author{liamoc}
10
+
\author/literal{Joel Beeren}
11
+
\author{yutakang}
12
+
\author/literal{Japheth Lim}
13
+
\author{tsewell}
14
+
\author/literal{Joseph Tuong}
15
+
\author{gckeller}
16
+
\author{tobym}
17
+
\author{gklein}
18
+
\author{heiser}
19
+
\date{2016-03-25}
20
+
\meta{doi}{10.1145/2980024.2872404}
21
+
\tag{cogent}
22
+
\tag{refereed}
23
+
\p{
24
+
We present an approach to writing and formally verifying high-assurance file-system code in a restricted language called Cogent, supported by a certifying compiler that produces C code, high-level specification of Cogent, and translation correctness proofs. The language is strongly typed and guarantees absence of a number of common file system implementation errors. We show how verification effort is drastically reduced for proving higher-level properties of the file system implementation by reasoning about the generated formal specification rather than its low-level C code. We use the framework to write two Linux file systems, and compare their performance with their native C implementations.
25
+
}
26
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/Amani_HCRCOBNLSTKMKH_16.abstract)}
+14
trees/refs/amjad-vanglabbeek-oconnor-2024.tree
+14
trees/refs/amjad-vanglabbeek-oconnor-2024.tree
···
1
+
\title{Semantics for Linear-time Temporal Logic with Finite Observations}
2
+
\taxon{reference}
3
+
\meta{venue}{[[expresssos24]]}
4
+
\author{rayhana}
5
+
\author{rvg}
6
+
\author{liamoc}
7
+
\date{2024-11-22}
8
+
\meta{doi}{10.4204/EPTCS.412.4}
9
+
\tag{temporal-logic}
10
+
\tag{semantics}
11
+
\tag{refereed}
12
+
\p{LTL3 is a multi-valued variant of Linear-time Temporal Logic for runtime verification applications. The semantic descriptions of LTL3 in previous work are given only in terms of the relationship to conventional LTL. Our approach, by contrast, gives a full model-based inductive accounting of the semantics of LTL3, in terms of families of definitive prefix sets. We show that our definitive prefix sets are isomorphic to linear-time temporal properties (sets of infinite traces), and thereby show that our semantics of LTL3 directly correspond to the semantics of conventional LTL. In addition, we formalise the formula progression evaluation technique, popularly used in runtime verification and testing contexts, and show its soundness and completeness up to finite traces with respect to our semantics. All of our definitions and proofs are mechanised in Isabelle/HOL.}
13
+
14
+
\meta{source}{[Proofs on AFP](https://www.isa-afp.org/entries/LTL3_Semantics.html)}
+17
trees/refs/chen-lokmjr-2023.tree
+17
trees/refs/chen-lokmjr-2023.tree
···
1
+
\title{Dargent: A Silver Bullet for Verified Data Layout Refinement}
2
+
\taxon{reference}
3
+
\meta{venue}{[[popl23]]}
4
+
\author{zilinc}
5
+
\author{amblafont}
6
+
\author{liamoc}
7
+
\author{gckeller}
8
+
\author{craigmcl}
9
+
\author{vjackson}
10
+
\author{crizkallah}
11
+
\date{2023-01-11}
12
+
\meta{doi}{10.1145/3571240}
13
+
\tag{cogent}
14
+
\tag{refereed}
15
+
16
+
\p{Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed by the implementation of tedious marshalling code to convert between compiler-selected data representations and the desired compact data formats. Such marshalling code is error-prone and can lead to a significant runtime overhead due to excessive copying. While there are many languages and systems that address the correctness issue, by automating the generation and, in some cases, the verification of the marshalling code, the performance overhead introduced by the marshalling code remains. In particular for systems code, this overhead can be prohibitive. In this work, we address both the correctness and the performance problems.}
17
+
\p{We present a data layout description language and data refinement framework, called Dargent, which allows programmers to declaratively specify how algebraic data types are laid out in memory. Our solution is applied to the Cogent language, but the general ideas behind our solution are applicable to other settings. The Dargent framework generates C code that manipulates data directly with the desired memory layout, while retaining the formal proof that this generated C code is correct with respect to the functional semantics. This added expressivity removes the need for implementing and verifying marshalling code, which eliminates copying, smoothens interoperability with surrounding systems, and increases the trustworthiness of the overall system.}
+15
trees/refs/chen-okkh-2017.tree
+15
trees/refs/chen-okkh-2017.tree
···
1
+
\title{The Cogent Case for Property-Based Testing}
2
+
\taxon{reference}
3
+
\meta{venue}{[[plos17]]}
4
+
\author{zilinc}
5
+
\author{liamoc}
6
+
\author{gckeller}
7
+
\author{gklein}
8
+
\author{heiser}
9
+
\date{2017-10-28}
10
+
\meta{doi}{10.1145/3144555.3144556}
11
+
\tag{cogent}
12
+
\tag{pbt}
13
+
\tag{refereed}
14
+
\p{Property-based testing can play an important role in reducing the cost of formal verification: It has been demonstrated to be effective at detecting bugs and finding inconsistencies in specifications, and thus can eliminate effort wasted on fruitless proof attempts. We argue that in addition, property-based testing enables an incremental approach to a fully verified system, by allowing replacement of automatically generated tests of properties stated in the specification by formal proofs. We demonstrate this approach on the verification of systems code, discuss the implications on systems design, and outline the integration of property-based testing into the Cogent framework.}
15
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/Chen_OKKH_17.abstract)}
+20
trees/refs/chen-roskhk-2022.tree
+20
trees/refs/chen-roskhk-2022.tree
···
1
+
2
+
\title{Property-based Testing: Climbing the Stairway to Verification}
3
+
\taxon{reference}
4
+
\meta{venue}{[[sle22]]}
5
+
\author{zilinc}
6
+
\author{crizkallah}
7
+
\author{liamoc}
8
+
\author/literal{Partha Susarla}
9
+
\author{gklein}
10
+
\author{heiser}
11
+
\author{gckeller}
12
+
\date{2022-12-01}
13
+
\meta{doi}{10.1145/3567512.3567520}
14
+
\tag{cogent}
15
+
\tag{pbt}
16
+
\tag{refereed}
17
+
\meta{source}{\strong{Best Artifact Award}}
18
+
\p{Property-based testing (PBT) is a powerful tool that is widely available in modern programming languages. It has been used to reduce formal software verification effort. We demonstrate how PBT can be used in conjunction with formal verification to incrementally gain greater assurance in code correctness by integrating PBT into the verification framework of Cogent---a programming language equipped with a certifying compiler for developing high-assurance systems components. Specifically, for PBT and formal verification to work in tandem, we structure the tests to mirror the refinement proof that we used in Cogent's verification framework: The expected behaviour of the system under test is captured by a functional correctness specification, which mimics the formal specification of the system, and we test the refinement relation between the implementation and the specification. We exhibit the additional benefits that this mutualism brings to developers and demonstrate the techniques we used in this style of PBT, by studying two concrete examples.}
19
+
20
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/papers/Chen_ROSKHK_22.abstract)}
+13
trees/refs/cheung-oconnor-rizkallah-2022.tree
+13
trees/refs/cheung-oconnor-rizkallah-2022.tree
···
1
+
\title{Overcoming Restraint: Composing Verification of Foreign Functions with Cogent}
2
+
\taxon{reference}
3
+
\meta{venue}{[[cpp22]]}
4
+
\author{lcheung}
5
+
\author{liamoc}
6
+
\author{crizkallah}
7
+
\date{2022-01-11}
8
+
\meta{doi}{10.1145/3497775.350368}
9
+
\meta{doi}{10.48550/arXiv.2102.09920}
10
+
\tag{cogent}
11
+
\tag{refereed}
12
+
\p{Cogent is a restricted functional language designed to reduce the cost of developing verified systems code. Because of its sometimes-onerous restrictions, such as the lack of support for recursion and its strict uniqueness type system, Cogent provides an escape hatch in the form of a foreign function interface (FFI) to C code. This poses a problem when verifying Cogent programs, as imported C components do not enjoy the same level of static guarantees that Cogent does. Previous verification of file systems implemented in Cogent merely assumed that their C components were correct and that they preserved the invariants of Cogent’s type system. In this paper, we instead prove such obligations. We demonstrate how they smoothly compose with existing Cogent theorems, and result in a correctness theorem of the overall Cogent-C system. The Cogent FFI constraints ensure that key invariants of Cogent’s type system are maintained even when calling C code. We verify reusable higher-order and polymorphic functions including a generic loop combinator and array iterators and demonstrate their application to several examples including binary search and the BilbyFs file system. We demonstrate the feasibility of verification of mixed Cogent-C systems, and provide some insight into verification of software comprised of code in multiple languages with differing levels of static guarantees.}
13
+
\meta{video}{https://www.youtube.com/watch?v=0x5DYZcXJcc}
+19
trees/refs/keller-maocrkh-2013.tree
+19
trees/refs/keller-maocrkh-2013.tree
···
1
+
\title{File Systems Deserve Verification Too!}
2
+
\taxon{reference}
3
+
\meta{venue}{[[plos13]]}
4
+
\author{gckeller}
5
+
\author{tobym}
6
+
\author/literal{Sidney Amani}
7
+
\author{liamoc}
8
+
\author{zilinc}
9
+
\author/literal{Leonid Ryzhyk}
10
+
\author{gklein}
11
+
\author{heiser}
12
+
\date{2013-11-03}
13
+
\meta{doi}{10.1145/2525528.2525530}
14
+
\tag{cogent}
15
+
\tag{refereed}
16
+
17
+
\p{File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations --- we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time.}
18
+
19
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/Keller_MAOCRKH_13.abstract)}
+15
trees/refs/klein-akmmo-2017.tree
+15
trees/refs/klein-akmmo-2017.tree
···
1
+
\title{Provably Trustworthy Systems}
2
+
\taxon{reference}
3
+
\meta{venue}{[[philtransA]], Volume 375, Issue 2104}
4
+
\author{gklein}
5
+
\author/literal{June Andronick}
6
+
\author{gckeller}
7
+
\author/literal{Daniel Matichuk}
8
+
\author{tobym}
9
+
\author{liamoc}
10
+
\date{2017-09-04}
11
+
\meta{doi}{10.1098/rsta.2015.0404}
12
+
\tag{cogent}
13
+
\tag{invited}
14
+
\p{We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort; and code/proof co-generation, for scalable development of provably trustworthy applications.}
15
+
\p{This article is part of the themed issue ‘Verified trustworthy software systems’.}
+11
trees/refs/nagashima-oconnor-2016.tree
+11
trees/refs/nagashima-oconnor-2016.tree
···
1
+
\title{Close Encounters of the Higher Kind: Emulating Constructor Classes in Standard ML}
2
+
\taxon{reference}
3
+
\meta{venue}{[[ml16]]}
4
+
\author{yutakang}
5
+
\author{liamoc}
6
+
\date{2016-08-11}
7
+
\tag{workshop}
8
+
\meta{doi}{10.48550/arXiv.1608.03350}
9
+
\p{We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.}
10
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/Nagashima_OConnor_16.abstract)}
11
+
\meta{video}{https://www.youtube.com/watch?v=A2BJ6HRPRyg}
+8
trees/refs/oconnor-2022-plmw.tree
+8
trees/refs/oconnor-2022-plmw.tree
···
1
+
\title{Writing Valuable Papers}
2
+
\taxon{reference}
3
+
\meta{venue}{[POPL '22](popl22) Programming Languages Mentoring Workshop}
4
+
\author{liamoc}
5
+
\date{2022-01}
6
+
\meta{video}{https://www.youtube.com/watch?v=ycM6OOxGF_0}
7
+
\tag{talk}
8
+
\p{Most materials aimed at teaching people how to write, even within an academic context, focus largely on giving a rules-based framework for structure and prose style. These frameworks are based on outdated and inaccurate models of knowledge and are not suitable for academic writing. In this talk I will try to challenge some of the assumptions you have about writing papers, what (and who) writing papers is for, and how to think about writing as part of a research process.}
+8
trees/refs/oconnor-2024-compsoc.tree
+8
trees/refs/oconnor-2024-compsoc.tree
···
1
+
\title{Why Domain Theory Matters}
2
+
\taxon{reference}
3
+
\meta{venue}{[[uoe]] CompSoc Meeting}
4
+
\author{liamoc}
5
+
\date{2024-01}
6
+
\tag{talk}
7
+
\tag{semantics}
8
+
\p{In this talk I give whirlwind tour of denotational semantics, an oft-neglected but very important branch of theoretical computer science, which truly connects computer programs to mathematics}
+9
trees/refs/oconnor-2024-wg21.tree
+9
trees/refs/oconnor-2024-wg21.tree
···
1
+
\title{Putting the Past Behind Us (but not forgetting it)}
2
+
\taxon{reference}
3
+
\meta{venue}{[[wg21]] Meeting, Kloster Neustadt an der Weinstraße, Germany}
4
+
\author{liamoc}
5
+
\date{2024-04}
6
+
\tag{talk}
7
+
\tag{temporal-logic}
8
+
\tag{semantics}
9
+
\p{In this talk I demonstrated how the well known Zipper structure of Huet, later generalised by McBride, can be used to equip any modal logic with inverse modalities. In particular, this allows us to equip any temporal logic, including CTL, with a notion of linear past.}
+13
trees/refs/oconnor-amjad-2022.tree
+13
trees/refs/oconnor-amjad-2022.tree
···
1
+
\title{Holbert: Reading, Writing, Proving and Learning in the Browser}
2
+
\taxon{reference}
3
+
\meta{venue}{[[hatra22]]}
4
+
\author{liamoc}
5
+
\author{rayhana}
6
+
\date{2022-10-17}
7
+
\meta{doi}{10.48550/arXiv.2210.11411}
8
+
\tag{workshop}
9
+
\meta{external}{https://liamoc.net/hatra-2022/}
10
+
\p{
11
+
This paper presents Holbert: a work-in-progress pedagogical proof assistant and online textbook platform, aimed at the educational use-case, specifically for the teaching of programming language theory. Holbert allows proof exercises and rule definitions to be embedded directly in an online textbook, where proofs and rules can be manipulated using a graphical interface. We give an overview of the logical foundations of Holbert, examples of its use, and give an update as to its current implementation status.
12
+
}
13
+
\meta{video}{https://www.youtube.com/watch?v=Rdb7P5MJZLw}
+20
trees/refs/oconnor-cralmnsk-2016.tree
+20
trees/refs/oconnor-cralmnsk-2016.tree
···
1
+
\title{Refinement through Restraint: Bringing Down the Cost of Verification}
2
+
\taxon{reference}
3
+
\meta{venue}{[[icfp16]]}
4
+
\author{liamoc}
5
+
\author{zilinc}
6
+
\author{crizkallah}
7
+
\author/literal{Sidney Amani}
8
+
\author/literal{Japheth Lim}
9
+
\author{tobym}
10
+
\author{yutakang}
11
+
\author{tsewell}
12
+
\author{gklein}
13
+
\date{2016-09-04}
14
+
\meta{doi}{10.1145/2951913.2951940}
15
+
\tag{cogent}
16
+
\tag{refereed}
17
+
18
+
\p{We present a framework aimed at significantly reducing the cost of verifying certain classes of systems software, such as file systems. Our framework allows for equational reasoning about systems code written in our new language, Cogent. Cogent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. Linear types allow us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. As Cogent is a restricted language, it is designed to easily interoperate with existing C functions and to connect to existing C verification frameworks. Our framework is based on certifying compilation: For a well-typed Cogent program, our compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.}
19
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/OConnor_CRALMNSK_16.abstract)}
20
+
\meta{video}{https://www.youtube.com/watch?v=sJwcm_worfM}
+18
trees/refs/oconnor-crjakmsk-2021.tree
+18
trees/refs/oconnor-crjakmsk-2021.tree
···
1
+
\title{Cogent: Uniqueness Types and Certifying Compilation}
2
+
\taxon{reference}
3
+
\meta{venue}{[[jfp]], Volume 31, Issue on Secure Compilation}
4
+
\author{liamoc}
5
+
\author{zilinc}
6
+
\author{crizkallah}
7
+
\author{vjackson}
8
+
\author/literal{Sidney Amani}
9
+
\author{gklein}
10
+
\author{tobym}
11
+
\author{tsewell}
12
+
\author{gckeller}
13
+
\date{2021-10-27}
14
+
\meta{doi}{10.1017/S095679682100023X}
15
+
\tag{cogent}
16
+
\tag{refereed}
17
+
\p{This paper presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components. The framework is designed around a new functional programming language, Cogent. A central aspect of the language is its uniqueness type system, which eliminates the need for a trusted runtime or garbage collector while still guaranteeing memory safety, a crucial property for safety and security. Moreover, it allows us to assign two semantics to the language: The first semantics is imperative, suitable for efficient C code generation, and the second is purely functional, providing a user-friendly interface for equational reasoning and verification of higher-level correctness properties. The refinement theorem connecting the two semantics allows the compiler to produce a proof via translation validation certifying the correctness of the generated C code with respect to the semantics of the Cogent source program. We have demonstrated the effectiveness of our framework for implementation and for verification through two file system implementations.}
18
+
\p{This paper is largely based on [my](liamoc) [PhD Thesis](oconnor-thesis-2019).}
+17
trees/refs/oconnor-csrkk-2018.tree
+17
trees/refs/oconnor-csrkk-2018.tree
···
1
+
\title{Bringing Effortless Refinement of Data Layouts to Cogent}
2
+
\taxon{reference}
3
+
\meta{venue}{[[isola18]]}
4
+
\author{liamoc}
5
+
\author{zilinc}
6
+
\author/literal{Partha Susarla}
7
+
\author{crizkallah}
8
+
\author{gklein}
9
+
\author{gckeller}
10
+
\date{2018-10-29}
11
+
\meta{doi}{10.1007/978-3-030-03418-4_9}
12
+
\tag{cogent}
13
+
\tag{invited}
14
+
\p{The language Cogent allows low-level operating system components to be modelled as pure mathematical functions operating on algebraic data types, which makes it highly suitable for verification in an interactive theorem prover. Furthermore, the Cogent compiler translates these models into imperative C programs, and provides a proof that this compilation is a refinement of the functional model. There remains a gap, however, between the C data structures used in the operating system, and the algebraic data types used by Cogent. This forces the programmer to write a large amount of boilerplate marshalling code to connect the two, which can lead to a significant runtime performance overhead due to excessive copying.}
15
+
\p{In this paper, we outline our design for a data description language and data refinement framework, called Dargent, which provides the programmer with a means to specify how Cogent represents its algebraic data types. From this specification, the compiler can then generate the C code which manipulates the C data structures directly. Once fully realised, this extension will enable more code to be automatically verified by Cogent, smoother interoperability with C, and substantially improved performance of the generated code.}
16
+
17
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/csiroabstracts/OConnorDavis_CSRKK_18.abstract)}
+16
trees/refs/oconnor-kamkcr-2014.tree
+16
trees/refs/oconnor-kamkcr-2014.tree
···
1
+
\title{CDSL Version 1: Simplifying Verification with Linear Types}
2
+
\taxon{reference}
3
+
\meta{venue}{NICTA Technical Report}
4
+
5
+
\author{liamoc}
6
+
\author{gckeller}
7
+
\author/literal{Sidney Amani}
8
+
\author{tobym}
9
+
\author{gklein}
10
+
\author{zilinc}
11
+
\author{crizkallah}
12
+
\date{2014-10}
13
+
\tag{cogent}
14
+
15
+
\p{We introduce a purely functional domain specific language, CDSL, which aims to substantially reduce the cost of producing efficient, verified file system code. Given an executable specification of a file system, the CDSL compiler generates C code and, when fully implemented, will also generate an Isabelle/HOL proof linking the specification and the C implementation. We present two operational semantics for CDSL: (1) a value semantics, well suited for verification, and (2) an update semantics, which can be mapped to efficient C code. We outline the equivalence proof between these two semantics and discuss how the type system guarantees properties like termination, correct error handling, absence of memory leaks and aliasing.}
16
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/OConnorDavis_KAMKCR_14:tr.abstract)}
+9
trees/refs/oconnor-thesis-2019.tree
+9
trees/refs/oconnor-thesis-2019.tree
···
1
+
\title{Type Systems For Systems Types}
2
+
\taxon{reference}
3
+
\meta{venue}{PhD Thesis, [[unsw]]}
4
+
\author{liamoc}
5
+
\date{2019-10-23}
6
+
\meta{doi}{10.26190/unsworks/21495}
7
+
\tag{cogent}
8
+
\tag{thesis}
9
+
\p{This thesis presents a framework aimed at significantly reducing the cost of proving functional correctness for low-level operating systems components, designed around a new programming language, Cogent. This language is total, polymorphic, higher-order, and purely functional, including features such as algebraic data types and type inference. Crucially, Cogent is equipped with a uniqueness type system, which eliminates the need for a trusted runtime or garbage collector, and allows us to assign two semantics to the language: one imperative, suitable for efficient C code generation; and one functional, suitable for equational reasoning and verification. We prove that the functional semantics is a valid abstraction of the imperative semantics for all well-typed programs. Cogent is designed to easily interoperate with existing C code, to enable Cogent software to interact with existing C systems, and also to provide an escape hatch of sorts, for when the restrictions of Cogent's type system are too onerous. This interoperability extends to Cogent's verification framework, which composes with existing C verification frameworks to enable whole systems to be verified. Cogent's verification framework is based on certifying compilation: For a well-typed Cogent program, the compiler produces C code, a high-level representation of its semantics in Isabelle/HOL, and a proof that the C code correctly refines this embedding. Thus one can reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C. The compiler certificate is a series of language-level proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL. To evaluate the effectiveness of this framework, two realistic file systems were implemented as a case study, and key operations for one file system were formally verified on top of Cogent specifications. These studies demonstrate that verification effort is drastically reduced for proving higher-level properties of file system implementations, by reasoning about the generated formal specification from Cogent, rather than low-level C code.}
+13
trees/refs/oconnor-tyde-2016.tree
+13
trees/refs/oconnor-tyde-2016.tree
···
1
+
\title{Applications of Applicative Proof Search}
2
+
\taxon{reference}
3
+
\meta{venue}{[[tyde16]]}
4
+
\author{liamoc}
5
+
\date{2016-09-18}
6
+
\meta{doi}{10.1145/2976022.2976030}
7
+
\meta{download}{\route-asset{assets/applications.pdf}}
8
+
\tag{pbt}
9
+
\tag{temporal-logic}
10
+
\tag{refereed}
11
+
\p{In this paper, we develop a library of typed proof search procedures, and demonstrate their remarkable utility as a mechanism for proof-search and automation. We describe a framework for describing proof-search procedures in Agda, with a library of tactical combinators based on applicative functors. This framework is very general, so we demonstrate the approach with two common applications from the field of software verification: a library for property-based testing in the style of SmallCheck, and the embedding of a basic model checker inside our framework, which we use to verify the correctness of common concurrency algorithms.}
12
+
13
+
\meta{video}{https://www.youtube.com/watch?v=qiI3Avnp0XA}
+11
trees/refs/oconnor-tyde-2019.tree
+11
trees/refs/oconnor-tyde-2019.tree
···
1
+
\title{Deferring the Details and Deriving Programs}
2
+
\taxon{reference}
3
+
\meta{venue}{[[tyde19]]}
4
+
\author{liamoc}
5
+
\date{2019-08-18}
6
+
\meta{doi}{10.1145/3331554.3342605}
7
+
\meta{download}{\route-asset{assets/deferring.pdf}}
8
+
\tag{refereed}
9
+
\p{A commonly-used technique in dependently-typed programming is to encode invariants about a data structure into its type, thus ensuring that the data structure is correct by construction. Unfortunately, this often necessitates the embedding of explicit proof terms within the data structure, which are not part of the structure conceptually, but merely supplied to ensure that the data invariants are maintained. As the complexity of the specifications in the types increases, these additional terms tend to clutter definitions, reducing readability. We introduce a technique where these proof terms can be supplied later, by constructing the data structure within a proof delay applicative functor. We apply this technique to Trip, our new language for Hoare-logic verification of imperative programs embedded in Agda, where our applicative functor is used as the basis for a verification condition generator, turning the typed holes of Agda into a method for stepwise derivation of a program from its specification in the form of a Hoare triple.}
10
+
11
+
\meta{video}{https://www.youtube.com/watch?v=2euFCCeMZOM}
+10
trees/refs/oconnor-ug-thesis-2012.tree
+10
trees/refs/oconnor-ug-thesis-2012.tree
···
1
+
\title{Formalising GHC's Type System}
2
+
\taxon{reference}
3
+
\meta{venue}{Undergraduate Thesis, [[unsw]]}
4
+
\author{liamoc}
5
+
\date{2012-10}
6
+
\meta{download}{\route-asset{assets/reportb.pdf}}
7
+
\tag{thesis}
8
+
\p{GHC, a Haskell compiler, offers numerous extensions to the standard Haskell type system. Each of these extensions is usually specified only semi-formally, and only in isolation. Very little work has been done examining type system properties when multiple type system extensions are combined, which is the scenario actually being faced by GHC developers. To address this, the GHC team published OutsideIn(X), a mostly-rigorous formulation of GHC's type inference system, which encompasses every type system extension developed for GHC to date.}
9
+
\p{We formalise OutsideIn(X) in a mechanical proof assistant, in order to provide a body of formal work upon which future extensions can be developed. By using a mechanical proof assistant we not only ensure correctness of our proofs and complete rigor in our definitions, but also make possible the incremental development of the formal work alongside the more practically-minded type checker implementation in GHC. This additional accessibility will hopefully prevent further extensions from being developed without regard to the effect such an extension may have on other parts of the type system.}
10
+
\p{Our formalisation is developed in Agda. As a dependently typed programming language which enforces totality, Agda doubles as a proof assistant. It is still under heavy development, and is quite experimental. By formalising OutsideIn(X) in Agda, we demonstrate its readiness for type system work, and also provide an example to encourage further type systems research in Agda.}
+8
trees/refs/oconnor-ugproject-2012.tree
+8
trees/refs/oconnor-ugproject-2012.tree
···
1
+
\title{Gentzen: A Beginner's Proof Assistant based on Higher Order Logic}
2
+
\taxon{reference}
3
+
\meta{venue}{Undergraduate Project, [[unsw]]}
4
+
\author{liamoc}
5
+
\date{2012-12}
6
+
\meta{download}{\route-asset{assets/gentzen.pdf}}
7
+
\tag{thesis}
8
+
\p{Existing proof assistants such as Isabelle or Coq are geared towards large-scale, complicated verification projects, and are not ideal educational tools for topics of a fairly formal nature, such as the theoretical foundations of programming languages. In particular, they opt for a proof language that resembles a programming language, rather than the structure typically seen in pen-and-paper proofs. Gentzen is a simple theorem prover we are developing in Haskell, which will be tightly integrated with its user interface, using a structural editor for graphically presented proofs. This allows proof scripts to resemble pen-and-paper proofs, and assists students to focus on the proof, rather than the proof assistant. This report outlines the current state of Gentzen development, and gives a formal treatment of its proof checker semantics.}
+8
trees/refs/oconnor-vanglabbeek-2023-compsoc.tree
+8
trees/refs/oconnor-vanglabbeek-2023-compsoc.tree
···
1
+
\title{Mutual Exclusion: Harder than you Think!}
2
+
\taxon{reference}
3
+
\meta{venue}{[[uoe]] CompSoc Meeting}
4
+
\author{liamoc}
5
+
\author{rvg}
6
+
\date{2023-01}
7
+
\tag{talk}
8
+
\p{It’s well known that some problems in computer science are unsolvable — finding a recipe to tell whether an arbitrary computer program halts is a classic example. But in the world of concurrency, the most classical problem, mutual exclusion, is widely considered to be solved. In this talk we will examine the assumptions that have led concurrency theorists to this conclusion, and show that, unless either an assumption about hardware or a requirement of the problem are relaxed, this most famous problem of concurrency theory has, in fact, no satisfactory solution.}
+13
trees/refs/oconnor-wickstrom-2022.tree
+13
trees/refs/oconnor-wickstrom-2022.tree
···
1
+
\title{Quickstrom: Property-based Acceptance Testing with LTL Specifications}
2
+
\taxon{reference}
3
+
\meta{venue}{[[pldi22]]}
4
+
\author{liamoc}
5
+
\author{owickstrom}
6
+
\date{2022-06-09}
7
+
\meta{doi}{10.1145/3519939.3523728}
8
+
\meta{doi}{10.48550/arXiv.2203.11532}
9
+
\tag{temporal-logic}
10
+
\tag{pbt}
11
+
\tag{refereed}
12
+
\p{We present Quickstrom, a property-based testing system for acceptance testing of interactive applications. Using Quickstrom, programmers can specify the behaviour of web applications as properties in our testing-oriented dialect of Linear Temporal Logic (LTL) called QuickLTL, and then automatically test their application against the given specification with hundreds of automatically generated interactions. QuickLTL extends existing finite variants of LTL for the testing use-case, determining likely outcomes from partial traces whose minimum length is itself determined by the LTL formula. This temporal logic is embedded in our specification language, Specstrom, which is designed to be approachable to web programmers, expressive for writing specifications, and easy to analyse. Because Quickstrom tests only user-facing behaviour, it is agnostic to the implementation language of the system under test. We therefore formally specify and test many implementations of the popular TodoMVC benchmark, used for evaluation and comparison across various web frontend frameworks and languages. Our tests uncovered bugs in almost half of the available implementations.}
13
+
\meta{video}{https://www.youtube.com/watch?v=6t8emhea0pA}
+9
trees/refs/qin-oconnor-steuwer-2023.tree
+9
trees/refs/qin-oconnor-steuwer-2023.tree
···
1
+
\title{Primrose: Selecting Container Data Types by Their Properties}
2
+
\taxon{reference}
3
+
\meta{venue}{[[programming-journal]], Volume 7, Issue 3, Article 11}
4
+
\author/literal{Xueying Qin}
5
+
\author{liamoc}
6
+
\author{msteuwer}
7
+
\date{2023-02-15}
8
+
\tag{refereed}
9
+
\meta{doi}{10.22152/programming-journal.org/2023/7/11}
+16
trees/refs/qin-ovghks-2024.tree
+16
trees/refs/qin-ovghks-2024.tree
···
1
+
\title{Shoggoth: A Formal Foundation for Strategic Rewriting}
2
+
\taxon{reference}
3
+
\meta{venue}{[[popl24]]}
4
+
\author/literal{Xueying Qin}
5
+
\author{liamoc}
6
+
\author{rvg}
7
+
\author{hoefner}
8
+
\author{ohad}
9
+
\author{msteuwer}
10
+
\date{2024-01-05}
11
+
\tag{refereed}
12
+
\tag{semantics}
13
+
\meta{doi}{10.1145/3633211}
14
+
\p{Rewriting is a versatile and powerful technique used in many domains. Strategic rewriting allows programmers to control the application of rewrite rules by composing individual rewrite rules into complex rewrite strategies. These strategies are semantically complex, as they may be nondeterministic, they may raise errors that trigger backtracking, and they may not terminate.}
15
+
\p{Given such semantic complexity, it is necessary to establish a formal understanding of rewrite strategies and to enable reasoning about them in order to answer questions like: How do we know that a rewrite strategy terminates? How do we know that a rewrite strategy does not fail because we compose two incompatible rewrites? How do we know that a desired property holds after applying a rewrite strategy?}
16
+
\p{In this paper, we introduce Shoggoth: a formal foundation for understanding, analysing and reasoning about strategic rewriting that is capable of answering these questions. We provide a denotational semantics of System S, a core language for strategic rewriting, and prove its equivalence to our big-step operational semantics, which extends existing work by explicitly accounting for divergence. We further define a location-based weakest precondition calculus to enable formal reasoning about rewriting strategies, and we prove this calculus sound with respect to the denotational semantics. We show how this calculus can be used in practice to reason about properties of rewriting strategies, including termination, that they are well-composed, and that desired postconditions hold. The semantics and calculus are formalised in Isabelle/HOL and all proofs are mechanised.}
+19
trees/refs/rizkallah-lnscomkk-2016.tree
+19
trees/refs/rizkallah-lnscomkk-2016.tree
···
1
+
\title{A Framework for the Automatic Formal Verification of Refinement from Cogent to C}
2
+
\taxon{reference}
3
+
\meta{venue}{[[itp16]]}
4
+
\author{crizkallah}
5
+
\author/literal{Japheth Lim}
6
+
\author{yutakang}
7
+
\author{tsewell}
8
+
\author{zilinc}
9
+
\author{liamoc}
10
+
\author{tobym}
11
+
\author{gckeller}
12
+
\author{gklein}
13
+
\tag{refereed}
14
+
\date{2016-08-07}
15
+
\meta{doi}{10.1007/978-3-319-43144-4_20}
16
+
\tag{cogent}
17
+
\p{Our language Cogent simplifies verification of systems software using a certifying compiler, which produces a proof that the generated C code is a refinement of the original Cogent program. Despite the fact that Cogent itself contains a number of refinement layers, the semantic gap between even the lowest level of Cogent semantics and the generated C code remains large. In this paper we close this gap with an automated refinement framework which validates the compiler’s code generation phase. This framework makes use of existing C verification tools and introduces a new technique to relate the type systems of Cogent and C. }
18
+
19
+
\meta{source}{[Available from TS](https://trustworthy.systems/publications/nictaabstracts/Rizkallah_LNSCOMKK_16.abstract)}
+21
trees/table-macros.tree
+21
trees/table-macros.tree
···
1
+
2
+
\xmlns:html{http://www.w3.org/1999/xhtml}
3
+
\def\table[body]{
4
+
\<html:table>{\body}
5
+
}
6
+
\def\small[body]{
7
+
\<html:small>{\body}
8
+
}
9
+
\def\br{\<html:br>}
10
+
\def\tr[body]{
11
+
\<html:tr>{\body}
12
+
}
13
+
\def\td[body]{
14
+
\<html:td>{\body}
15
+
}
16
+
\def\th[body]{
17
+
\<html:th>{\body}
18
+
}
19
+
\def\hr{
20
+
\<html:hr>{}
21
+
}