Formalizing "Formale Systeme"

Talk by Matthias Meißner

Location: APB room 3027
Start: 31. August 2023 at 11:00 am
End: 31. August 2023 at 12:00 pm
Event series: Research Seminar Logic and AI
iCal

Abstract: In undergraduate theoretical computer science courses, students

encounter many new concepts along with techniques to prove theorems about those with mathematical rigour. Most of those definitions and proofs are both constructive in nature and fairly self contained, since they depend on only very few mathematical facts. This makes formalising them in an automated theorem prover feasible and educational. The objective of this project was to formalize a subset of the two lectures "Formale Systeme" and "Theoretische Informatik und Logik", serving both as a reference for students and as a starting point for future formalisations.

The LEAN theorem prover and programming language is a project under active development with a large, community maintained library of mathematical definitions and theorems called "mathlib". This makes it a good fit for formalising the undergraduate computer science lectures. LEAN also incorporates interesting and convenient features, notably a Haskell inspired type class resolution, a first-class support for quotients and the ability to very easily extend the language with new notations or tactics.

While there has already been some effort to formalizing "Formale Systeme", most has been reimplemented to make the definitions easier to work with, taking special care to end up with small and reusable proofs. Overall the focus has been on regular languages, where the equivalence of DFAs, NFAs and regular grammars among each other is the major implemented result.

In this talk I will give a short introduction to LEAN and outline the definitions and theorems that have been formalized as a part of this project.

The talk will take place in a hybrid fashion, physically in the APB room 3027, and online through the link:

https://bbb.tu-dresden.de/b/pio-zwt-smp-aus