On June 4th at 15h00, Philip Wadler will offer the INESC-ID Distinguished Lecture “(Programming Languages) in Agda = Programming (Languages in Agda)“. The event is supported by the BIG ERA Chair Project.
Abstract
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. Proof by induction is just programming by recursion. Finding a proof becomes as fun as hacking a program. Dependently-typed programming languages, such as Agda, exploit this pun. This talk introduces Programming Language Foundations in Agda, a textbook that doubles as an executable Agda script and also explains the role Agda plays in IOG’s Cardano cryptocurrency.
Short Bio
Philip Wadler is a Professor of Computer Science at the University of Edinburgh and a Senior Research Fellow at IOHK. He is a Fellow of the Royal Society, a Fellow of the Royal Society of Edinburgh, and an ACM Fellow. He is head of the steering committee for Proceedings of the ACM, past editor-in-chief of PACMPL and JFP, 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. According to Google Scholar, he has an h-index of over 70 with more than 25,000 citations to his work. 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.
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 100,000 views. Wadler is also an area leader for programming languages at IOHK (now Input Output Global), the blockchain engineering company developing Cardano. He has contributed to work on Plutus, a Turing-complete smart contract language for Cardano written in Haskell; the UTXO ledger system, native tokens, and System F in Agda.
Date and location
Date: June 4th, 2024
Time: 15h00-16h15
Location: Anfiteatro Abreu Faro – Complexo Interdisciplinar, Instituto Superior Técnico (Alameda)
Registration and contacts
To facilitate the organization of the event, we invite you to complete your registration here. For more information about the lecture, please contact us.