Agda Alive
The proof assistant that's also a language — Curry-Howard as daily practice in the Swedish functional tradition.
1960198020002020
Created by Ulf Norell
Ulf Norell's Agda (1999/2007) — a dependently-typed proof assistant and language — is where you write programs that are also proofs, with the Curry-Howard correspondence as the operating principle.\n\nIt is the Haskell-adjacent formal methods language; the cubical Agda extension is its research frontier.