Portal for research and teaching in higher-order logic, in particular using the proof assistant Isabelle for formalization and verification.
10:15 Lawrence C. Paulson FRS (Director of Research, Computer Laboratory, University of Cambridge, UK): Formalised Mathematics: Obstacles and Achievements
Abstract: The practice of formalising mathematics is starting to attract the attention of mathematicians themselves. The main motivation is an awareness that mathematicians regularly make serious errors, some of which go undetected. This raises the question of applying verification tools, such as Isabelle and HOL Light, which were originally built in order to verify computer systems by mechanically proving theorems in a formal calculus. But is formalised mathematics at all a realistic possibility? It turns out that a great body of mathematics has been formalised. Unfortunately, rather little of it approaches the sophistication of modern research mathematics. Moreover, formalised proofs are typically unreadable and require lengthy blocks of code to prove obvious facts. The talk will highlight recent progress using Isabelle and Lean.
Lawrence C. Paulson FRS is Director of Research at the University of Cambridge, where he has held established positions since 1983. He has written over 120 refereed conference and journal papers as well as four books. He introduced the popular Isabelle theorem proving environment in 1986, and made contributions to the verification of cryptographic protocols, the formalisation of mathematics, automated theorem proving technology, and other fields. He achieved a formal analysis of the ubiquitous TLS protocol, which is used to secure online shopping, and the formal verification of advanced mathematical results such as Gödel's second incompleteness theorem. In 2008, he introduced MetiTarski, an automatic theorem prover for real-valued functions such as logarithms and exponentials. He has supervised over 20 postgraduate students and numerous postdoctoral researchers. He has the honorary title of Distinguished Affiliated Professor from the Technical University of Munich and is an ACM Fellow and a Fellow of the Royal Society. He holds a PhD in Computer Science from Stanford University, and a BS in Mathematics from the California Institute of Technology. He has a European Research Council (ERC) Advanced Grant 2017-2023 (ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician).
COPLAS - Copenhagen Programming Language Seminar - Host: Jørgen Villadsen, AlgoLoG, DTU Compute
Introduction to Type Theory and Higher-Order Logic - Advanced Course in Logic and Computation, European Summer School in Logic, Language and Information (ESSLLI), 5-16 August 2019, Riga, Latvia.
The course prerequisites are basic knowledge of computability, first-order logic and Gödel's incompleteness theorems, but the relevant concepts, systems and theorems will be briefly covered as part of the course.
The focus is on computational logic, recently explained by Larry Paulson, Professor of Computational Logic, University of Cambridge, as "the use of computers to establish facts in a logical formalism" (PDF).
The course introduces type theory and higher-order logic, in particular the Isabelle proof assistant, which by default supports the logical formalism Isabelle/HOL based on Church’s simple type theory.
As preparation students are recommended to follow the short "getting started with Isabelle" guide (PDF) and load the following Isabelle/HOL theory file formalizing first-order logic (PDF): FOL.thy
Stable Open Access References:
[1] Introduction to Mathematical Logic / "4.6.3 The Theory of Types (ST)" (Elliott Mendelson 2015)
[2] The Seven Virtues of Simple Type Theory (William Farmer 2008)
[3] Church’s Type Theory / "1.4 A Formulation Based on Equality" (Peter Andrews 2018)
[4] Self-Formalisation of Higher-Order Logic (Ramana Kumar, Rob Arthan, Magnus Myreen & Scott Owens 2016)
[5] Higher-Order Logic (Makarius Wenzel 2019)
[6] Formal Proof (Thomas Hales 2008)
[7] Formal Proof - The Four-Color Theorem (Georges Gonthier 2008)
[8] Formal Proof - Theory and Practice (John Harrison 2008)
[9] Formal Proof - Getting Started (Freek Wiedijk 2008)
[10] A Formal Proof of the Kepler Conjecture (Thomas Hales et al. 2017)
10:00 Tobias Nipkow (Technische Universität München): Verified Analysis of Algorithms 13:00 Anders Schlichtkrull (DTU Compute): Formalization of Logic in the Isabelle Proof Assistant (PhD Defense)
Abstract of talk by Tobias Nipkow: This talk will survey the state of the art in the verification of basic algorithms from standard textbooks such as CLRS. Both functional correctness and computational complexity are considered and the formalization of the necessary mathematical basis for the latter is discussed.
Prof. Nipkow (*1958) works in the area of logic in computer science. He focuses on interactive and automatic theorem proving, programming language semantics, type systems and functional programming. His chair is developing the interactive proof assistant Isabelle. More information: https://www.professoren.tum.de/nipkow-tobias
COPLAS - Copenhagen Programming Language Seminar - Host: Jørgen Villadsen, AlgoLoG, DTU Compute
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
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
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/.
IsaFoL: Isabelle Formalization of Logic
Proof Assistants and Related Tools - The PART Projects
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
