my forest
more weeknotes and comp1110 news
+157
-5
+5
trees/courses/COMP1110.tree
+5
trees/courses/COMP1110.tree
+6
-4
trees/loc-0007.tree
+6
-4
trees/loc-0007.tree
···
3
3
\parent{loc-0004}
4
4
\p{The following teaching engagements were/are all at the [[anu]]:}
5
5
\table{
6
-
\tr{\td{2025}\td{ [[COMP1100]]. Lecturer.}}
6
+
\tr{\td{2026}\td{ [[COMP1110]]. Lecturer Convenor.}}
7
+
\tr{\td{2025}\td{ [[COMP1100]]. Lecturer Convenor.}}
7
8
}
8
9
\p{The following teaching engagements were all at the [[uoe]]:}
9
10
\table{
···
25
26
\tr{\td{}\td{ [[COMP3141]] (308 students). Lecturer Convenor. }}
26
27
\tr{\td{}\td{ [[COMP3153]] (18 students). Lecturer Convenor. }}
27
28
\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.}}}
29
+
\tr{\td{2019}\td{ [[COMP3161]] (111 students).}}\tr{\td{}\td{ \small{#{100\%} teacher satisfaction. #{95.1\%} course satisfaction.} }}
30
+
\tr{\td{}\td{ [[COMP3141]] (196 students). Lecturer Convenor.}}\tr{\td{}\td{ \small{ #{97.3\%} teacher satisfaction. #{93.9\%} course satisfaction.}}}
31
+
\tr{\td{2018}\td{ [[COMP3161]] (96 students). Lecturer Convenor, Tutor.}}
32
+
\tr{\td{}\td{ \small{#{98.1\%} teacher satisfaction. #{100\%} course satisfaction.}}}
31
33
\tr{\td{}\td{ [[COMP2111]]. Tutor (6 tutorials), Relief Lecturer.}}
32
34
\tr{\td{}\td{ \small{#{94.1\%} teacher satisfaction.}}}
33
35
\tr{\td{}\td{ [[COMP3141]]. Course Designer and Administrator.}}
+16
trees/loc-001W.tree
+16
trees/loc-001W.tree
···
1
+
\date{2025-09-19}
2
+
\author{liamoc}
3
+
\title{ANU Logic Summer School 2025}
4
+
\meta{external}{https://comp.anu.edu.au/lss/}
5
+
\meta{venue}{[[anu]]}
6
+
\p{
7
+
The [ANU](anu) Logic Summer School is back again this year, and this time I feature on [the program](https://comp.anu.edu.au/lss/lectures/2025/). I will be teaching an Introduction to Interactive Theorem Proving using [Isabelle/HOL](https://isabelle.in.tum.de). The timetable is tentative but it looks like I will be teaching it over the final two days of the first week, with one two-hour and one one-hour lecture per day. This means it will be quite a packed programme, but I will do my best.
8
+
}
9
+
\p{It's my hope that I can figure out a nice way to include Isabelle code in Forester trees, so that I can make my lecture notes with Forester. But this may be difficult for a variety of technical reasons, so in the worst case it will be a bunch of Isabelle theory files with comments. }
10
+
\p{
11
+
My introduction will hopefully tie in to [[cledmonds]]' teaching Hoare logic and rely/guarantee reasoning in Isabelle over the second week.
12
+
}
13
+
\p{
14
+
If you or your students have an interest in logic or verification, please consider sending your students! We also have some limited scholarships available.
15
+
}
16
+
+7
trees/loc-001X.tree
+7
trees/loc-001X.tree
···
1
+
\date{2025-09-19}
2
+
\author{liamoc}
3
+
\title{Against "eureka steps"}
4
+
\p{Both [[hoefner]] and I enjoyed [[tomschrijvers]]' talk at the [[loc-001U]] answering a challenge from [[brunooliveira]]: to stepwise \em{derive} his [QuickSub](zhou-oliveira-2025) efficient iso-recursive subtype checking algorithm from the exponential-time Amber rules of [[lucacardelli]]'s #{\mathcal{F}_{<}}. Impressively, [Tom](tomschrijvers) and his student were able to get there, and it's certainly nice to have such a neat justification of QuickSub's correctness, but I did experience some mild irritation: The calculation was done \em{with a very specific goal in mind} — namely the QuickSub algorithm — and so several steps in the proof were, in a sense, "goal-motivated". If we didn't know the QuickSub algorithm in advance, many steps would have had no intuition behind them at all. Another member of the group called such steps "eureka steps".}
5
+
\p{It led me to wonder about the myriad of possible choices available at any given step in that refinement. Why do we choose \em{this} algorithm? If I recall some of the classic works on program calculation from [[richardbird]] or [[ccm]], the algorithms we end up with proceed from a series of calculations, each of which makes sense in isolation. You can read the derivation from beginning to end and each step feels like it's improving the algorithm in some way. The process feels entirely natural. Whereas here, these "eureka steps" mean that I need to look much further ahead to find the motivation for the transformation being performed. }
6
+
\p{I encountered a similar feeling when my student [[xinloi]] raised [[raad-bdo-2022]] for discussion with me and [[hoefner]]. [[ohearn-2020]] is, in a nutshell, a logic for showing the presence of bugs rather than their absence. One of its nice qualities is that, like its almost-dual Hoare logic, it offers a relatively \em{calculational} way to approach program (in)correctness, where each proof step follows naturally from the structure of the program and the assertions within it. Unfortunately, [[raad-bdo-2022]] doesn't quite preserve this property when moving to a concurrent setting. To prove the existence of concurrency bugs like races, each thread's local assertions build a history of writes and lock actions, and then, in the assertion after the potential race, a "eureka step" comes in which points out the problematic interleaving of these histories that exhibits the race condition. Proving the presence of this bug required first knowing that the bug exists and how it can arise, and then doing the same "goal-motivated" reasoning that we saw in [Tom](tomschrijvers)'s talk. This seems to me quite dissatisfying. Is there a more genuinely calculational approach here? I suspect concurrency makes things fundamentally more difficult, but I think we should nonetheless strive for the elimination of these "eureka steps" even if it's not always possible to do so. }
7
+
+4
trees/news.tree
+4
trees/news.tree
+6
trees/people/azalea.tree
+6
trees/people/azalea.tree
+6
trees/people/brunooliveira.tree
+6
trees/people/brunooliveira.tree
+6
trees/people/cledmonds.tree
+6
trees/people/cledmonds.tree
+6
trees/people/dreyer.tree
+6
trees/people/dreyer.tree
+6
trees/people/joshberdine.tree
+6
trees/people/joshberdine.tree
+6
trees/people/litaozhou.tree
+6
trees/people/litaozhou.tree
+6
trees/people/lucacardelli.tree
+6
trees/people/lucacardelli.tree
+6
trees/people/ohearn.tree
+6
trees/people/ohearn.tree
+6
trees/people/richardbird.tree
+6
trees/people/richardbird.tree
+6
trees/people/tomschrijvers.tree
+6
trees/people/tomschrijvers.tree
+4
trees/places/hku.tree
+4
trees/places/hku.tree
+4
trees/places/kuleuven.tree
+4
trees/places/kuleuven.tree
+3
trees/places/mpi-sws.tree
+3
trees/places/mpi-sws.tree
+8
trees/places/popl20.tree
+8
trees/places/popl20.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL '20}{47th ACM SIGPLAN Symposium on Principles of Programming Languages}}
3
+
\taxon{Conference}
4
+
\date{2020-01}
5
+
\meta{venue}{New Orleans, Louisiana, USA}
6
+
\meta{external}{https://popl20.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/popl25.tree
+8
trees/places/popl25.tree
···
1
+
\import{conf-name-macros}
2
+
\title{\conf-name{POPL ’25}{52nd ACM SIGPLAN Symposium on Principles of Programming Languages}}
3
+
\taxon{Conference}
4
+
\date{2025-01}
5
+
\meta{venue}{Denver, Colorado, USA}
6
+
\meta{external}{https://popl25.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.}
+4
trees/places/ucl.tree
+4
trees/places/ucl.tree
+4
trees/places/uwa.tree
+4
trees/places/uwa.tree
+6
trees/refs/ohearn-2020.tree
+6
trees/refs/ohearn-2020.tree
+9
trees/refs/raad-bdo-2022.tree
+9
trees/refs/raad-bdo-2022.tree
+6
trees/refs/zhou-oliveira-2025.tree
+6
trees/refs/zhou-oliveira-2025.tree
+3
-1
trees/weeknotes/2025-W38.tree
+3
-1
trees/weeknotes/2025-W38.tree