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, 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 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

• 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

• 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

• 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 an MSc thesis project titled "A formally verified compiler for a functional programming language with linear types".

If you are a student at DTU and are interested in writing your BSc or MSc thesis 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.

You may be able to find me in: