Abstract

TALK CANCELLED

We present a novel formulation of substitution, inspired by the explicit substitutions of Abadi, Cardelli, Curien, and Levy (1991). In their formulation, substitutions are constructed with four operations and substitution is an explicit operator on terms. In our formulation, substitutions are constructed with three operations and weakening is an explicit operator on terms, while substitution becomes a meta operation. The advantage of our formulation is that facts about substitution that previously required tens or hundreds of lines justify in a proof assistant now follow immediately—-they can be justified by writing the four letters “refl”.

A paper has been written as an executable literate Agda script, and source of the paper is available as an artifact.

Joint work with Jeremy Siek and Peter Thiemann.

Bio:

Philip Wadler likes to introduce theory into practice, and practice into theory. An example of theory into practice: GJ, the basis for Java with generics, derives from quantifiers in second-order logic. An example of practice into theory: Featherweight Java specifies the core of Java in less than one page of rules. He is a principal designer of the Haskell programming language, contributing to its two main innovations, type classes and monads. The YouTube video of his Strange Loop talk Propositions as Types has over 75,000 views.

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK . He is an ACM Fellow, a Fellow of the Royal Society of Edinburgh, and editor-in-chief of Proceedings of the ACM for Programming Languages. He is past chair of ACM SIGPLAN , past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, 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 over 70 with more than 25,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O’Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.

Link to join virtually: https://zoom.us/j/98901725392?pwd=UWNVZVFTcVQxL2JkS0V1WVBoelBuUT09

This talk is being recorded.