my forest
add a pic
+5
-1
assets/cloudy.jpeg
assets/cloudy.jpeg
This is a binary file and will not be displayed.
+5
-1
trees/weeknotes/2025-W50.tree
+5
-1
trees/weeknotes/2025-W50.tree
···
2
2
\title{Weeknotes 2025-W50}
3
3
\author{liamoc}
4
4
\date{2025-12-14}
5
-
\p{This week felt quite productive. The [Logic Summer School](loc-001W) has now finished, and my PhD student at [[uoe]], [[rayhana]], has now embarked back to the UK. My course ([[isa-001]]) was only for the first week, so I had some time to get work done this week. [[hoefner]] and I finally finished a mammoth proof in Isabelle that matrices over a Kleene algebra are themselves a Kleene algebra, a proof that's important for [[dexterkozen]]'s completeness result for Kleene algebras. This required some novel proof engineering, and some constructions to make the proof go though that we think [Dexter](dexterkozen) may have missed in his pen-and-paper proof. I may write up my thoughts this coming week, but it's also possible that you might have to wait for a paper. [[rayhana]] and I also sketched out some future directions for our work, which is quite exciting. }
5
+
\p{This week felt quite productive. The [Logic Summer School](loc-001W) has now finished, and my PhD student at [[uoe]], [[rayhana]], has now embarked back to the UK. My course ([[isa-001]]) was only for the first week, so I had some time to get work done this week. [[hoefner]] and I finally finished a mammoth proof in Isabelle that matrices over a Kleene algebra are themselves a Kleene algebra, a proof that's important for [[dexterkozen]]'s completeness result for Kleene algebras. This required some novel proof engineering, and some constructions to make the proof go though that we think [Dexter](dexterkozen) may have missed in his pen-and-paper proof. I may write up my thoughts this coming week, but it's also possible that you might have to wait for a paper. [[rayhana]] and I also sketched out some future directions for our work, which is quite exciting.}
6
+
\figure{
7
+
\<html:img>[width]{350px}[src]{\route-asset{assets/cloudy.jpeg}}%{}
8
+
\figcaption{A picturesque cloudy Canberra evening.}
9
+
}
6
10
\transclude{loc-002N}
7
11
\transclude{loc-002O}
8
12
\transclude{loc-002P}