Migration to Agda 2.7.0

We upgraded to Agda 2.7.0 and version 2.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.

In the past, we maintained compatibility with versions of Agda all the way back to Agda 2.6.1.3 and version 1.6 of the standard library. However, version 2.0 of the standard library broke backwards compatibility with earlier versions of the standard library. Consequently, starting with today’s version of PLFA, the oldest supported versions of Agda and its standard library are Agda 2.6.4.3 and version 2.0 of the standard library.

Migration to Agda 2.6.3

We upgraded to Agda 2.6.3 and version 1.7.2 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.

Release Notes v22.08

We are pleased to announce the release of v22.08 of Programming Language Foundations in Agda.

The release will be permanently available at:

Changes:

  • We have migrated to Agda v2.6.2.2 with standard library v1.7.1.
  • Our contributors have contributed numerous fixes to the text.
  • Support for dark mode was added by Wen Kokke. To activate click the moon in the header or add ?dark=true to the URL.

We are grateful to the many individuals who have made contributions, which have improved the book significantly.

PLFA as PDF and EPUB

We’re pleased to announce that PLFA is now available as both a PDF and an EPUB! Thanks to hard work by Yuanting Mao, who did an internship with Phil at the University of Edinburgh, and a little elbow grease on our part, we’re finally compiling to PDF!

In a double whammy, we’ve recently fixed compilation to EPUB as well! Compilation to EPUB never quite survived the move to Hakyll, and the EPUB available on the website was broken for quite a while. Fortunately, we’ve fixed the EPUB compilation, based on Yuanting Mao work on PDF compilation and Michael Reed’s original work on EPUB compilation.

(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)

Release Notes v20.07

We are pleased to announce the release of v20.07 of Programming Language Foundations in Agda.

The release will be permanently available at:

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, the course we teach in Edinburgh, was shortlisted as an Outstanding Course by the Edinburgh University Student Association (Runner Up)!

“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.

Release Notes v19.08

We are pleased to announce the release of v19.08 of Programming Language Foundations in Agda.

The release will be permanently available at:

Migration to Agda 2.6.0.1

We upgraded to Agda 2.6.0.1 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)