Jakob Botsch Nielsen
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]
Conferences and workshops
- POPL 2020, New Orleans, USA, January 19-25, 2020.
- Formal Methods for Blockchains, Porto, Portugal, October 11, 2019.
- Theory and Practice of Blockchains 2019, Aarhus, Denmark, May 27-29, 2019.
More
GitHub
Click here