Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification.
10:30-11:30 Jørgen Villadsen (DTU Compute): We consider the following theorem and the proof in the proof assistant Isabelle: "The set of real numbers R is not countable" P. 35: Fundamental Concepts in Modern Analysis, Vagn Lundsgaard Hansen, World Scientific 1999
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): The MLKit Standard ML Compiler Tool Kit 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
Martin Elsman is Associate Professor at Department of Computer Science, University of Copenhagen (DIKU), where he serves as manager for the HIPERFIT Research Center, a center that focuses on high-performance functional computing techniques for financial information technology. Before joining DIKU in 2012, Martin spent four years in SimCorp developing software, using functional programming techniques, for specifying and managing financial contracts. Before his time at SimCorp, Martin was Associate Professor at the IT University of Copenhagen. Martin conducts research in the areas of domain-specific languages for financial contracts and compilation techniques for functional languages, in particular with focus on data-parallel languages, module systems, Web technology, program analyses for memory management, and program optimisation. Martin is the co-developer of a number of systems and tools. For more information, see http://www.elsman.com.
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.
Lars Hupel is a PhD student at TU München in the field of logic and verification. His research focus is on techniques for verified code generation from theorem provers. Additionally, he has worked on formal treatments of Linux firewalls. A frequent conference speaker and co-founder of the Typelevel initiative, he is active in the open source community, particularly in Scala. He also enjoys programming in Haskell, Prolog, and Rust. The full CV can be found at https://lars.hupel.info/cv/.
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-02-16 https://hol.compute.dtu.dk/