Asta (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.

Articles

  • Multi-Agent Programming Contest 2018 - The Jason-DTU Team
    Jørgen Villadsen, Mads Okholm Bjørn, Andreas Halkjær From, Thomas Søren Henney, John Bruntse Larsen.

    Editors: Tobias Ahlbrecht, Jürgen Dix and Niklas Fiekas.
    Accepted, to appear in Springer Lecture Notes in Computer Science (pp. 1-31).


  • A Verified Simple Prover for First-Order Logic at PAAR 2018
    Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.

    PDF

  • Students' Proof Assistant (SPA) in ThEdu'18 post-proceedings
    Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From.

    DOI: 10.4204/EPTCS.290.1

  • Natural Deduction Assistant (NaDeA) in ThEdu'18 post-proceedings
    Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.

    DOI: 10.4204/EPTCS.290.2

  • Substitutionless First-Order Logic: A Formal Soundness Proof at Isabelle Workshop 2018
    Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen.

    PDF

  • Drawing Trees at Isabelle Workshop 2018
    Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.

    PDF, Isabelle theory

  • Natural Deduction and the Isabelle Proof Assistant in ThEdu'17 post-proceedings
    Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.

    Includes my work on translating online NaDeA proofs to the Isabelle encoding of the proof system.

    DOI: 10.4204/EPTCS.267.9

  • Multi-Agent Programming Contest 2016 - The Python-DTU Team in IJAOSE 2018
    Jørgen Villadsen, Andreas Halkjær From, Salvador Jacobi, Nikolaj Nøkkentved Larsen.

    I did the initial work on the code used by the Python-DTU team for the Multi-Agent Programming Contest 2016.

    DOI: 10.1504/IJAOSE.2018.10010604

  • Code Generation for a Simple First-Order Prover at Isabelle Workshop 2016
    Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.

    PDF

Published formalizations

Abstracts

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

Theses

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

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

    Report, Slides (Danish)

  • 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

Talks

Software

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

    GitHub

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