Building with Hakyll
We’re pleased to announce that as of today, PLFA builds entirely using Haskell! We’ve migrated our build system from a bundle of Makefiles, shell scripts, and Jekyll, over to Hakyll, a static site building written in Haskell. All you need to do to build and serve PLFA locally is:
git clone --recurse-submodules https://github.com/plfa/plfa.github.io PLFA cd PLFA/ stack build && stack exec site watch
That will pull in all the dependencies: Agda, the standard library, Hakyll, Pandoc, etc.
There’s been lots of changes to the organisation of PLFA as a consequence, but the most important change, if you’re using PLFA as a student, is that we now include the correct version of the Agda standard library as a Git submodule. The “Getting Started” page can help you set it up correctly!
If you’re a contributor to PLFA, there are some further changes that will affect you!(more)
Migration to Agda 2.6.1
We upgraded to Agda 2.6.1 and version 1.3 of the standard library. If you want to continue working with the latest version of the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.(more)
Versions and Releases
We’re adding stable releases to PLFA, which you can find on GitHub!(more)
Introducing Part 3: Denotational Semantics
We’re pleased to announce an entirely new part of the book, contributed by Jeremy G. Siek! You may have noticed his name appearing on the list of authors some months ago, or the chapters that make up Part 3 slowly making their appearance. Well, that’s all Jeremy’s work!(more)
Talking about PLFA…
We published a paper about PLFA at the Brazilian Symposium on Formal Methods and in the Science of Computer Programming (extended version). In them, we describe our experiences writing the book, and compare it to Software Foundations.
PLFA as EPUB
It has been just over a year and a half since this feature was first requested in #112… Thanks to hard work by Michael Reed, and a little elbow grease on our part, it is finally here! An EPUB version of PLFA!
Praise for PLFA
“Types and Semantics for Programming Languages was the single best course I took throughout my time at the University of Edinburgh. Philip Wadler clearly poured his heart into teaching it, including writing a whole textbook including exercises specifically for the course.”
“One of the most inspiring courses. Philip designed a course that is both very theoretical and very practical.”
PLFA as a Notebook
NextJournal has created a notebook version of PLFA, which lets you edit and run the code samples from the book online! The notebook is based on PLFA version 19.08, with some minor changes to adapt the contents to NextJournal.
Migration to Agda 220.127.116.11
We upgraded to Agda 18.104.22.168 and version 1.1 of the standard library. If you want to continue working with the book, you’ll have to update your versions locally. Please follow the instructions in Getting Started to reinstall Agda and the standard library.(more)