| Programming Language Foundations in Agda | https://plfa.github.io/ |
| The Book | https://plfa.github.io/ |
| Announcements | https://plfa.github.io/Announcements/ |
| Getting Started | https://plfa.github.io/GettingStarted/ |
| Citing | https://plfa.github.io/Citing/ |
| 中文 | https://agda-zh.github.io/PLFA-zh/ |
| https://plfa.github.io/plfa.epub |
| Source | https://github.com/plfa/plfa.github.io/blob/dev/web/TableOfContents.md |
| Next | https://plfa.github.io/Dedication/ |
| GitHub | https://github.com/plfa/plfa.github.io/ |
| Dedication | https://plfa.github.io/Dedication/ |
| Preface | https://plfa.github.io/Preface/ |
| Getting Started | https://plfa.github.io/GettingStarted/ |
| Naturals | https://plfa.github.io/Naturals/ |
| Induction | https://plfa.github.io/Induction/ |
| Relations | https://plfa.github.io/Relations/ |
| Equality | https://plfa.github.io/Equality/ |
| Isomorphism | https://plfa.github.io/Isomorphism/ |
| Connectives | https://plfa.github.io/Connectives/ |
| Negation | https://plfa.github.io/Negation/ |
| Quantifiers | https://plfa.github.io/Quantifiers/ |
| Decidable | https://plfa.github.io/Decidable/ |
| Lists | https://plfa.github.io/Lists/ |
| Lambda | https://plfa.github.io/Lambda/ |
| Properties | https://plfa.github.io/Properties/ |
| DeBruijn | https://plfa.github.io/DeBruijn/ |
| More | https://plfa.github.io/More/ |
| Bisimulation | https://plfa.github.io/Bisimulation/ |
| Inference | https://plfa.github.io/Inference/ |
| Untyped | https://plfa.github.io/Untyped/ |
| Confluence | https://plfa.github.io/Confluence/ |
| BigStep | https://plfa.github.io/BigStep/ |
| Denotational | https://plfa.github.io/Denotational/ |
| Compositional | https://plfa.github.io/Compositional/ |
| Soundness | https://plfa.github.io/Soundness/ |
| Adequacy | https://plfa.github.io/Adequacy/ |
| ContextualEquivalence | https://plfa.github.io/ContextualEquivalence/ |
| Substitution | https://plfa.github.io/Substitution/ |
| Acknowledgements | https://plfa.github.io/Acknowledgements/ |
| Fonts | https://plfa.github.io/Fonts/ |
| Jeremy Siek, Indiana University | https://jsiek.github.io/PLFA-Spring-2026/ |
| Peter Thiemann, Albert-Ludwigs University | https://proglang.github.io/teaching/25ss/eopl.html |
| Joseph Eremondi, University of Regina | https://www2.cs.uregina.ca/~eremondj/ |
| Philip Wadler, University of Edinburgh | https://plfa.github.io/TSPL/2024/ |
| Peter Thiemann, Albert-Ludwigs University | https://web.archive.org/web/20240208112146/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2023ws/ |
| Philip Wadler, University of Edinburgh | https://plfa.github.io/TSPL/2023/ |
| Andrej Bauer, University of Ljubljana | https://web.archive.org/web/20220222095923/https://www.andrej.com/zapiski/ISRM-LOGRAC-2022/00-introduction.html |
| Peter Thiemann, Albert-Ludwigs University | https://web.archive.org/web/20220810154516/https://proglang.informatik.uni-freiburg.de/teaching/proglang/2022ss/ |
| Philip Wadler, University of Edinburgh | https://plfa.github.io/TSPL/2022/ |
| Prabhakar Ragde, University of Waterloo | https://web.archive.org/web/20210424214202/https://cs.uwaterloo.ca/~plragde/747/ |
| Jacques Carette, McMaster University | https://github.com/JacquesCarette/CAS706-F2021/ |
| William Cook, University of Texas | https://web.archive.org/web/20220101114527/https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf |
| Maria Emilia Maietti and Ingo Blechschmidt, Università di Padova | https://web.archive.org/web/20220810154713/https://www.math.unipd.it/~maietti/typ21.html |
| John Maraist, University of Wisconsin-La Crosse | https://web.archive.org/web/20220810155032/https://github.com/jphmrst/PLC/tree/fall2020#readme |
| Jeremy Siek, Indiana University | https://web.archive.org/web/20220421134334/https://jsiek.github.io/B522-PL-Foundations/ |
| Dan Ghica, University of Birmingham | https://web.archive.org/web/20210126123738/https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/ |
| Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup | https://meet.meetup.com/wf/click?upn=ZDzXt-2B-2BZmzYir6Bq5X7vEQ2iNYdgjN9-2FU9nWKp99AU8rZjrncUsSYODqOGn6kV-2BqW71oirCo-2Bk8O1q2FtDFhYZR-2B737CPhNWBjt58LuSRC-2BWTj61VZCHquysW8z7dVtQWxB5Sorl3chjZLDptP70L7aBZL14FTERnKJcRQdrMtc-3D_IqHN4t3hH47BvE1Cz0BakIxV4odHudhr6IVs-2Fzslmv-2FBuORsh-2FwQmOxMBdyMHsSBndQDQmt47hobqsLp-2Bm04Y9LwgV66MGyucsd0I9EgDEUB-2FjzdtSgRv-2Fxng8Pgsa3AZIEYILOhLpQ5ige5VFYTEHVN1pEqnujCHovmTxJkqAK9H-2BIL15-2FPxx97RfHcz7M30YNyqp6TOYfgTxyUHc6lufYKFA75Y7MV6MeDJMxw9-2FYUxR6CEjdoagQBmaGkBVzN |
| Prabhakar Ragde, University of Waterloo | https://web.archive.org/web/20220103155952/https://cs.uwaterloo.ca/~plragde/842/ |
| Philip Wadler, University of Edinburgh | https://plfa.github.io/20.07/TSPL/2019/ |
| Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro | https://plfa.github.io/20.07/PUC/2019/ |
| David Darais, University of Vermont | https://web.archive.org/web/20190324115921/https://david.darais.com/courses/fa2018-cs295A/ |
| Philip Wadler, University of Edinburgh | https://plfa.github.io/19.08/TSPL/2018/ |
| PLFArend | https://github.com/marat-rkh/PLFArend |
| PLFaLean | https://github.com/rami3l/PLFaLean |
| Source | https://github.com/plfa/plfa.github.io/blob/dev/web/TableOfContents.md |
| Next | https://plfa.github.io/Dedication/ |
| wadler | https://github.com/wadler |
| wenkokke | https://github.com/wenkokke |
| jsiek | https://github.com/jsiek |
| Creative Commons Attribution 4.0 International License | https://creativecommons.org/licenses/by/4.0/ |