Hi, my name is Jakob.
I am a software engineer from Aarhus, Denmark working remotely at Microsoft on the .NET JIT compiler.
You can find me day-to-day on GitHub.
Before my switch to Microsoft I was a PhD student in the Logic and Semantics group at Aarhus University
where I applied formal methods in the area of smart contracts using the Coq proof assistant.
I am still interested and sometimes active in projects like ConCert and MetaCoq.
Work experience
Senior Software Engineer
Microsoft
Apr 2021 — Present
I work on the open-source .NET JIT compiler.
You can see me work in the dotnet/runtime repository on GitHub.
Software Engineer Intern
Microsoft
Jul 2019 — Sep 2019
I was an intern on the .NET core JIT compiler team in Redmond where I worked on enabling tail call optimization in a wider range of scenarios than previously.
Senior Developer
Bossland GmbH
Sep 2009 — Aug 2018
I was involved in writing automation software for various computer games such as World of Warcraft.
Publications
Correct and Complete Type Checking and Certified Erasure for Coq, in Coq
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter. JACM 2025.
[GitHub]
Extracting funcitonal programs from Coq, in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. JFP 2022.
[arXiv] [GitHub]
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. CPP'2021.
[arXiv] [GitHub]
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters. CPP'2020.
[PDF] [GitHub]
Smart Contract Interactions in Coq
Jakob Botsch Nielsen, Bas Spitters. In pre-proceedings, FMBC19.
[PDF] [SRC]
