Keynote: (Programming Languages) in Agda = Programming (Languages in Agda)
Please log in to watch this conference skillscast.
The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion. Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces Programming Language Foundations in Agda, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.
The textbook can be found here.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Gold
Silver
Bronze
Keynote: (Programming Languages) in Agda = Programming (Languages in Agda)
Philip Wadler
Philip Wadler has contributed to the designs of Haskell, Java, and XQuery, and is a co-author of XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O'Reilly, 2006).