Date: June 4th
Hour: 3 p.m.
Venue: Abreu Faro Amphitheatre, Alameda campus
On June 4th, at 3 p.m., Philip Wadler will give the INESC-ID Distinguished Lecture “(Programming Languages) in Agda = Programming (Languages in Agda)“.
The event is supported by the BIG ERA Chair Project, an EU funded initiative involving Técnico, INESC-ID and ITI/LARSyS.
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.
