Higher-Order Logic - DTU Compute - Denmark

Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification.

Workshop 15 March 2018 (Thursday) at DTU Meeting Center building 101 room S04

13:00-13:30 Jørgen Villadsen (DTU Compute, joint work with Anders Schlichtkrull): Code Generation in Isabelle/HOL for Students' Proof Assistant (SPA)
13:30-14:30 Martin Elsman (University of Copenhagen): TBA

15:00-15:30 Andreas Halkjær From (DTU Compute): Implementing System F with Anonymous Sums and Products
15:30-16:30 Lars Hupel (Technische Universität München, joint work with Tobias Nipkow): A Verified Compiler from Isabelle/HOL to CakeML

Abstract of talk by Lars Hupel: Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML.

About Isabelle

Getting Started with Isabelle

IsaFoL: Isabelle Formalization of Logic

Proof Assistants and Related Tools - The PART Projects

NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle


Photo: Jørgen Villadsen

Jørgen Villadsen 2018-01-16 https://hol.compute.dtu.dk/