INESC-ID Distinguished Lecture: “(Programming Languages) in Agda = Programming (Languages in Agda)” by Professor Philip Wadler (UEdin)

INESC-ID Distinguished Lecture: “(Programming Languages) in Agda = Programming (Languages in Agda)” by Professor Philip Wadler (UEdin)

On June 4, Professor Philip Wadler will give an INESC-ID Distinguished Lecture organized in the scope of the BIG ERA Chair Project, titled “(Programming Languages) in Agda = Programming (Languages in Agda)”.

Registration: To facilitate the organisation of the event we invite you to complete your registration here.

Date: June 4, 2024
Time: 15h00-16h15
Where: Anfiteatro Abreu Faro – Complexo Interdisciplinar, Instituto Superior Técnico (Alameda)

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. 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.

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 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.

The event is finished.


INESC-ID, “Instituto de Engenharia de Sistemas e Computadores: Investigação e Desenvolvimento em Lisboa” is a Research and Development and Innovation Organization (R&D+i) in the fields of Computer Science and Electrical and Computer Engineering. INESC-ID mission is to produce added value to people and society, supporting the response of public policies to scientific, health, environmental, cultural, social, economic and political challenges. INESC-ID promotes cooperation between academia and industry by addressing research on daily life issues, such as healthcare, space, mobility, agri-food, industry 4.0, and smart grids. This high level of knowledge transfer is achieved through both competitive research projects and direct contracted research. Public and private entities have therefore access to a pool of knowledge, resources and services provided through the unique competencies available at the institution.


INESC-ID is supported by:

Join our newsletter

* indicates required

Subscriber consent

The data submitted through this form will be used exclusively for the sending of INESC-ID Newsletter, NEWS-ID, and will not, under any circumstances, be shared with third parties. If you choose to, you can easily unsubscribe from the newsletter by following the link presented in the footer. In that case, your data will be automatically deleted from our information system. If you need to update your contact information or clarify any questions related to the newsletter, please contact By submitting this form, you give permission to the use of your personal data according to the conditions above.

We use Mailchimp as our marketing platform. By clicking below to subscribe, you acknowledge that your information will be transferred to Mailchimp for processing. Learn more about Mailchimp's privacy practices here.

© 2024, INESC-ID. All rights reserved