February 2020

Håkon Robbestad Gylterud

2020–02–02, Sunday

Palindrome day – 20200202 – today. If you were born today, and lived for 101 years (another palindrome number) and a few months, you would live to see yet another palindrome day 2121–12–12.

2020-02-06, Thursday

My second son has chosen this morning to be born. Conscious and curious from the first second.

2020–02–12, Wednesday

First real snowfall this year. My Australian leather works surprisingly well in the snow: It keeps the flakes out of my face, even in wind. And when I get home the snow brushes off easily.

My Australian leather hat.

2020–02–16, Sunday

Reading “Permanent record”, which is Edward Snowden’s autobiography (but appearently written with the help of Joshua Cohen). Only about eighty pages into it, but the nostalgia for early Internet really hits a string in me. He describes his childhood and adolesence on Internet at a time when everyone there was an enthusiast, and websites were made by people – not algorithms.

I have spent quite some time on The Way Back Machine visiting websites as the appeared in the late 90s and early 00s. My most recent trip went to my Alma Mater’s website in 1997. The University of Oslo had quite a lot of information online at that point, and the website feels very sincere and open. My favourite find was in the recollection of activities of the university museums in 1993, where they describe the dinosaur exhibition I went to that year. As a four year old, with dinosaurs as my big fascination, this left a huge impression on me. Thus, it is nice to see that this was in fact a big event for rest of the city as well.

«På Paleontologisk museum ble det nyoppbygde skjelettet av Iguanodon-øglen ferdig i februar.» (UiO 1993)

2020–02–25, Tuesday

Gradually coming back to work routines. Last week my office was unaccessible due to maintainance on the network cables, and much of the time yesterday was spent tidying my office. Today I could sit down and get some actual work down. First, I finished a review for the post proceedings of TYPES 2019. Then Stefano and I had an interesting discussion on coherence for symmetric monoidal groupoids.

2020–02–28, Friday

Working on a simply typed λ-calculus with a quoting operation. I am developing it in Agda, where I have leared a lot about how to formalise formal languages over the years. One of my inspirations is Russel O’Connor’s formalisation of the base theory.

Expecting a comment section? Feel free to e-mail me your comments, or otherwise contact me to discuss the content of this site. See my contact info. You can also write your opinion on your own website, and link back here! ☺