rootmos' what-nots

Some math, mostly programming and everything in between

Soundsjamdemoallbor19

2020 Q1	Wed, 08 Apr 2020
Unscalable walls	Wed, 15 Jan 2020
Negative space	Thu, 10 Oct 2019
Introduction to what comes after	Tue, 17 Sep 2019
M44	Sat, 24 Aug 2019

Twitch highlights

Sat, 18 Jul 2020	Session @ 2020-07-18: March to the devil
Sat, 30 May 2020	The Vermona Clap, ladies and gents
Sat, 30 May 2020	Session @ 2020-05-29 (2/2)
Sat, 30 May 2020	Session @ 2020-05-29 (1/2)
Tue, 19 May 2020	Session @ 2020-05-19: Dune sample

Activity

Thu, 29 Oct 2020	iotaledger/stronghold.rs	Add convenience lemma about post padding when pages are aligned
Tue, 27 Oct 2020	iotaledger/stronghold.rs	Extend the aligned_add_le lemma
Tue, 27 Oct 2020	iotaledger/stronghold.rs	Prove an estimate about an aligned addition of pointers
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Rewrite qi into an analyzable form
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Prove that the `data - pad_pre` calculation isn't truncating
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Move the memory allocation layout into its own type
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Sketch a pad and alignment formalization in Coq
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Prove that padding is invariant under addition of aligned pointers
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Formalize mmap
Mon, 26 Oct 2020	iotaledger/stronghold.rs	Implement a naive allocator

Projects

wwwo » A continuation-style static website generator in OCaml
midi » Music and MIDI processing tools
spl » Deterministically configure, build and install custom Linux distributions from scratch
twitch-cli » Twitch command line interface
config » Personal configuration files: vimrc and what-not.
stream » Streaming utilities
fb » rootmos generates buffers with frames
audio-journal » Android app and Linux scripts to keep a diary of sounds
displayswitcheroo » Configure your monitors based on a list of preferred profiles
tabs-vs-spaces » Configure Vim according to heuristics based on the current buffer
agda-hack » A place to collect things I learn about Agda
- bf » A BrainFuck interpreter
dvorak » My customized Dvorak layout: a mixture of Dvorak, Svorak and programmers Dvorak, combining the best of all worlds.
apl-hack » A place to collect things I learn about APL
- aoc19 » My solutions to Advent of Code 2019
- aoc18 » My solutions to Advent of Code 2018
- aoc17 » My solutions to Advent of Code 2017
arweaver » An Arweave client written in Rust
loom » Run a local development Arweave blockchain with faucets and on-demand mining
git-audit » Manages an audit trail for a Git repository by considering it as an Ethereum side-chain
coq-hack » A place to collect things I learn about Coq.
- wf » Equivalence between two definitions of a well-founded relation (Coq's and Wikipedia's) using classical logic
- STLC » Formalization of the simply typed lambda calculus
silly-actor » Small actor model implementation that compiles to C using nanopass-framework
dont-fear-the-reaper » A Linux subreaper that terminates orphans
libpquv » A small library combining libpq and libuv
lambdasylum » A place to study some lambda calculi
silly-joy » Interpreter for Joy in Haskell using extensible-effects
silly-ml » A small ML-like, type-checked, interpreted or x86-64 compiled, language created because it's weekend
silly-k » silly-k is an experimental hobby language inspired by K and APL
ppx_useless » A useless ppx extension
silly-church » A small example of a nanopass style compiler
ppx_ski » SKI combinator calculus implemented in OCaml
ldapy » Command line tool to explore LDAP databases

Posts

Services

ip.rootmos.io

Academic work

2014 » Carleman-Sobolev classes and Green’s potentials for weighted Laplacians
- Licentiate thesis (DiVA)
- Paper 1: Carleman-Sobolev classes for small exponents (arXiv, coauthored with Aron Wennman)
- Paper 2: Solving Poisson's equation for the standard weighted Laplacian in the unit disc (arXiv)
2012 » Green’s function for two weighted Laplacians in the unit disc
- Master's thesis (PDF)
2010 » On p-groups of low power order, Representations of p-groups
- Bachelor's thesis (PDF)
- joint work with Gustav Sædén Ståhl and Johan Laine

Resume

PDF (updated 30 Nov 2018)