| Programming Language Foundations in Agda | http://plfa.inf.ed.ac.uk/ |
| The Book | http://plfa.inf.ed.ac.uk/ |
| Announcements | http://plfa.inf.ed.ac.uk/Announcements/ |
| Getting Started | http://plfa.inf.ed.ac.uk/GettingStarted/ |
| Citing | http://plfa.inf.ed.ac.uk/Citing/ |
| 中文 | https://agda-zh.github.io/PLFA-zh/ |
| http://plfa.inf.ed.ac.uk/plfa.epub |
| Source | https://github.com/plfa/plfa.github.io/blob/dev/web/TableOfContents.md |
| Next | http://plfa.inf.ed.ac.uk/Dedication/ |
| GitHub | https://github.com/plfa/plfa.github.io/ |
| Dedication | http://plfa.inf.ed.ac.uk/Dedication/ |
| Preface | http://plfa.inf.ed.ac.uk/Preface/ |
| Getting Started | http://plfa.inf.ed.ac.uk/GettingStarted/ |
| Naturals | http://plfa.inf.ed.ac.uk/Naturals/ |
| Induction | http://plfa.inf.ed.ac.uk/Induction/ |
| Relations | http://plfa.inf.ed.ac.uk/Relations/ |
| Equality | http://plfa.inf.ed.ac.uk/Equality/ |
| Isomorphism | http://plfa.inf.ed.ac.uk/Isomorphism/ |
| Connectives | http://plfa.inf.ed.ac.uk/Connectives/ |
| Negation | http://plfa.inf.ed.ac.uk/Negation/ |
| Quantifiers | http://plfa.inf.ed.ac.uk/Quantifiers/ |
| Decidable | http://plfa.inf.ed.ac.uk/Decidable/ |
| Lists | http://plfa.inf.ed.ac.uk/Lists/ |
| Lambda | http://plfa.inf.ed.ac.uk/Lambda/ |
| Properties | http://plfa.inf.ed.ac.uk/Properties/ |
| DeBruijn | http://plfa.inf.ed.ac.uk/DeBruijn/ |
| More | http://plfa.inf.ed.ac.uk/More/ |
| Bisimulation | http://plfa.inf.ed.ac.uk/Bisimulation/ |
| Inference | http://plfa.inf.ed.ac.uk/Inference/ |
| Untyped | http://plfa.inf.ed.ac.uk/Untyped/ |
| Confluence | http://plfa.inf.ed.ac.uk/Confluence/ |
| BigStep | http://plfa.inf.ed.ac.uk/BigStep/ |
| Denotational | http://plfa.inf.ed.ac.uk/Denotational/ |
| Compositional | http://plfa.inf.ed.ac.uk/Compositional/ |
| Soundness | http://plfa.inf.ed.ac.uk/Soundness/ |
| Adequacy | http://plfa.inf.ed.ac.uk/Adequacy/ |
| ContextualEquivalence | http://plfa.inf.ed.ac.uk/ContextualEquivalence/ |
| Substitution | http://plfa.inf.ed.ac.uk/Substitution/ |
| Acknowledgements | http://plfa.inf.ed.ac.uk/Acknowledgements/ |
| Fonts | http://plfa.inf.ed.ac.uk/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 | http://plfa.inf.ed.ac.uk/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 | http://plfa.inf.ed.ac.uk/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 | http://plfa.inf.ed.ac.uk/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 | http://plfa.inf.ed.ac.uk/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/ |