Unless you're trying to find some old stuff, please see my new website.
This website is no longer updated as I am no longer at DTU.
I was a PhD student at DTU Compute from July 2021 to June 2024, working on UserFriendly Formal Methods, especially for distributed systems and using Isabelle/HOL.
My supervisor was Jørgen Villadsen, and my cosupervisor is Alceste Scalas.
I am interested in formal methods for safety critical embedded systems and distributed systems. I am also interested in formal methods in the context of teaching.
Check out my GitHub page to see what I'm working on.Please see my profiles on ORCID or dblp for a (somewhat) uptodate list of publications.
Articles
Note: open access versions of most of these articles are available through DTU Orbit.

Verifying a Sequent Calculus Prover for FirstOrder Logic with Functions in Isabelle/HOL in the Journal of Automated Reasoning.
Asta Halkjær From & Frederik Krogsdal Jacobsen.
DOI: 10.1007/s10817024096973 
The Concurrent Calculi Formalisation Benchmark in the Proceedings of the 26th International Conference on Coordination Models and Languages (COORDINATION 2024).
Marco Carbone, David CastroPerez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Tirore, Martin Vassor, Nobuko Yoshida & Daniel Zackon.
DOI: 10.1007/9783031626975_9 
ProofBuddy: A Proof Assistant for Learning and Monitoring in the Proceedings of the
12th International Workshop on Trends in Functional
Programming in Education (TFPIE 2023).
Nadine Karsten, Frederik Krogsdal Jacobsen, Kim Jana Eiken, Uwe Nestmann & Jørgen Villadsen.
DOI: 10.4204/EPTCS.382.1 
On Exams with the Isabelle Proof Assistant in the Proceedings of the
11th
International Workshop on TheoremProving Components for
Educational Software (ThEdu 2022).
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
DOI: 10.4204/EPTCS.375.6 
Verifying a Sequent Calculus Prover for FirstOrder
Logic with Functions in Isabelle/HOL in the
Proceedings of the 13th
International Conference on Interactive Theorem Proving (ITP
2022).
Asta Halkjær From & Frederik Krogsdal Jacobsen.
DOI: 10.4230/LIPIcs.ITP.2022.13 
Teaching Functional Programmers Logic and
Metatheory
in the Proceedings of the 10th and
11th
International Workshop on Trends in Functional Programming In
Education (TFPIE 2022).
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
DOI: 10.4204/EPTCS.363.5 
Using Isabelle in Two Courses on Logic and Automated
Reasoning in the Proceedings of the
4th International Workshop
and Tutorial on Formal Methods Teaching (FMTea 2021).
Jørgen Villadsen & Frederik Krogsdal Jacobsen.
DOI: 10.1007/9783030915506_9 
SeCaV: A Sequent Calculus Verifier in
Isabelle/HOL in the Proceedings of the
16th International
Workshop on Logical and Semantic Frameworks with Applications
(LSFA 2021).
Asta Halkjær From, Frederik Krogsdal Jacobsen & Jørgen Villadsen.
DOI: 10.4204/EPTCS.357.4 
Do repeated transurethral procedures under general anesthesia
influence mortality in patients with noninvasive urothelial bladder
cancer? A Danish national cohort study in the
Scandinavian Journal of Urology, 54:4, 281289.
Marie Schmidt Eriksson, Astrid Christine Pedersen, Klaus Kaae Andersen, Frederik Krogsdal Jacobsen, Karin Mogensen & Gregers Gautier Hermann.
DOI: 10.1080/21681805.2020.1782978
Abstracts

ProofBuddy: Acquiring Proof Competence with Friendly Assistance
(extended abstract) at the 12th International Workshop on Trends in Functional Programming in Education (TFPIE 2023).
Nadine Karsten, Frederik Krogsdal Jacobsen, Uwe Nestmann & Jørgen Villadsen.
PDF: available from the workshop website. 
Lessons of Teaching Formal Methods with Isabelle
(extended abstract) at
the Isabelle
Workshop 2022.
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
PDF: available from the workshop website. 
On Exams with the Isabelle Proof Assistant
(extended abstract) at
the 11th
International Workshop on TheoremProving Components for
Educational Software (ThEdu 2022).
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
(To appear on workshop website) 
Teaching Logic for Computer Science Students: Proof Assistants and Related Tools (extended abstract) at
the Workshop on Why and how to teach Logic for CS undergraduates (LogTeach22).
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
Abstract available in the workshop program. 
Sequent Calculus Verifier (SeCaV) (tool description) at the Formal Methods Education Online 2022 workshop (FOMEO'22).
Asta Halkjær From, Frederik Krogsdal Jacobsen & Jørgen Villadsen.
Listed on the FOMEO website.
Published formalizations
 A Sequent Calculus Prover for FirstOrder Logic With Functions in the Archive of Formal Proofs (2022).
Asta Halkjær From & Frederik Krogsdal Jacobsen.
Theses
 Formalization of Logical Systems in Isabelle.
MSc Thesis (Computer Science and Engineering).
Frederik Krogsdal Jacobsen, 2021.
Available from the Technical Information Center of Denmark  A formally verified compiler backend for a timepredictable processor.
BSc Thesis (Electrical Engineering).
Frederik Krogsdal Jacobsen, 2019.
Available from the Technical Information Center of Denmark
Talks

The Concurrent Calculi Formalisation Benchmark
26th International Conference on Coordination Models and Languages, June 2024 (Slides) 
The Concurrent Calculi Formalisation Benchmark
Logic & AI @ AlgoLoG Seminar, May 2024 (Slides) 
Brugervenlige formelle metoder (invited talk, in Danish)
Danish Society of Engineers (IDA), May 2024 (Slides, Isabelle Example) 
Hvordan kan vi stole på en computer? (invited talk, in Danish)
Silkeborg Gymnasium, November 2023 (Slides, Isabelle Example) 
Porpoise: contextual secondorder abstract syntax in higherorder logic
Logic & AI @ AlgoLoG Seminar, November 2023 (Slides) 
Learning Proof Competence with Computer Assistance (invited talk)
Mobility Reading Group Seminar, University of Oxford, June 2023 (Slides) 
Formally Verifying a Theorem Prover for FirstOrder Logic (invited talk)
Formal Methods Seminar, Royal Holloway, University of London, March 2023 (Slides) 
Isabelle  an introduction (invited talk)
Proofs and Programs Club, Royal Holloway, University of London, February 2023 (Slides, Isabelle Examples) 
Teaching Functional Programmers Logic and Metatheory
AlgoLoG Seminar, November 2022 (Slides) 
Formalizing multiparty session types
Logic & AI @ AlgoLoG Seminar, September 2022 (Slides) 
Verifying a Sequent Calculus Prover for FirstOrder Logic with Functions in Isabelle/HOL
13th Conference on Interactive Theorem Proving (ITP), August 2022 (Slides)
Joint talk with Asta Halkjær From 
On Exams with the Isabelle Proof Assistant
11th International Workshop on TheoremProving Components for Educational Software (ThEdu), August 2022 (Slides) 
Lessons of Teaching Formal Methods with Isabelle
Isabelle Workshop, August 2022 (Slides) 
Proof Assistants and Related Tools
Why and how to teach Logic for CS undergraduates? (LogTeach), August 2022 (Slides) 
Teaching Functional Programmers Logic and Metatheory (invited talk)
Lambda Days, July 2022 (Slides, Video) 
Verifying a Sequent Calculus Prover
DTU Compute PhD Bazaar, July 2022 (Slides)
Joint talk with Asta Halkjær From 
Proving completeness by showing your work (participant talk)
Midlands Graduate School, April 2022 
A Comprehensible Automated Theorem Prover for the Sequent Calculus Verifier
DTU Compute Isabelle Workshop, November 2021 (Slides) 
UserFriendly Formal Methods
DTU Compute PhD Bazaar, August 2021 
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
16th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA), July 2021 (Slides, Video)
Software
 The Isabelle Cabal, which adds Isabelle code generation support to Cabal.

SeCaV Prover, an automated theorem prover for the SeCaV proof system.
Joint work with Asta Halkjær From. 
SeCaV Unshortener, a tool for translating proofs into formal SeCaV proofs.
Joint work with Asta Halkjær From, Emmanuel André Ryom, Oliver Emil Bøving, and Jørgen Villadsen.  coqmicroprover, an automated theorem prover for propositional logic.

A bidirectional typechecker for predicative System F, featuring complete MLstyle type inference.
Joint work with Sindri Pétur Ingimundarson.  cctlcheck, a prototype model checker for CTL over constraint semirings.
Teaching and supervision
If you are interested in writing your BSc or MSc thesis (or doing a special course) on a topic related to my interests, please feel free to contact me!
I have previously (co)supervised the following student projects:
 "Development of a Tour Guide for the Lambda Zoo" (BSc thesis)
 "Prover Programming" (BSc thesis)
 "Mechanized Ghost Code and Weakest Precondition Reasoning" (MSc thesis)
 "Tools for Resolution Calculus" (MSc thesis)
 "Formalization of Datalog in Isabelle" (MSc thesis)
 "Reactive Programming and Lambda Calculus" (special course)
 "Extension and Improvement of a proof tool" (special course)
 "Formalization in the Isabelle Proof Assistant" (special course)
 "Topics in Datalog and Relational Algebra" (special course)
 "A formally verified compiler for a functional programming language with linear types" (MSc thesis)
I have been a teaching assistant in the following courses at DTU:
 02256  Automated Reasoning (using Isabelle) (2022)
 02156  Logical Systems and Logic Programming (2020, 2021)
 02101  Introductory Programming (in Java) (2020)
 02102  Introductory Programming (in Java and C) (2020, 2021, 2022)
 31302  Linear control design 1 (2019)
 31300  Linear control design 1 (2019)
 01005  Advanced Engineering Mathematics 1 (2017)
Other stuff
I have worked professionally as a software developer since 2013,
last at the Danish
Cancer Society Research Center, where I worked until 2021
developing software for statistical cancer research.
Before that I worked with content management and pricing systems
for travel products.
I am a member of the board
of IDA Young Professionals,
which supports engineers at the start of their careers by
organizing talks, workshops and other events that provide useful
skills.
I was a member of the board of
DTU Climbing, one of the
largest climbing clubs in Denmark, from 2022 to 2024.
I was a member of the board of the small nonprofit internet
service provider KNet from 2017 to 2021.
I was vice chairman of the board for most of that time.
I also used to volunteer as a Network Operations Engineer in the KNet Operations Group.
I helped start the Vermilion Racing team at DTU, where I designed safety critical electronics and software for their electric vehicle.
Contact
If you would like to see a more detailed resume, you can visit my LinkedIn page.
If you want to talk about something, please write me at fkjacobsen@gmail.com.