Photo by Geir Skjalmar on Unsplash
Hi great to meet you, I'm William Sørensen! I am a computer scientist specializing in programming language theory, compilers and systems programming. I intend to start a blog where I write tools and posts about my course!
As a bit of background, I stem from Harstad, a beautiful city of the north. I later moved to Cambridge for uni where I still reside.
In my freetime I enjoy long distance biking, rowing, and playing the timps (though not as often as I'd like to).
I am trying to write a silly little blog.
To begin I explore the great lengths I have to go to for animation on the web!
Canvas commons for web animation
Over the years I have worked on a few different projects.
Most of these are just silly proof of concepts,
but some of them also larger, more developed projects.
'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M100%20170L70%20170L70%20140L100%20140L100%20170ZM80%20160L90%20160L90%20150L80%20150L80%20160Z'%20fill='black'/%3e%3crect%20x='70'%20y='160'%20width='10'%20height='10'%20transform='rotate(-180%2070%20160)'%20fill='black'/%3e%3crect%20x='50'%20y='70'%20width='10'%20height='50'%20fill='black'/%3e%3crect%20x='40'%20y='110'%20width='10'%20height='10'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M100%2090L70%2090L70%2060L100%2060L100%2090ZM80%2080L90%2080L90%2070L80%2070L80%2080Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M100%2090L70%2090L70%2060L100%2060L100%2090ZM80%2080L90%2080L90%2070L80%2070L80%2080Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M140%20130L110%20130L110%20100L140%20100L140%20130ZM120%20120L130%20120L130%20110L120%20110L120%20120Z'%20fill='black'/%3e%3crect%20x='70'%20y='80'%20width='10'%20height='10'%20transform='rotate(-180%2070%2080)'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M100%20170L70%20170L70%20140L100%20140L100%20170ZM80%20160L90%20160L90%20150L80%20150L80%20160Z'%20fill='black'/%3e%3crect%20x='70'%20y='160'%20width='10'%20height='10'%20transform='rotate(-180%2070%20160)'%20fill='black'/%3e%3crect%20x='110'%20y='160'%20width='10'%20height='10'%20transform='rotate(-180%20110%20160)'%20fill='black'/%3e%3crect%20x='130'%20y='160'%20width='10'%20height='10'%20transform='rotate(-180%20130%20160)'%20fill='black'/%3e%3crect%20x='150'%20y='160'%20width='10'%20height='10'%20transform='rotate(-180%20150%20160)'%20fill='black'/%3e%3crect%20x='110'%20y='80'%20width='10'%20height='10'%20transform='rotate(-180%20110%2080)'%20fill='black'/%3e%3crect%20x='130'%20y='80'%20width='10'%20height='10'%20transform='rotate(-180%20130%2080)'%20fill='black'/%3e%3crect%20x='150'%20y='80'%20width='10'%20height='10'%20transform='rotate(-180%20150%2080)'%20fill='black'/%3e%3crect%20x='150'%20y='120'%20width='10'%20height='10'%20transform='rotate(-180%20150%20120)'%20fill='black'/%3e%3crect%20x='110'%20y='120'%20width='20'%20height='10'%20transform='rotate(-180%20110%20120)'%20fill='black'/%3e%3crect%20x='170'%20y='120'%20width='10'%20height='10'%20transform='rotate(-180%20170%20120)'%20fill='black'/%3e%3crect%20x='190'%20y='120'%20width='10'%20height='10'%20transform='rotate(-180%20190%20120)'%20fill='black'/%3e%3crect%20x='180'%20y='50'%20width='10'%20height='10'%20transform='rotate(-180%20180%2050)'%20fill='black'/%3e%3crect%20x='180'%20y='30'%20width='10'%20height='10'%20transform='rotate(-180%20180%2030)'%20fill='black'/%3e%3crect%20x='50'%20y='70'%20width='10'%20height='90'%20fill='black'/%3e%3crect%20x='10'%20y='20'%20width='10'%20height='30'%20fill='black'/%3e%3crect%20x='80'%20y='90'%20width='10'%20height='30'%20fill='black'/%3e%3crect%20x='20'%20y='30'%20width='170'%20height='10'%20fill='black'/%3e%3c/svg%3e)
Fast and easy-to-use coinductive datatypes for Lean4
Coinductive datatypes are structures I have taken a great deal of interest in in the past years.
I wrote my dissertation on how to make them performant,
and I had an internship under Alex Keizer working on them!
'%20fill='black'/%3e%3crect%20width='10'%20height='160'%20transform='matrix(-1%200%200%201%2020%2020)'%20fill='black'/%3e%3crect%20x='110'%20y='10'%20width='10'%20height='10'%20fill='black'/%3e%3crect%20x='110'%20y='30'%20width='10'%20height='10'%20fill='black'/%3e%3crect%20x='70'%20y='10'%20width='10'%20height='10'%20fill='black'/%3e%3crect%20x='70'%20y='30'%20width='10'%20height='10'%20fill='black'/%3e%3c/svg%3e)
Termination checking
During first year of Cambridge, I became quite interested in termination checking of ML like programs.
I then implemented a super simple term checker in OCaml.
'%20fill='black'/%3e%3crect%20x='70'%20y='70'%20width='10'%20height='10'%20transform='rotate(90%2070%2070)'%20fill='black'/%3e%3crect%20x='60'%20y='80'%20width='10'%20height='10'%20transform='rotate(90%2060%2080)'%20fill='black'/%3e%3crect%20x='190'%20y='110'%20width='10'%20height='10'%20transform='rotate(-180%20190%20110)'%20fill='black'/%3e%3crect%20x='180'%20y='90'%20width='10'%20height='10'%20transform='rotate(-180%20180%2090)'%20fill='black'/%3e%3crect%20x='170'%20y='80'%20width='10'%20height='10'%20transform='rotate(-180%20170%2080)'%20fill='black'/%3e%3crect%20x='160'%20y='70'%20width='10'%20height='10'%20transform='rotate(-180%20160%2070)'%20fill='black'/%3e%3crect%20x='150'%20y='140'%20width='10'%20height='10'%20transform='rotate(-90%20150%20140)'%20fill='black'/%3e%3crect%20x='160'%20y='130'%20width='10'%20height='10'%20transform='rotate(-90%20160%20130)'%20fill='black'/%3e%3crect%20x='170'%20y='120'%20width='10'%20height='10'%20transform='rotate(-90%20170%20120)'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M70%2050L40%2050L40%2020L70%2020L70%2050ZM50%2040L60%2040L60%2030L50%2030L50%2040Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M130%2090L100%2090L100%2060L130%2060L130%2090ZM110%2080L120%2080L120%2070L110%2070L110%2080Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M130%20140L100%20140L100%20110L130%20110L130%20140ZM110%20130L120%20130L120%20120L110%20120L110%20130Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M130%20180L100%20180L100%20150L130%20150L130%20180ZM110%20170L120%20170L120%20160L110%20160L110%20170Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M70%20180L40%20180L40%20150L70%20150L70%20180ZM50%20170L60%20170L60%20160L50%20160L50%20170Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M190%20180L160%20180L160%20150L190%20150L190%20180ZM170%20170L180%20170L180%20160L170%20160L170%20170Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M130%2050L100%2050L100%2020L130%2020L130%2050ZM110%2040L120%2040L120%2030L110%2030L110%2040Z'%20fill='black'/%3e%3cpath%20fill-rule='evenodd'%20clip-rule='evenodd'%20d='M190%2050L160%2050L160%2020L190%2020L190%2050ZM170%2040L180%2040L180%2030L170%2030L170%2040Z'%20fill='black'/%3e%3crect%20x='110'%20y='50'%20width='10'%20height='10'%20fill='black'/%3e%3crect%20x='110'%20y='140'%20width='10'%20height='10'%20fill='black'/%3e%3crect%20x='110'%20y='90'%20width='10'%20height='20'%20fill='black'/%3e%3crect%20x='100'%20y='160'%20width='10'%20height='30'%20transform='rotate(90%20100%20160)'%20fill='black'/%3e%3crect%20x='160'%20y='160'%20width='10'%20height='30'%20transform='rotate(90%20160%20160)'%20fill='black'/%3e%3crect%20x='160'%20y='30'%20width='10'%20height='30'%20transform='rotate(90%20160%2030)'%20fill='black'/%3e%3crect%20x='100'%20y='30'%20width='10'%20height='30'%20transform='rotate(90%20100%2030)'%20fill='black'/%3e%3c/svg%3e)
Type driven parsing
A quick project done before uni was a LL(k) parser implemented as Rust generics.
Source code for this site on Github