Athena: A Declarative Language For Proofs In Computer Science
summary
Athena is a declarative proof language (not tactic based) that you can install and run at the command line; it emphasizes declarative not tactic-based proofs, term rewriting and substitutions are primitive so unification looks different. The REPL is rough but usable, it generates free theorems for datatypes and lets you prove concrete facts about the Option Type (e.g. none ≠ some x) and experiment with certified computation at runtime.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:30Why should you care
- 1:08Athena
- 2:10Industry vs Academia
- 3:20Whos trying to do this
- 5:00Rant
- 9:00Work on Athena
- 10:45Types
- 11:54Substitutions
- 13:55Equality Chaining
- 17:10Universal Algebra
- 24:55Math
- 29:03Reverse Mathematics
- 32:10Proof
- 40:00Education
related talks
45m(Programming Languages) in Agda = Programming (Languages in Agda)
37mAeon — An AI-native programming language
18mA Verified Compiler for a Functional Tensor Language
21mAutomating equational proofs in Dirac notation
43mPropositions as Types
40mAdvances in Deep Learning for Mathematical Theorem Proving
57mPropositions as Types
01h 20mA Practical Introduction to Haskell GADTs