Data: 4 de junho
Hora: 15h
Local: Anfiteatro Abreu Faro, campus Alameda
«No dia 4 de Junho, às 15h00, Philip Wadler irá apresentar a INESC-ID Distinguished Lecture “(Programming Languages) in Agda = Programming (Languages in Agda)“.
Este evento é apoiado pelo Projeto BIG ERA Chair, uma iniciativa financiada pela União Europeia, tendo como parceiros o Instituto Superior Técnico, o INESC-ID e o ITI/LARSyS.
Resumo:
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.»
