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

Isabelle/HOL as a MetaLanguage for Teaching Logic in
ThEdu'20 postproceedings
Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn.
DOI: 10.4204/EPTCS.328.2

Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road
Ahead at AiML 2020
Asta Halkjær From
Booklet: PDF

Formalizing HenkinStyle Completeness of an Axiomatic System for Propositional
Logic
at WeSSLLII + ESSLLI Virtual Student Session 2020 Asta Halkjær FromProceedings: PDF
 A Concise Sequent Calculus for Teaching FirstOrder Logic at Isabelle Workshop 2020 Asta Halkjær From, Jørgen Villadsen.

Formalizing a SeligmanStyle Tableau System for Hybrid Logic (short paper) at
IJCAR 2020
Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen.
DOI: 10.1007/9783030510749_27
Talk: YouTube 
Teaching a Formalized Logical Calculus in
ThEdu'19 postproceedings
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen.
DOI: 10.4204/EPTCS.313.5

MultiAgent Programming Contest 2018 
The JasonDTU Team
Jørgen Villadsen, Mads Okholm Bjørn, Andreas Halkjær From, Thomas Søren Henney, John
Bruntse Larsen.
Lecture Notes in Computer Science, vol 11957, pp. 4171. Springer.
Editors: Tobias Ahlbrecht, Jürgen Dix and Niklas Fiekas.  A Verified Simple Prover for FirstOrder Logic at PAAR 2018 Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.

Students' Proof Assistant (SPA) in
ThEdu'18 postproceedings
Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From.
DOI: 10.4204/EPTCS.290.1

Natural Deduction Assistant (NaDeA) in
ThEdu'18 postproceedings
Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull.
DOI: 10.4204/EPTCS.290.2
 Substitutionless FirstOrder Logic: A Formal Soundness Proof at Isabelle Workshop 2018 Andreas Halkjær From, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen.
 Drawing Trees at Isabelle Workshop 2018 Andreas Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.

Natural Deduction and the Isabelle Proof Assistant in
ThEdu'17 postproceedings
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

MultiAgent Programming Contest 2016  The PythonDTU 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 PythonDTU team for the MultiAgent Programming Contest 2016.
 Code Generation for a Simple FirstOrder Prover at Isabelle Workshop 2016 Jørgen Villadsen, Anders Schlichtkrull, Andreas Halkjær From.
Published formalizations

Hybrid Logic in
Archive of Formal Proofs (December 2019)
Asta Halkjær From
The formalization accompanying my MSc thesis.
The development version contains the latest results. 
A Sequent Calculus for FirstOrder Logic in
Archive of Formal Proofs (July 2019)
Andreas Halkjær From
This work formalizes soundness and completeness of a onesided sequent calculus for firstorder logic. The completeness is shown via a translation from a complete semantic tableau calculus, the proof of which is based on the FirstOrder Logic According to Fitting theory. The calculi and proof techniques are taken from BenAri's Mathematical Logic for Computer Science.

Epistemic Logic in
Archive of Formal Proofs (October 2018)
Andreas Halkjær From
This work is a formalization of epistemic logic with countably many agents. It includes proofs of soundness and completeness for the axiom system K. The completeness proof is based on the textbook "Reasoning About Knowledge" by Fagin, Halpern, Moses and Vardi (MIT Press 1995).

IsaFoL: Isabelle Formalization of Logic
I have contributed to a number of formalizations in the IsaFoL project:
Abstracts
Theses

MSc: Hybrid Logic (January 2020)
My MSc thesis on formalizing the soundness and completeness of a Seligmanstyle tableau system for hybrid logic in Isabelle/HOL.

BSc: Formalized FirstOrder Logic (July 2017)
My BSc thesis on formalizing the soundness and completeness of NaDeA in Isabelle/HOL.
Talks

Hybrid Logic (January 2021)
Given at 3rd World Logic Day  14 January 2021  A Zoom on Logic..

Belief Revision and Isabelle/HOL (November 2020)
Given at a DTU seminar course.

Hybrid Logic in the Isabelle Proof Assistant: Benefits, Challenges and the Road Ahead
Given at AiML 2020.

Formally Correct Deduction Methods for Computational Logic (July 2020)
Given at CICM 2020 doctoral session.

Formalizing HenkinStyle Completeness of an Axiomatic System for Propositional Logic (July 2020)

Formalizing a SeligmanStyle Tableau System for Hybrid Logic (July 2020)
Overview of our paper. Recording: YouTube. Given at IJCAR 2020.

A Concise Sequent Calculus for Teaching FirstOrder Logic (June 2020)
Overview of our paper. Recording: YouTube. Given at the Isabelle Workshop 2020.

The Isabelle Proof Assistant and Hybrid Logic: Formalizing SeligmanStyle Tableaux (October 2019)
Update on my MSc thesis work. Given at an AlgoLoG seminar at DTU.

Using the Isabelle Proof Assistant: SeligmanStyle Tableau for Hybrid Logic (September 2019)
The Isabelle proof assistant can be used to mechanically develop and check results in logic, mathematics, computer science etc. In this talk I motivate this process and explain how it looks in practice for a basic hybrid logic. The running example will be preliminary work on the completeness and termination for a Seligmanstyle tableau system by Blackburn, Bolander, Braüner and Jørgensen. Given at The LogicS of Prior Past, Present, and Future at Roskilde University.

Magnolia – Implementing System F with Anonymous Sums and Products (March 2018)
Overview of the Complete and Easy Bidirectional Type Checking for HigherRank Polymorphism paper as well as my own additions. Also briefly describes Abstract Binding Trees. Given at DTU.

FIT – From's Isabelle Tutorial – Verification of Quicksort (October 2017)
A fastpaced, handson introduction to Isabelle/HOL I gave at PART DTU.
Software

A Pretty but not Greedy Printer (January 2018)
My implementation of JeanPhilippe Bernardy's A Pretty But Not Greedy Printer (Functional Pearl). PACMPL 1(ICFP): 6:16:21 (2017) in OCaml. The author of the paper has a version in Haskell.

Sudoku Solver (June 2016)
A solver for large Sudoku puzzles which we wrote as a fourthsemester final project. Solving is done either using our own backtracking tactic solver or with an external SAT solver by compiling the problem into the CNFformat DIMACS. The GitHub page includes an abstract in English.

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