O professor da Philip Wadler (Edinburgh University), visitará o departamento de Informática da PUC-Rio na próxima semana e ficará até a primeira semana de agosto.
Ele também irá oferecer um mini-curso no LEAN Interactive Theorem Prover. LEAN é baseado em teoria de tipos dependentes e foi desenvolvido pelo Leonardo Moura, ex-aluno de graduação, mestrado e doutorado do DI e atual principal investigator na Microsoft Research. As aulas acontecerão nos dias 15, 22 e 29 de julho e 4 de agosto (ou dia 2 de agosto, ainda a confirmar), das 14 às 16, na sala 511 RDC, dentro do departamento, e o tempo será dividido entre 1 hora de exposição e 1 hora de experimentação prática.
Conheça um pouco sobre o professor:
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 35,000 views.
Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, 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 60, with more than 20,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O’Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.
Caso for participar, pedimos para que tragam o seu notebook para participar das aulas!
Para se inscrever envie um email para hermann@inf.puc-rio.br com o assunto “LEAN”.