About me
Hey, I'm Frederik! I'm a Staff Engineer at Idura, where I work on privacy-preserving digital identity verification. Identity verification is useful for a lot of things such as fraud prevention and anti-money laundering. Privacy preservation means that people shouldn't have to reveal all of their personal information just to buy a beer.
A big part of my work consists of contributing to standards at the OpenID Foundation, the Internet Engineering Task Force and the World Wide Web Consortium. A smaller part consists of advising on standards, business models and public policy and legislation. I also do a lot of programming, mostly in F# and TypeScript.
I am interested in, and have experience with:
- Formal verification of software
- Software engineering tools for functional programming languages
- Type theory for distributed systems (and in general)
- Proof assistants (interactive theorem provers)
- Static program analysis tools
- Security properties of internet standards
- Approaches for teaching formal methods
- Structural proof theory
If you are a student interested in writing your thesis on one of these topics, feel free to contact me and we might be able to work something out!
Check out my GitHub page or my LinkedIn page to see what I might be up to.
Talks
-
The wallet ecosystem of the future
Criipto Connect, November 2025 -
Introduction to identity verification
Seminar for Experis Norway, November 2025 -
Towards user-friendly proof mechanization
PhD defense lecture, DTU Compute, October 2024 (Slides) -
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 second-order abstract syntax in higher-order 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 First-Order 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 First-Order 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 Theorem-Proving 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) -
User-Friendly 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. - coq-microprover, an automated theorem prover for propositional logic.
-
A bidirectional typechecker for predicative System F, featuring complete ML-style type inference.
Joint work with Sindri Pétur Ingimundarson. - c-ctl-check, a prototype model checker for CTL over constraint semirings.
Articles
Please see my profiles on ORCID or dblp for a (somewhat) up-to-date list of scientific publications.
-
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL in the Journal of Automated Reasoning.
Asta Halkjær From & Frederik Krogsdal Jacobsen.
DOI: 10.1007/s10817-024-09697-3 -
The Concurrent Calculi Formalisation Benchmark in the Proceedings of the 26th International Conference on Coordination Models and Languages (COORDINATION 2024).
Marco Carbone, David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, Frederik Krogsdal Jacobsen, Alberto Momigliano, Luca Padovani, Alceste Scalas, Dawit Tirore, Martin Vassor, Nobuko Yoshida & Daniel Zackon.
DOI: 10.1007/978-3-031-62697-5_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 Theorem-Proving Components for
Educational Software (ThEdu 2022).
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
DOI: 10.4204/EPTCS.375.6 -
Verifying a Sequent Calculus Prover for First-Order
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/978-3-030-91550-6_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 non-invasive urothelial bladder
cancer? A Danish national cohort study in the
Scandinavian Journal of Urology, 54:4, 281-289.
Marie Schmidt Eriksson, Astrid Christine Pedersen, Klaus Kaae Andersen, Frederik Krogsdal Jacobsen, Karin Mogensen & Gregers Gautier Hermann.
DOI: 10.1080/21681805.2020.1782978
Abstracts
-
A Formalization of Sequent Calculus for Classical Implicational Logic
(extended abstract) at the Isabelle Workshop 2024.
Frederik Krogsdal Jacobsen & Jørgen Villadsen.
PDF: available from the workshop website. -
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 Theorem-Proving 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 (LogTeach-22).
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 First-Order Logic With Functions in the Archive of Formal Proofs (2022).
Asta Halkjær From & Frederik Krogsdal Jacobsen.
Theses
- User-Friendly Formal Methods: Towards user-friendly proof mechanization.
PhD Thesis.
Frederik Krogsdal Jacobsen, 2024 (PDF). - Formalization of Logical Systems in Isabelle.
MSc Thesis (Computer Science and Engineering).
Frederik Krogsdal Jacobsen, 2021 (PDF). - A formally verified compiler back-end for a time-predictable processor.
BSc Thesis (Electrical Engineering).
Frederik Krogsdal Jacobsen, 2019 (PDF).
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 non-profit internet
service provider K-Net 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 K-Net 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, you can write me at fkjacobsen@gmail.com. I usually respond pretty quickly. If I don't, feel free to follow-up after a few days.