Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification.
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.
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
Jørgen Villadsen 2018-01-16 https://hol.compute.dtu.dk/