Programming Language Foundations in Agda

https://plfa.github.io/

83 5 6 years ago

plfa.github.io

kvlr• 5 years ago

Here’s a runnable version of this book https://nextjournal.com/try/plfa/Naturals

samvher• 5 years ago

Is this in any way related to Software Foundations Volume 2: Programming Language Foundations [0] (in Coq)? The table of contents looks quite different but the choice of name suggest some commonality.

[0] https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht...

mechanicalDigit• 5 years ago

Wadler stated in a talk somewhere that he was inspired by that book, but thought Agda may be more approachable.

remexre• 5 years ago

The second paragraph of [0] says about the same, with reasons.

[0] https://plfa.github.io/Preface/#personal-remarks

amw-zero• 5 years ago

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.

Programming Language Foundations in Agda

Related Stories