Asta Halkjær From

Curriculum vitae

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.

Presence elsewhere

GitHub

dblp

ORCID
0000-0002-3601-0804

Academic Activities

Co-chair of the Logic and Computation track for the Student Session @ 32nd European Summer School in Logic, Language and Information (ESSLLI 2021).

Awards

DTU Travel Grant awarded to me personally by DTU's executive board, February 2022, in recognition of my academic qualities and merits.

Articles

A Succinct Formalization of the Completeness of First-Order Logic in TYPES 2021 post-proceedings
Asta Halkjær From.

DOI: 10.4230/LIPIcs.TYPES.2021.8
Formalization: First-Order Logic
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL at ITP 2022
Asta Halkjær From, Frederik Krogsdal Jacobsen.

DOI: 10.4230/LIPIcs.ITP.2022.13
Formalization: Prover for First-Order Logic
On Termination for Hybrid Tableaux at Isabelle Workshop 2022
Asta Halkjær From.

Paper: PDF
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL in Proceedings 16th Logical and Semantic Frameworks with Applications (LSFA 2021)
Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen.

DOI: 10.4204/EPTCS.357.4
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle in ThEdu'21 post-proceedings
Jørgen Villadsen, Asta Halkjær From, Patrick Blackburn.

DOI: 10.4204/EPTCS.354.6
Interactive Theorem Proving for Logic and Information in Natural Language Processing in Artificial Intelligence — NLPinAI 2021
Jørgen Villadsen, Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull.

DOI: 10.1007/978-3-030-90138-7_2
Formalizations: Epistemic Logic, Public Announcement Logic
Formalized Soundness and Completeness of Epistemic Logic at WoLLIC 2021
Asta Halkjær From.

DOI: 10.1007/978-3-030-88853-4_1
Formalization: Epistemic Logic
A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL at CILC 2021
Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.

CEUR-WS: PDF
Formalization: Sequent Calculus
A Case Study in Computer-Assisted Meta-reasoning at DCAI 2021, Special Session on Computational Linguistics, Information, Reasoning, and AI (CompLingInfoReasAI'21)
Asta Halkjær From, Simon Tobias Lund, Jørgen Villadsen.

DOI: 10.1007/978-3-030-86887-1_5
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL at Conference on Intelligent Computer Mathematics (CICM 2021)
Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen.

DOI: 10.1007/978-3-030-81097-9_3
Teaching Automated Reasoning and Formally Verified Functional Programming in Agda and Isabelle/HOL at 10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021)
Asta Halkjær From, Jørgen Villadsen.

Paper: PDF
Formalizations: GitHub
Synthetic Completeness for a Terminating Seligman-Style Tableau System in TYPES 2020 post-proceedings
Asta Halkjær From.

DOI: 10.4230/LIPIcs.TYPES.2020.5
Formalization: Hybrid Logic
Isabelle/HOL as a Meta-Language for Teaching Logic in ThEdu'20 post-proceedings
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 (short paper) at AiML 2020
Asta Halkjær From

Booklet: PDF
Formalization: Hybrid Logic
Formalizing Henkin-Style Completeness of an Axiomatic System for Propositional Logic
at WeSSLLII + ESSLLI Virtual Student Session 2020
Asta Halkjær From

Proceedings: PDF
A Concise Sequent Calculus for Teaching First-Order Logic at Isabelle Workshop 2020
Asta Halkjær From, Jørgen Villadsen.

Paper: PDF
Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) at IJCAR 2020
Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen.

DOI: 10.1007/978-3-030-51074-9_27
Formalization: Hybrid Logic
Teaching a Formalized Logical Calculus in ThEdu'19 post-proceedings
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen.

DOI: 10.4204/EPTCS.313.5
Multi-Agent Programming Contest 2018 - The Jason-DTU Team
Jørgen Villadsen, Mads Okholm Bjørn, A. Halkjær From, Thomas Søren Henney, John Bruntse Larsen.

DOI: 10.1007/978-3-030-37959-9_3
A Verified Simple Prover for First-Order Logic at PAAR 2018
Jørgen Villadsen, Anders Schlichtkrull, A. Halkjær From.

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

DOI: 10.4204/EPTCS.290.1
Natural Deduction Assistant (NaDeA) in ThEdu'18 post-proceedings
Jørgen Villadsen, A. Halkjær From, Anders Schlichtkrull.

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

Paper: PDF
Drawing Trees at Isabelle Workshop 2018
A. Halkjær From, Anders Schlichtkrull, Jørgen Villadsen.

Paper: PDF, Formalization: Isabelle theory
Natural Deduction and the Isabelle Proof Assistant in ThEdu'17 post-proceedings
Jørgen Villadsen, A. Halkjær From, Anders Schlichtkrull.

DOI: 10.4204/EPTCS.267.9
Multi-Agent Programming Contest 2016 - The Python-DTU Team in IJAOSE 2018
Jørgen Villadsen, A. Halkjær From, Salvador Jacobi, Nikolaj Nøkkentved Larsen.

DOI: 10.1504/IJAOSE.2018.10010604
Code Generation for a Simple First-Order Prover at Isabelle Workshop 2016
Jørgen Villadsen, Anders Schlichtkrull, A. Halkjær From.

Paper: PDF

Published formalizations

Soundness and Completeness of Implicational Logic in Archive of Formal Proofs (September 2022)
Asta Halkjær From, Jørgen Villadsen

Website, Outline (PDF), Isabelle Theory
A Naive Prover for First-Order Logic in Archive of Formal Proofs (March 2022)
Asta Halkjær From

Website, Outline (PDF), Result Theory
A Sequent Calculus Prover for First-Order Logic with Functions in Archive of Formal Proofs (February 2022)
Asta Halkjær From, Frederik Krogsdal Jacobsen

Website, Outline (PDF), Results Theory
Soundness and Completeness of an Axiomatic System for First-Order Logic in Archive of Formal Proofs (October 2021)
Asta Halkjær From

Website, Outline (PDF), Theory
Public Announcement Logic in Archive of Formal Proofs (June 2021)
Asta Halkjær From

Website, Outline (PDF), Theory
Epistemic Logic: Completeness of Modal Logics in Archive of Formal Proofs (October 2018, updated April 2021)
Asta Halkjær From

Website, Outline (PDF), Theory
Hybrid Logic in Archive of Formal Proofs (December 2019, updated June 2020)
Asta Halkjær From

Website, Outline (PDF), Theory
A Sequent Calculus for First-Order Logic in Archive of Formal Proofs (July 2019)
Asta Halkjær From

Website, Outline (PDF), Theory
IsaFoL: Isabelle Formalization of Logic
I have contributed to a number of formalizations in the IsaFoL project:

Abstracts

On the Use of Isabelle/HOL for Formalizing New Concise Axiomatic Systems for Classical Propositional Logic at TYPES 2021
Asta Halkjær From and Jørgen Villadsen

Abstract, Slides, Presentation, Zoom session
Formalized Soundness and Completeness of Epistemic Logic at LAMAS & SR 2021
Asta Halkjær From, Alexander Birch Jensen and Jørgen Villadsen

Abstract, Slides
Formalized soundness and completeness of natural deduction for first-order logic at SLS 2018
A. Halkjær From.

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

Theses

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)

Talks

Generic Epistemic and Public Announcement Logic Completeness Results (September 2022)

Given at a Logic & AI @ AlgoLoG seminar, DTU Compute.
Verifying a Sequent Calculus Prover (August 2022)

Given at the ITP 2022 conference together with Frederik Krogsdal Jacobsen.
On Termination for Hybrid Tableaux (August 2022)

Given at the Isabelle Workshop 2022.
Verifying a Sequent Calculus Prover (July 2022)

Given at the DTU PhD Bazaar together with Frederik Krogsdal Jacobsen.
A Naive Prover for First-Order Logic - LSD Seminar (May 2022)

Invited talk at the Languages, Systems, and Data Seminar (Spring 2022).
A Naive Prover for First-Order Logic - 02256 (April 2022)

Guest talk in the course 02256 Automated Reasoning at the Technical University of Denmark.
Formalized Soundness and Completeness of Epistemic Logic (October 2021)

Given at WoLLIC 2021.
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL (July 2021)

Given at CICM 2021.
Formalized Soundness and Completeness of Epistemic Logic (May 2021)

Given at LAMAS & SR 2021.
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 Henkin-Style Completeness of an Axiomatic System for Propositional Logic (July 2020)

Given at WeSSLLI + ESSLLI Virtual Student Session 2020.
Formalizing a Seligman-Style Tableau System for Hybrid Logic (July 2020)

Overview of our paper. Recording: YouTube. Given at IJCAR 2020.
A Concise Sequent Calculus for Teaching First-Order Logic (June 2020)

Overview of our paper. Recording: YouTube. Given at the Isabelle Workshop 2020.
The Isabelle Proof Assistant and Hybrid Logic: Formalizing Seligman-Style Tableaux (October 2019)

Update on my MSc thesis work. Given at an AlgoLoG seminar at DTU.
Using the Isabelle Proof Assistant: Seligman-Style 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 Seligman-style tableau system by Blackburn, Bolander, Braüner and Jørgensen. Given at The LogicS of Prior Past, Present, and Future at Roskilde University.
Formalized Soundness and Completeness of Natural Deduction for First-Order Logic (June 2018)

Given at Scandinavian Logic Symposisum 2018 in Gothenburg.
Formalized Soundness and Completeness of Natural Deduction for First-Order Logic (June 2018)

Given at Local Isabelle Workshop 2018 at DTU.
Magnolia – Implementing System F with Anonymous Sums and Products (March 2018)

Overview of the Complete and Easy Bidirectional Type Checking for Higher-Rank 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 fast-paced, hands-on introduction to Isabelle/HOL I gave at PART DTU.

Work Experience

Teaching Assistant

I have been a TA in the following courses:

02287 Logical Theories for Uncertainty and Learning, fall 2020
02256 Automated Reasoning, spring 2020
02102 Introductory Programming, spring 2020
02156 Logical Systems and Logic Programming, fall 2019
02156 Logical Systems and Logic Programming, fall 2018
02180 Introduction to Artificial Intelligence, spring 2018
02105 Algorithms and Data Structures 1, spring 2017
02110 Algorithms and Data Structures 2, fall 2016
02101 Introductory Programming, fall 2016
02105 Algorithms and Data Structures 1, spring 2016
02101 Introductory Programming, fall 2015

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.