(Programming Languages) in Agda = Programming (Languages in Agda)

on YouTube ↗45m

" summary

An executable Agda textbook implements language definitions and checks proofs as programs so examples like addition and a 20‑line proof that plus is associative actually run and typecheck, covering infinitely many cases. The project proved meta-theory for a tiny Haskell-like core and uses Agda to connect high‑level specifications to low‑level semantics. Work feeds into IOHK’s blockchain toolchain: Plutus is a Haskell library for smart contracts and a proven subset is in active development.

AI-written summary · about

" chapters (5)

1. 0:00Start
2. 3:58Functional Programming in Haskell
3. 9:49Programming Language Foundations in Agda
4. 35:08Agda for Fun and Profit: IOHK and Cardano
5. 42:10Conclusions

" related talks

• 49mAthena: A Declarative Language For Proofs In Computer ScienceSandy Vanderbleek · LambdaConf 2018
• 55mProving Theorems and Certifying Programs with CoqStephan Boyer · LambdaConf 2018
• 01h 47mAgda from Nothing: Order in the TypesScott Fleischman · LambdaConf Winter Retreat 2017
• 58mType Theory Behind the Glasgow Haskell Compiler Internals (Part 4)Vitaly Bragilevsky · LambdaConf 2018
• 57mType Theory Behind Glasgow Haskell Compiler Internals (Part 1)Vitaly Bragilevsky · LambdaConf 2018
• 01h 20mA Practical Introduction to Haskell GADTsRichard A. Eisenberg · LambdaConf 2015
• 43mPropositions as TypesPhilip Wadler · Strange Loop 2015
• 36mProgramming Languages for Automatic Differentiation: What Now?Damiano Mazza · LAFI 2022