I am a PhD student at DTU Compute since July 2021, working on User-Friendly Formal Methods, especially for distributed systems and using Isabelle/HOL.
My supervisor is Jørgen Villadsen, and my co-supervisor is Alceste Scalas. You can find more information, including a popular science abstract, on the department page about my project.
I am interested in formal methods, especially for safety critical embedded systems and distributed systems. This interest includes both hardware and software systems, especially if the systems also have hard real-time targets. I am also interested in formal methods in the context of teaching.
I am currently working on:
- formalizing proof techniques for process calculi
- formalizing multiparty session types in Isabelle/HOL
- approaches to teaching logic (especially using Isabelle)
- formalizing first-order logic in Isabelle/HOL
Please see my profiles on ORCID or dblp for a (somewhat) up-to-date list of publications.
Articles
Note: open access versions of most of these articles are available through DTU Orbit.
-
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
-
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
- 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 back-end for a time-predictable processor.
BSc Thesis (Electrical Engineering).
Frederik Krogsdal Jacobsen, 2019.
Available from the Technical Information Center of Denmark
Talks
-
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 System F, featuring complete type inference.
Joint work with Sindri Pétur Ingimundarson. - c-ctl-check, a prototype model checker for CTL over constraint semirings.
Teaching and supervision
I am currently (co-)supervising the following student projects:
- "Reactive Programming and Lambda Calculus" (special course)
- "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)
I have previously (co-)supervised the following student projects:
- "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)
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 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
DTU Climbing, one of the
largest climbing clubs in Denmark.
I was for a long time a member of the board of the small internet
service provider K-Net.
I was vice chairman of the board for a few years.
I also used to volunteer in the K-Net Operations Group.
I once volunteered at the Vermilion Racing team at DTU, where I designed safety critical electronics in collaboration with a number of other people, but unfortunately I don't have the time any more.
Contact
If you would like to see a more detailed resume, you can
visit my LinkedIn
page.
If you would like to check out what I am working on, you can visit
my GitHub page.
For inquiries relating to my job, please write me
at fkjac@dtu.dk.
If you want to talk about something else, please write me
at fkjacobsen@gmail.com.
I am currently on a research visit to the UK, and am thus not in office.