Alexander Birch Jensen
In August 2016 I obtained the MSc in Computer Science and Engineering degree on the Honours Programme at DTU (Technical University of Denmark).
I was a research assistant at DTU Compute from September 2016 to January 2017 and then I was a software developer at PDC A/S.
From February 2019 I am a PhD student at DTU Compute:
PhD project: Logical Foundations of AI Algorithms
This project takes up the challenge of developing new AI algorithms with provable properties of functional correctness including safety, security, soundness, completeness and termination. Building upon recent advancements, the project strives to combine functional programming languages like SML, Haskell, OCaml and Scala with type systems and programming in the Isabelle proof assistant to achieve robust and efficient algorithms based on logical foundations.
Main supervisor: Jørgen Villadsen, DTU Compute - Algorithms, Logic and Graphs Section
Co-supervisor: Sebastian Mödersheim, DTU Compute - Formal Methods Section
List of publications
Programming and Verifying a Declarative First-Order Prover in Isabelle/HOL.
Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull & Jørgen Villadsen.
AI Communications 31:281-299 2018.
First-Order Logic According to Harrison.
Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen.
Archive of Formal Proofs - Isabelle Document 1-66 2017.
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle.
Jørgen Villadsen, Alexander Birch Jensen & Anders Schlichtkrull.
IFCoLog Journal of Logics and their Applications 4:55-82 2017.
Development and Verification of a Proof Assistant.
Alexander Birch Jensen,
Master's Thesis, Technical University of Denmark, 2016.
Verification of an LCF-Style First-Order Prover with Equality.
Alexander Birch Jensen, Anders Schlichtkrull & Jørgen Villadsen.
Isabelle Workshop 2016.