Keynote: (Programming Languages) in Agda = Programming (Languages in Agda)
Please log in to watch this conference skillscast.
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. 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:
- Philip Wadler on Reynolds’s ‘Definitional Interpreters for Higher-Order Programming Languages’ (SkillsCast recorded in June 2016)
- Haskell eXchange 2020 (Online Conference on 4th - 5th November 2020)
- Type Me If You Can: Writing Safe Communication Protocols with F# (SkillsCast recorded in October 2020)
- What's in a Functional Compiler? (SkillsCast recorded in July 2020)
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).