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:
- (Programming Languages) in Agda = Programming (Languages in Agda) (SkillsCast recorded in May 2019)
- FP in Kotlin with Arrow with Jorge Castillo (Online Course on 20th - 23rd September 2021)
- F# eXchange 2021 (Online Conference on 20th October 2021)
- ScalaCon 2021: November Edition (Online Conference on 2nd - 5th November 2021)
- In The Belly Of The Whale: Tales From Haskell In The Enterprise (SkillsCast recorded in May 2021)
- Testing smart contracts with QuickCheck (SkillsCast recorded in May 2021)
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).