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.

Local Isabelle Workshop - 6 Talks 6/6 2018 13:00-15:00 at DTU building 303B room 034

13:00 Jørgen Villadsen (joint work with Andreas Halkjær From, John Bruntse Larsen and Anders Schlichtkrull): Substitutionless First-Order Logic: A Formal Soundness Proof

13:20 Helge Hatteland (joint work with Andreas Halkjær From and Jørgen Villadsen): Teaching First-Order Logic with the Natural Deduction Assistant (NaDeA)

13:40 Andreas Halkjær From: Formalized Soundness and Completeness of Natural Deduction for First-Order Logic

14:00 Anders Schlichtkrull (joint work with Andreas Halkjær From and Jørgen Villadsen): Drawing Trees

14:20 Andreas Viktor Hess (joint work with Sebastian A. Mödersheim): A Typing Result for Stateful Protocols

14:40 John Bruntse Larsen: Operational Semantics for Organizational Reasoning in Agent-Based Simulation

Informal Workshop on Formal Proofs - Friday 16 March 2018 at DTU Meeting Center in building 101 room S08

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

Workshop on Programs & Proofs - Thursday 15 March 2018 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): 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

Abstract of talk by Martin Elsman: The general-purpose Standard ML functional programming language, with its stable formal definition and long research tradition, enables higher-order and typed application development. Its rich core and module languages allow programmers to write useful abstract components and its Standard Basis Library provides a foundation for writing new generic components. For a language to be useful in practice, however, proper tooling is essential, including support for foreign function integration, an enriched set of libraries, and tooling for managing build- and recompile-processes. In this talk, we give an overview of the MLKit Standard ML compiler tool kit, which, with a common Standard ML frontend and build system, features (1) the MLKit with Regions compiler, an efficient native x86 region-based compiler backend, (2) SMLserver, a region-based bytecode backend suitable for web-server integration, and (3) SMLtoJs, a Javascript backend suitable for writing client-side web applications. We outline some of the nifty features of the MLKit and report on how the tool kit is used for developing real-world applications with Standard ML code being compiled for and executed on different tiers of an application. This ability allows, for instance, in the context of web applications, for migration of values between tiers using a highly efficient type-indexed binary serialisation library written purely in Standard ML. Other features include an efficient generic database library for SMLserver and an SMLtoJs library for client-side functional reactive programming.

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/.

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

Contact

Photo: Jørgen Villadsen

Jørgen Villadsen 2018-06-04 https://hol.compute.dtu.dk/