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:
- Philip Wadler on Reynolds’s ‘Definitional Interpreters for Higher-Order Programming Languages’ (SkillsCast recorded in June 2016)
- Haskell Fundamentals (4-Day Course) with Alejandro Serrano (Online Course on 19th - 22nd April 2021)
- FP in Kotlin with Arrow with Jorge Castillo (Online Course on 24th - 27th May 2021)
- F# eXchange 2021 (Online Conference on 20th - 21st October 2021)
- Haskell eXchange 2021 (Online Conference on 16th - 17th November 2021)
- Theorems for Free (SkillsCast recorded in November 2020)
- Comparing Strict and Lazy (SkillsCast recorded in November 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).