My main interest these days is privacy-preserving identity verification and authentication for digital transactions. This is useful for things such as fraud prevention and anti-money laundering. Mainly, it is useful for ordinary people who don't want to reveal all of their personal information whenever they need to prove that they are old enough to buy a beer.
I am also interested in formal methods for logic and distributed systems and in the context of teaching. In particular, I am interested in proof assistants (interactive theorem provers) and model checking. I have done a lot of research on these topics in the past (see below), but I don't really have time for it any more.
I was a PhD student at DTU Compute from July 2021 to June 2024, working on User-Friendly Formal Methods, especially for distributed systems and using Isabelle/HOL. My supervisor was Jørgen Villadsen, and my co-supervisor was Alceste Scalas.
I am currently not working on anything in particular. Check out my GitHub page to see what I might be up to.
Please see my profiles on ORCID or dblp for a (somewhat) up-to-date list of scientific publications.
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 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
Note: open access versions of most of these articles are available through DTU Orbit.
-
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
-
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
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.