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.

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

Published formalizations

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

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.