Asta (formerly Andreas) Halkjær From

I am a PhD student at DTU Compute since February 2020 working on Formally Correct Deduction Methods for Computational Logic, especially using the proof assistant Isabelle/HOL. My supervisor is Jørgen Villadsen and my co-supervisor is Nina Gierasimczuk.

I was a MSc student on the Honours Programme in Computer Science and Engineering at DTU from 2018 to 2020. My MSc thesis on Hybrid Logic was supervised by Jørgen Villadsen, Alexander Birch Jensen and Patrick Blackburn.


Published formalizations


  • Formalized soundness and completeness of natural deduction for first-order logic at SLS 2018
    Andreas Halkjær From.

    Abstract, Slides

  • Teaching first-order logic with the natural deduction assistant (NaDeA) at SLS 2018
    Andreas Halkjær From, Helge Hatteland, Jørgen Villadsen.


  • MSc: Hybrid Logic (January 2020)

    My MSc thesis on formalizing the soundness and completeness of a Seligman-style tableau system for hybrid logic in Isabelle/HOL.

    Thesis, Slides

  • BSc: Formalized First-Order Logic (July 2017)

    My BSc thesis on formalizing the soundness and completeness of NaDeA in Isabelle/HOL.

    Report, Slides (Danish)



  • A Pretty but not Greedy Printer (January 2018)

    My implementation of Jean-Philippe Bernardy's A Pretty But Not Greedy Printer (Functional Pearl). PACMPL 1(ICFP): 6:1-6:21 (2017) in OCaml. The author of the paper has a version in Haskell.

    GitHub, OPAM

  • Sudoku Solver (June 2016)

    A solver for large Sudoku puzzles which we wrote as a fourth-semester final project. Solving is done either using our own backtracking tactic solver or with an external SAT solver by compiling the problem into the CNF-format DIMACS. The GitHub page includes an abstract in English.

    GitHub, PDF (Danish)

  • The Playground (December 2015)

    My solution to an internal programming competition in the Algorithms and Data Structures 2 course at DTU. The readme includes a description of the problem and my algorithm as well as fully annotated version of the C code.


Work Experience

Teaching Assistant

I am or have been a TA in the following courses:
  • 02101 Introductory Programming, fall 2015
  • 02105 Algorithms and Data Structures 1, spring 2016
  • 02101 Introductory Programming, fall 2016
  • 02110 Algorithms and Data Structures 2, fall 2016
  • 02105 Algorithms and Data Structures 1, spring 2017
  • 02180 Introduction to Artificial Intelligence, spring 2018
  • 02156 Logical Systems and Logic Programming, fall 2018
  • 02156 Logical Systems and Logic Programming, fall 2019
  • 02102 Introductory Programming, spring 2020
  • 02256 Automated Reasoning, spring 2020
  • 02287 Logical Theories for Uncertainty and Learning, fall 2020
I have also helped teach kids aged 9-12 years old game programming in MIT Scratch at Hello World.

Research Assistant

I worked as a research assistant at DTU Compute from August 2017 to December 2017, working with Isabelle and NaDeA, especially translating students' proofs in NaDeA to their encodings in Isabelle.