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)
- The Serverless We Need (in Perth on 21st September 2022)
- F# eXchange 2022: Online (Online Conference on 25th - 26th October 2022)
- Haskell eXchange 2022: Novice Track (Online Conference on 7th December 2022)
- Haskell: Why and How the External STG Interpreter is Useful (SkillsCast recorded in December 2021)
- Keynote — Haskell: What To Do When Success Can't Be Avoided (SkillsCast recorded in November 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).