DIKU Bits by Asta Halkjær From

DIKU bits picture

Speaker

Asta Halkjær From, Postdoc in the SDPS (Software, Data, People & Society) section.

Title

How to Speak Logic with Your Computer: The unreasonable effectiveness of a machine assistant

Abstract

Imagine if LaTeX could check your work and fill out parts of your proofs for you.
In this talk, I will introduce higher-order logic and the Isabelle proof assistant.
Unlike English, sentences in logic have a precise meaning.
This means we can do computer science and mathematics in a language that both humans and computers can "speak".
I do most of my own work on logic with Isabelle as my companion.