DistriNet Seminar:
Meet the jury seminar

May 17, 2017 - Celestijnenlaan 200A, Heverlee (Leuven)

Theorems for Free, Blame for All

by Philip Wadler
Professor of Theoretical Computer Science at the University of Edinburgh, UK


Every great idea in computing will be discovered twice, once by a logician and once by an computer scientist. In 1974, John Reynolds introduced a tiny programming language – the polymorphic lambda calculus – to model data abstraction; nine years later he introduced a theory to explain how to change the representation of an abstract type without changing the behaviour of the program. But before all that, in 1972, Jean-Yves Girard introduced exactly the same tiny programming language – now called System F – for a completely different reason having to do with second-order logic. Related ideas were introduced by the logician Roger Hindley and later by the computer scientist Robin Milner, and now serve as the basis of the type system for Haskell, OCaml, and F#.
Reynolds’s theory can be viewed as a magic trick: give me the type of a function and I will tell you a theorem that it satisfies, even though I know nothing about the function's definition other than its type. The GHC Haskell compiler routinely exploits this fact to optimize operations on lists. It’s even possible to write the function in a dynamically typed language, such as JavaScript, and then impose the type later in a way that ensures it will still satisfy the corresponding theorem. We have a research version of TypeScript, called TypeScript The Next Generation, which does just that. This talk will explain the magic.


PhilipWadlerPhilip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 60, with more than 18,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O'Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.



Formal languages, coinductively formalized

By Andreas Abel
Senior Lecturer of Programming Logic at Chalmers University, Sweden


Formal languages and automata are taught to every computer science student. However, the student will most likely not see the beautiful oalgebraic foundations of formal languages and automata theory.
In this talk, I recapitulate how infinite tries can represent formal languages which are sets of strings. They allow an elegant representation of the usual language constructions like union, concatenation, and Kleene star, with the help of Brzozowski derivatives. We will then investigate how to prove the laws of the language constructions using bisimilarity and coinductive proofs.
All the definitions and proof are carried out in the foundational framework of Martin-Löf Type Theory, in particular in the implementation "Agda" of Type Theory. Agda is developed in a joint open-source project at Gothenburg, Leuven and other places of Europe.


AndresAbelAndreas Abel is Senior Lecturer of Programming Logic at Chalmers University in Sweden. Previously, he worked at INRIA in Paris, Ludwig-Maximilians-University Munich, and Carengie-Mellon University in Pittsburgh. His research interests include Verified Software Development, Dependently Typed Programming, Type Theory, Functional Programming, Termination Checking, Type Checking, Unification, Compiling Dependent Types, Theorem Proving, and Program Verification. He is one of the main developers of the Agda 2 programming language.



Practical info