Frederik Krogsdal Jacobsen

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 for safety critical embedded systems and distributed systems. I am also interested in formal methods in the context of teaching.

I am currently working on:

• formal proof techniques for process calculi (join us!)
• formalizing multiparty session types
• the metatheory of ghost code

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.

• 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.
  Accepted for publication in LNCS.
• 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.
  Accepted for publication in special issue: Selected Extended Papers of ITP 2022.
• 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

Talks

• 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.

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.

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.

You may be able to find me in my office: