Programming Language Foundations in Agda(plfa.github.io)
plfa.github.io
Programming Language Foundations in Agda
https://plfa.github.io/
3 comments
[deleted]
Wadler stated in a talk somewhere that he was inspired by that book, but thought Agda may be more approachable.
The second paragraph of [0] says about the same, with reasons.
[0]: https://plfa.github.io/Preface/#personal-remarks
[0]: https://plfa.github.io/Preface/#personal-remarks
Here’s a runnable version of this book https://nextjournal.com/try/plfa/Naturals
It’s been very difficult for me to devote any time to dependent type theory and it’s associated programming languages. It seems incredibly complicated for fairly little gain, since mis-specifying programs is so common.
I’m much more fond of the TLA+ style thinking of using simple untyped set theory and model-checking to verify computations.
I’m much more fond of the TLA+ style thinking of using simple untyped set theory and model-checking to verify computations.
[0] https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht...