From 7eb0b313bbdf14c2ca1ab47cf33a8b0fdedaab0e Mon Sep 17 00:00:00 2001
From: "github-merge-queue[bot]"
 <github-merge-queue[bot]@users.noreply.github.com>
Date: Thu, 26 Oct 2023 12:36:30 +0000
Subject: [PATCH] =?UTF-8?q?Deploying=20to=20web=20from=20@=20plfa/plfa.git?=
 =?UTF-8?q?hub.io@29d29797d32fd9bc6909d8951f37367b603dcc8a=20=F0=9F=9A=80?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 TSPL/2023/index.html |   2 +-
 plfa.epub            | Bin 737020 -> 737021 bytes
 rss.xml              |   2 +-
 3 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/TSPL/2023/index.html b/TSPL/2023/index.html
index d496aee34..0be77c35c 100644
--- a/TSPL/2023/index.html
+++ b/TSPL/2023/index.html
@@ -1 +1 @@
-<!DOCTYPE html><html lang="en"><head><meta charset="utf-8"><meta http-equiv="X-UA-Compatible" content="IE=edge"><meta name="viewport" content="width=device-width,initial-scale=1"><link rel="stylesheet" href="../../assets/css/light.css" integrity="sha512-J8Ko83OT11zQ2/+vowqJ0Ovx2JEWUBNPTbNptixluYAHAO009R7GVxRQNKA+Wq4skbsdZr1AEOjF2AeQmKt3/A==" title="Light" id="stylesheet-light"><link rel="stylesheet" href="../../assets/css/dark.css" integrity="sha512-kK/Wf2991I8CFsf5/Qu/2GIm2Enzw8H70RQ/yHNIb6iGTPF/SKE0B+kxTG2HjcFOgcjfKxZ9Jr4bvSfuKraNWw==" title="Dark" id="stylesheet-dark" disabled><title>Programming Language Foundations in Agda – TSPL</title><script src="../../assets/js/anchor.js" integrity="sha512-Y5IMGqYQp36NYYdEL6gXISLsHNpx0LxW0NS0twvYBvXI8GH5PZa1g5gm1B5lxg6tlFyUAiOOfgKL/NIn0dtY4w==" id="script-anchor"></script><script src="../../assets/js/darkmode.js" integrity="sha512-iUX9HnSphH4WbMv88MYJEFtLfkCtTHrvWyFwjigSm5GkwHv1L31GP5grIGDo7kI2jftuYVvt4xu4qeCn2fKbww==" id="script-darkmode"></script><script src="../../assets/js/main.js" integrity="sha512-X7aZg6IUKq1TvTVjSureaMGKZ/ylbAD7kxiU2w42IUgh4lUTWoOsoIWzNvrqkwBJdQ1y2GsS67gtsv39Uuq6ew==" id="script-main"></script></head><body><header class="site-header"><div class="wrapper"><a class="site-title" href="../../">Programming Language Foundations in Agda</a><nav class="site-nav"><input type="checkbox" id="nav-trigger" class="nav-trigger"><label for="nav-trigger"><span class="menu-icon"><svg class="svg-icon grey" viewBox="0 0 18 15" width="18px" height="15px"><path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"></path><path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"></path><path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"></path></svg></span></label><div class="trigger"><a class="page-link" href="../../">The Book</a> <a class="page-link" href="../../Announcements/">Announcements</a> <a class="page-link" href="../../GettingStarted/">Getting Started</a> <a class="page-link" href="../../Citing/">Citing</a> <a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a> <a class="page-link" onclick="window.darkmode.toggle()"><i id="darkmode-trigger" class="fas fa-moon" aria-hidden="true"></i> </a><a class="page-link" href="../../plfa.epub"><i class="fa fa-book" aria-hidden="true"></i></a></div></nav></div></header><main class="page-content" aria-label="Content"><div class="wrapper"><article class="post"><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/courses/TSPL/2023/tspl.md">Source</a></li><li class="separator">•</li></ul></nav><header class="post-header"><h1 class="post-title">TSPL: Course notes</h1></header><div class="post-content"><h2 id="staff">Staff</h2><ul><li><strong>Instructor</strong> <a href="https://homepages.inf.ed.ac.uk/wadler">Philip Wadler</a></li><li><strong>Teaching assistant</strong> <a href="https://www.inf.ed.ac.uk/people/students/Tudor_Ferariu.html">Tudor Ferariu</a></li></ul><h2 id="lectures-and-tutorials">Lectures and tutorials</h2><p>Lectures take place Monday and Wednesday. Each lecture is immediately followed by a tutorial.</p><ul><li><strong>12.10–14.00</strong> <em>Monday Lecture and Tutorial</em> <a href="https://www.ed.ac.uk/maps/maps?building=0113">Old Medical School</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0113_01M_01M.473">MST Teaching Room 13 (01M.473) - Doorway 3</a></li><li><strong>12.10–14.00</strong> <em>Wednesday Lecture and Tutorial</em> <a href="https://www.ed.ac.uk/maps/maps?building=0201">Appleton Tower</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0201_02_2.12">AT 2.12</a></li><li><strong>12.10–14.00</strong> <em>Friday Lecture and Tutorial</em> <strong>(week 1 only)</strong> <a href="https://www.ed.ac.uk/maps/maps?building=0113">Old Medical School</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0113_01M_01M.473">MST Teaching Room 13 (01M.473) - Doorway 3</a></li></ul><h2 id="links">Links</h2><ul><li><a href="https://piazza.com/class/lmgbduj9sw0589">Piazza</a></li><li><a href="https://www.learn.ed.ac.uk/ultra/courses/_108407_1/outline">Learn</a></li></ul><h2 id="schedule">Schedule</h2><table><thead><tr><th scope="col">Week</th><th scope="col">Mon</th><th scope="col">Wed</th><th scope="col">Fri</th><th scope="col"></th></tr></thead><tbody><tr><td>1</td><td><strong>18 Sep</strong> <a href="../../Naturals/">Naturals</a></td><td><strong>20 Sep</strong> <a href="../../Induction/">Induction</a></td><td><strong>22 Sep</strong> <a href="../../Relations/">Relations</a></td></tr><tr><td>2</td><td><strong>25 Sep</strong></td><td><strong>28 Sep</strong></td></tr><tr><td>3</td><td><strong>2 Oct</strong> <a href="../../Equality/">Equality</a> (no class, read on your own)</td><td><strong>4 Oct</strong> <a href="../../Isomorphism/">Isomorphism</a> (no class, read on your own)</td></tr><tr><td>4</td><td><strong>9 Oct</strong> <a href="../../Connectives/">Connectives</a></td><td><strong>11 Oct</strong> <a href="../../Negation/">Negation</a></td></tr><tr><td>5</td><td><strong>16 Oct</strong> <a href="../../Quantifiers/">Quantifiers</a></td><td><strong>18 Oct</strong> <a href="../../Decidable/">Decidable</a></td></tr><tr><td>6</td><td><strong>23 Oct</strong> <a href="../../Lambda/">Lambda</a></td><td><strong>25 Oct</strong> <a href="../../Properties/">Properties</a></td></tr><tr><td>7</td><td><strong>30 Oct</strong> <a href="../../DeBruijn/">DeBruijn</a></td><td><strong>1 Nov</strong> <a href="../../More/">More</a></td></tr><tr><td>8</td><td><strong>6 Nov</strong> <a href="../../Inference/">Inference</a></td><td><strong>8 Nov</strong> <a href="../../Untyped/">Untyped</a></td></tr><tr><td>9</td><td><strong>13 Nov</strong> <a href="../../TSPL/2022/Eval/">Eval</a></td><td><strong>15 Nov</strong></td></tr><tr><td>10</td><td><strong>20 Nov</strong></td><td><strong>23 Nov</strong></td></tr><tr><td>11</td><td><strong>27 Nov</strong> <a href="https://github.com/agda/agda2hs">agda2hs</a> (guest: <a href="https://omelkonian.github.io/">Orestis Melkonian</a>)</td><td><strong>29 Nov</strong> Propositions as Types</td></tr></tbody></table><h2 id="assessment">Assessment</h2><p>Assessment for the course is as follows.</p><ul><li>five courseworks, sixteen points each, <strong>80%</strong></li><li>optional project, take a research paper and formalise its development, <strong>20%</strong></li></ul><p>In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points or less (out of 20) on the optional project. Attempting the optional project may not be a good use of time compared to other courses where there are easier marks to be had.</p><h2 id="coursework">Coursework</h2><p>For instructions on how to set up Agda for PLFA see <a href="../../GettingStarted/">Getting Started</a>.</p><ul><li><a href="../../TSPL/2023/Assignment1/">Assignment 1</a> cw1 due 12 noon Thursday 5 October (Week 3)</li><li><a href="../../TSPL/2023/Assignment2/">Assignment 2</a> cw2 due 12 noon Thursday 19 October (Week 5)</li><li>Assignment 3 cw3 due 12 noon Thursday 2 November (Week 7)</li><li>Assignment 4 cw4 due 12 noon Thursday 16 November (Week 9)</li><li>Assignment 5 cw5 due 12 noon Thursday 23 November (Week 10)</li></ul><h2 id="how-to-submit-coursework">How to submit coursework</h2><p>Go to the TSPL <a href="https://www.learn.ed.ac.uk/ultra/courses/_108407_1/outline">Learn</a> course and select “Assessment” from the left hand menu. Select the “Assignment Submission” folder and then click on the link “submit your coursework here”. This will take you to the Gradescope interface.</p><p>For anyone who has sat an online exam, Gradescope should look familiar. Gradescope programming assignments differ from exams in that it offers three options for submitting your work:</p><ul><li>Drag and drop your code file(s) into Gradescope</li><li>Submit a GitHub repository</li><li>Submit a Bitbucket repository</li></ul><p>For the last two, you need to link your account to submit from GitHub or Bitbucket if you have not already. Instructions to do so are <a href="https://help.gradescope.com/article/lcn4nfvcww-student-edit-account#linking_accounts">here</a>.</p><h2 id="optional-project">Optional project</h2><p>The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional projects that contributed to ongoing research. Talk to me about what you would like to submit.</p><ul><li>Optional project cw6 due 12 noon Thursday 1 December (Week 11)</li></ul><h2 id="additional-reading">Additional reading</h2><ul><li><p>John Reynolds, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/reynolds/three-approaches.pdf">Three Approaches to Type Structure</a>, <em>Mathematical Foundations of Software Development</em>, LNCS 185, pages 97–138, 1985.</p></li><li><p>Henk Barendregt, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf">Introduction to generalized type systems</a> <em>Journal of Functional Programming</em>, 1(2): 125–154, 1991.</p></li><li><p>Vladimir Gapayev, Michael Levin, Benjamin Pierce. <a href="https://homepages.inf.ed.ac.uk/wadler/papers/gapayev/gapayev-et-al-icfp2000.pdf">Recursive Subtyping Revealed</a>, <em>International Conference on Functional Programming</em>, 2000.</p></li></ul></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/courses/TSPL/2023/tspl.md">Source</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk"><i class="far fa-envelope"></i>  wadler@inf.ed.ac.uk</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:me@wen.works"><i class="far fa-envelope"></i>  me@wen.works</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:jsiek@indiana.edu"><i class="far fa-envelope"></i>  jsiek@indiana.edu</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
\ No newline at end of file
+<!DOCTYPE html><html lang="en"><head><meta charset="utf-8"><meta http-equiv="X-UA-Compatible" content="IE=edge"><meta name="viewport" content="width=device-width,initial-scale=1"><link rel="stylesheet" href="../../assets/css/light.css" integrity="sha512-J8Ko83OT11zQ2/+vowqJ0Ovx2JEWUBNPTbNptixluYAHAO009R7GVxRQNKA+Wq4skbsdZr1AEOjF2AeQmKt3/A==" title="Light" id="stylesheet-light"><link rel="stylesheet" href="../../assets/css/dark.css" integrity="sha512-kK/Wf2991I8CFsf5/Qu/2GIm2Enzw8H70RQ/yHNIb6iGTPF/SKE0B+kxTG2HjcFOgcjfKxZ9Jr4bvSfuKraNWw==" title="Dark" id="stylesheet-dark" disabled><title>Programming Language Foundations in Agda – TSPL</title><script src="../../assets/js/anchor.js" integrity="sha512-Y5IMGqYQp36NYYdEL6gXISLsHNpx0LxW0NS0twvYBvXI8GH5PZa1g5gm1B5lxg6tlFyUAiOOfgKL/NIn0dtY4w==" id="script-anchor"></script><script src="../../assets/js/darkmode.js" integrity="sha512-iUX9HnSphH4WbMv88MYJEFtLfkCtTHrvWyFwjigSm5GkwHv1L31GP5grIGDo7kI2jftuYVvt4xu4qeCn2fKbww==" id="script-darkmode"></script><script src="../../assets/js/main.js" integrity="sha512-X7aZg6IUKq1TvTVjSureaMGKZ/ylbAD7kxiU2w42IUgh4lUTWoOsoIWzNvrqkwBJdQ1y2GsS67gtsv39Uuq6ew==" id="script-main"></script></head><body><header class="site-header"><div class="wrapper"><a class="site-title" href="../../">Programming Language Foundations in Agda</a><nav class="site-nav"><input type="checkbox" id="nav-trigger" class="nav-trigger"><label for="nav-trigger"><span class="menu-icon"><svg class="svg-icon grey" viewBox="0 0 18 15" width="18px" height="15px"><path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"></path><path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"></path><path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"></path></svg></span></label><div class="trigger"><a class="page-link" href="../../">The Book</a> <a class="page-link" href="../../Announcements/">Announcements</a> <a class="page-link" href="../../GettingStarted/">Getting Started</a> <a class="page-link" href="../../Citing/">Citing</a> <a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a> <a class="page-link" onclick="window.darkmode.toggle()"><i id="darkmode-trigger" class="fas fa-moon" aria-hidden="true"></i> </a><a class="page-link" href="../../plfa.epub"><i class="fa fa-book" aria-hidden="true"></i></a></div></nav></div></header><main class="page-content" aria-label="Content"><div class="wrapper"><article class="post"><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/courses/TSPL/2023/tspl.md">Source</a></li><li class="separator">•</li></ul></nav><header class="post-header"><h1 class="post-title">TSPL: Course notes</h1></header><div class="post-content"><h2 id="staff">Staff</h2><ul><li><strong>Instructor</strong> <a href="https://homepages.inf.ed.ac.uk/wadler">Philip Wadler</a></li><li><strong>Teaching assistant</strong> <a href="https://www.inf.ed.ac.uk/people/students/Tudor_Ferariu.html">Tudor Ferariu</a></li></ul><h2 id="lectures-and-tutorials">Lectures and tutorials</h2><p>Lectures take place Monday and Wednesday. Each lecture is immediately followed by a tutorial.</p><ul><li><strong>12.10–14.00</strong> <em>Monday Lecture and Tutorial</em> <a href="https://www.ed.ac.uk/maps/maps?building=0113">Old Medical School</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0113_01M_01M.473">MST Teaching Room 13 (01M.473) - Doorway 3</a></li><li><strong>12.10–14.00</strong> <em>Wednesday Lecture and Tutorial</em> <a href="https://www.ed.ac.uk/maps/maps?building=0201">Appleton Tower</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0201_02_2.12">AT 2.12</a></li><li><strong>12.10–14.00</strong> <em>Friday Lecture and Tutorial</em> <strong>(week 1 only)</strong> <a href="https://www.ed.ac.uk/maps/maps?building=0113">Old Medical School</a> <a href="https://www.ed.ac.uk/timetabling-examinations/timetabling/room-bookings/bookable-rooms3/room/0113_01M_01M.473">MST Teaching Room 13 (01M.473) - Doorway 3</a></li></ul><h2 id="links">Links</h2><ul><li><a href="https://piazza.com/class/lmgbduj9sw0589">Piazza</a></li><li><a href="https://www.learn.ed.ac.uk/ultra/courses/_108407_1/outline">Learn</a></li></ul><h2 id="schedule">Schedule</h2><table><thead><tr><th scope="col">Week</th><th scope="col">Mon</th><th scope="col">Wed</th><th scope="col">Fri</th><th scope="col"></th></tr></thead><tbody><tr><td>1</td><td><strong>18 Sep</strong> <a href="../../Naturals/">Naturals</a></td><td><strong>20 Sep</strong> <a href="../../Induction/">Induction</a></td><td><strong>22 Sep</strong> <a href="../../Relations/">Relations</a></td></tr><tr><td>2</td><td><strong>25 Sep</strong></td><td><strong>28 Sep</strong></td></tr><tr><td>3</td><td><strong>2 Oct</strong> <a href="../../Equality/">Equality</a> (no class, read on your own)</td><td><strong>4 Oct</strong> <a href="../../Isomorphism/">Isomorphism</a> (no class, read on your own)</td></tr><tr><td>4</td><td><strong>9 Oct</strong> <a href="../../Connectives/">Connectives</a></td><td><strong>11 Oct</strong> <a href="../../Negation/">Negation</a> &amp; <a href="../../Quantifiers/">Quantifiers</a></td></tr><tr><td>5</td><td><strong>16 Oct</strong> <a href="../../Decidable/">Decidable</a></td><td><strong>18 Oct</strong> <a href="../../Lambda/">Lambda</a></td></tr><tr><td>6</td><td><strong>23 Oct</strong> <a href="../../Lambda/">Lambda</a> &amp; <a href="../../Properties/">Properties</a></td><td><strong>25 Oct</strong> <a href="../../Properties/">Properties</a></td></tr><tr><td>7</td><td><strong>30 Oct</strong> <a href="../../DeBruijn/">DeBruijn</a></td><td><strong>1 Nov</strong> <a href="../../More/">More</a></td></tr><tr><td>8</td><td><strong>6 Nov</strong> <a href="../../Inference/">Inference</a></td><td><strong>8 Nov</strong> <a href="../../Untyped/">Untyped</a></td></tr><tr><td>9</td><td><strong>13 Nov</strong></td><td><strong>15 Nov</strong></td></tr><tr><td>10</td><td><strong>20 Nov</strong></td><td><strong>23 Nov</strong></td></tr><tr><td>11</td><td><strong>27 Nov</strong> <a href="https://github.com/agda/agda2hs">agda2hs</a> (guest: <a href="https://omelkonian.github.io/">Orestis Melkonian</a>)</td><td><strong>29 Nov</strong> Propositions as Types</td></tr></tbody></table><h2 id="assessment">Assessment</h2><p>Assessment for the course is as follows.</p><ul><li>five courseworks, sixteen points each, <strong>80%</strong></li><li>optional project, take a research paper and formalise its development, <strong>20%</strong></li></ul><p>In order to conform with the University’s Common Marking Scheme, students may typically get only 10 points or less (out of 20) on the optional project. Attempting the optional project may not be a good use of time compared to other courses where there are easier marks to be had.</p><h2 id="coursework">Coursework</h2><p>For instructions on how to set up Agda for PLFA see <a href="../../GettingStarted/">Getting Started</a>.</p><ul><li><a href="../../TSPL/2023/Assignment1/">Assignment 1</a> cw1 due 12 noon Thursday 5 October (Week 3)</li><li><a href="../../TSPL/2023/Assignment2/">Assignment 2</a> cw2 due 12 noon Thursday 19 October (Week 5)</li><li><a href="../../TSPL/2023/Assignment3/">Assignment 3</a> cw3 due 12 noon Thursday 2 November (Week 7)</li><li>Assignment 4 cw4 due 12 noon Thursday 16 November (Week 9)</li><li>Assignment 5 cw5 due 12 noon Thursday 23 November (Week 10)</li></ul><h2 id="how-to-submit-coursework">How to submit coursework</h2><p>Go to the TSPL <a href="https://www.learn.ed.ac.uk/ultra/courses/_108407_1/outline">Learn</a> course and select “Assessment” from the left hand menu. Select the “Assignment Submission” folder and then click on the link “submit your coursework here”. This will take you to the Gradescope interface.</p><p>For anyone who has sat an online exam, Gradescope should look familiar. Gradescope programming assignments differ from exams in that it offers three options for submitting your work:</p><ul><li>Drag and drop your code file(s) into Gradescope</li><li>Submit a GitHub repository</li><li>Submit a Bitbucket repository</li></ul><p>For the last two, you need to link your account to submit from GitHub or Bitbucket if you have not already. Instructions to do so are <a href="https://help.gradescope.com/article/lcn4nfvcww-student-edit-account#linking_accounts">here</a>.</p><h2 id="optional-project">Optional project</h2><p>The optional project is to take a research paper and formalise all or part of it in Agda. In the past, some students have submitted superb optional projects that contributed to ongoing research. Talk to me about what you would like to submit.</p><ul><li>Optional project cw6 due 12 noon Thursday 1 December (Week 11)</li></ul><h2 id="additional-reading">Additional reading</h2><ul><li><p>John Reynolds, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/reynolds/three-approaches.pdf">Three Approaches to Type Structure</a>, <em>Mathematical Foundations of Software Development</em>, LNCS 185, pages 97–138, 1985.</p></li><li><p>Henk Barendregt, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/barendregt/pure-type-systems.pdf">Introduction to generalized type systems</a> <em>Journal of Functional Programming</em>, 1(2): 125–154, 1991.</p></li><li><p>Vladimir Gapayev, Michael Levin, Benjamin Pierce. <a href="https://homepages.inf.ed.ac.uk/wadler/papers/gapayev/gapayev-et-al-icfp2000.pdf">Recursive Subtyping Revealed</a>, <em>International Conference on Functional Programming</em>, 2000.</p></li></ul></div><nav class="pager"><ul class="pagination"><li><a class="pagelink" href="https://github.com/plfa/plfa.github.io/blob/dev/courses/TSPL/2023/tspl.md">Source</a></li><li class="separator">•</li></ul></nav></article></div></main><footer class="site-footer h-card"><data class="u-url" href="../../"></data><div class="wrapper"><h2 class="footer-heading">Programming Language Foundations in Agda</h2><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Philip Wadler</li><li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk"><i class="far fa-envelope"></i>  wadler@inf.ed.ac.uk</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wadler" title="wadler"><i class="fab fa-github"></i>  wadler</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Wen Kokke</li><li><a class="u-email" href="mailto:me@wen.works"><i class="far fa-envelope"></i>  me@wen.works</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/wenkokke" title="wenkokke"><i class="fab fa-github"></i>  wenkokke</a></li><li><a rel="me" href="https://twitter.com/wenkokke" title="wenkokke"><i class="fab fa-twitter"></i>  wenkokke</a></li></ul></div><div class="footer-col footer-col-3"></div></div><div class="footer-col-wrapper"><div class="footer-col footer-col-1"><ul class="contact-list"><li class="p-name">Jeremy G. Siek</li><li><a class="u-email" href="mailto:jsiek@indiana.edu"><i class="far fa-envelope"></i>  jsiek@indiana.edu</a></li></ul></div><div class="footer-col footer-col-2"><ul class="social-media-list"><li><a rel="me" href="https://github.com/jsiek" title="jsiek"><i class="fab fa-github"></i>  jsiek</a></li><li><a rel="me" href="https://twitter.com/jeremysiek" title="jeremysiek"><i class="fab fa-twitter"></i>  jeremysiek</a></li></ul></div><div class="footer-col footer-col-3"></div></div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a></div></footer></body></html>
\ No newline at end of file
diff --git a/plfa.epub b/plfa.epub
index fc2ea39b2b0a651f4c2a72d618a3fd3e165fb35c..7b8368a798a22e2d54b8fac09e1a932b400cd489 100644
GIT binary patch
delta 6102
zcmaJ_2{=^m+dgB=3^SN4!^pmbEZLV)*0QFug;2>($(pS)cG<Ud6pBb8q0}Hk3S}=M
zyDV9=7Gn5jru@F&-~YS5nRBjruKV2Y^WM+%KJRm#dAEt;M4~vo;Ylbp3jojnK%|Xj
zGQA>{^i!tu5DL9vV+kfop$Moy&uIWM@JtdlOhaOrpQ>1CNo7Nevm=9p&fm%3mi1&B
z&};m4^<!loFB21EaxgsA8hr%+Y3k$j7<2y>6+UAfA+tc`8^#rSxw{kJyUuKRGq$}m
zWh(u$DW#j4u^2Jd)^^I|{i@#QK9^?8;tS4GsiTl1qitsD$l@R|`{VD8kIEZ;Vu0c#
z8#_C*A$P5CMlF}J8yj0!RGw>GNY{;vHSIfVQmNTeeRyisR6!s$Lg9Y+W&A4Fi%4tb
zf}4Z@s3Rjh_W{k<jy&cv4_lQVHA;cl-_@lqxOpX{gQzUln){OweOSCiYo6o%H;8G0
zgkP_`1w@ClhM$xMmWY^Ev#nEOhU&AWr+wh@3X9Jpv9Wq~ohi4^1iIBL+p2BTU5;J6
zeR7hus(Nj@r1-97vO}rGgaLlqWel7yI4sxt^?IntDTe&zgB3Rl;i+R%_4bHQ7hwWl
zY^yb_9#y)3wS3I6mfSr#6g7v4ZPp)aO)ycUpB!XPE5ro|d^7D|*=%cT8xNX^7G_Iw
z!fwy_B|;Zltt|-$;a~D(cmr+&w2>M@SIV6nW*1g$1d#-uz$fll7A5>*eD_3mtK-U1
z#Jim&$g<6vrsdt@X1!EvQQTI$(XyJo>B8@qTm9o%CD%7EC;Hab^Sr5dcIv6v;Itc<
z{@QEVSj~0Dve-YqtY(W#Nj)9PHSijZGjQ@;=ljTLQ`*;LoO1b`Jq?RRrZ?u0X8y$C
zY3WGa1og0&%8VvCAIhxpw+fykLtwGr8<tF!N08FSjX{deF;tL#ly*n>OHsvpnHIHk
ze09I;r%fLfgl_Ki3%aMi<*kF)PoJH&TT1qz!S*Ay&3TPHum+{gMizBjwRy}dpMsZ6
z=#oYp4aO~#i>z&wG(y%8WzEfp46lhV+}^hB5s&J57aR&_Fi!i954FYw#%Rpmj-{D7
zz<cv|5|Yl$k6B!G>Od9$rSZmy<{vw5lM?Wk-;K`RPZG-==SXf3e_t0u%@E?!^maHq
z??lLs4u2}EPry~PbS#QWNxyskhX4-C#$T@v*%g>n*E*LYz><=<?OkN-WxF<{rd5@c
zF4gj}ucSu;r~7@P0$+N!E-5qwNO-ULej=jtiGw{?Vjf1Y56hCh6Y+uf>3vbLNh&Dp
zhFXZy@(j<!k41&Xcidmr4Gj;7c)b#BH0J28g9jCLPsk)=qr7dlUf8-e2SALHGFjfb
ze@l1q;w7TS)|;G|?f~*iHbhiv@WTiU@+HR8X1k#DbQ>>r7Vp9@HNc2?(-Ajg!y7ye
zo<4m{N8$iChD&LQXzD6)p6Xf5==b8c(^2c&OpY?b?s4@KMb(Rb+Lhv~nqD{)yViup
zkQFDS!lL<^gt#y87t7^V+$WnVt&>079w9BqhODmVS}~uKt16qBOI&Eb`j)qgiK(EQ
z_k;8iV#^119G*p%j;WORNZ;Gb&~e?K>p?QkgkuBmyUxhZAXwKZ-+sc(g3f6mI|MxC
z#iu@iq76Vtx-1M=O$e3=N*a{CQxBoOfCO)!4jUZQJQo+O;&!0Ey429~(%^{8CYQ`B
zB>!$s`N8MM4Hmi}Fi!hy59wFwgGJERj;zuak+<1PGWb{R^;#31PYwHjYzz)7-%ajK
zN_C!G!F*g)->NOVi&4el^bHt=VeNM6TP>#IQdbt&UdeCc-brK45|V8ZB6x}7TW3#S
zP~`jFR~FJwqu`0!#KHYX1&r*CAxD|>V-~51BQef!%n^GLkwe!C{DuuQUxjHvzNvLY
z+-jC|Da6M$<SC!$*^Kaxrc%rb=I2|o8C8dXq6y5+_oejod!3GX7YH;{GiXU`U4qOB
zILnEsZFaw*#TX(h55W=BJJwt3_dbez$Q3k^cC`+>_Q}-M$ZqWu^j__q_6I_O$c(u4
zX<y>7AX2M~yOUU0YD)(jr@q$QJN_tz*~__&-W4CHzN*`o_Ceq-D^_()dBA6B5adi6
z$~7x{-Swh6gjc}0)wgRPJn+_9>2X%YCpBe=cWRPP^>4BY^QY>4XQ`AbO|>x$*%_a%
z-L20oqFR)kw3uk;DZVdohWU57_|dg;&$HYm-;h64uZu)qfjm8nbKRQRGFQ+BX@zj2
zjiTCkF1nw@*R1STHqRbQOc_2w%cKj(_)25v-m=mZHA8+(5YVl7heL+^!rx`G*o!?9
z5G%W)HzEZxJ1a~&RSkD!%9xl^F4LJH>bB-IoxcYJ9x-%h-adR9lE*Y*5Zow#Wp`2f
za4+Dm#)w+<rHkosJBC}3K;|!W_-h$lpyD&cOM3v~cx2h7N6l8v8Pd8#ZmdCkho<@*
z0P9-T0F7b)t1;3sCUvW*0I_CTDfM`1CQhJjB%y~zbc~}f$i}`>R7#k+yl2HKH;dit
z>GSn(pAnUYyIWTB{M1d&g_XPFmwd9LshFABl52(9H~f0h7i9+VR_Zn*^1fOzgM_#E
z2!aeV|BAInLE-sLx8vT#mv0%if4zwAu}*k4;guzsW{zIZ-Z^cps=Ok3yGJucAk|?f
zHX2Ice$8Y4`YV6O%T=waTGqojljQCUq+3|&s%y{|m1@Fhf%r&^!Mqwenn$(Rx%3Cd
z;d=2e?n!q-$yjggcCX~znM>hj%$-eey!9r3pJZ6V9Y~0?JUhJoMB9o?Y8ex~TIHqD
z+Sf)#xIT}sw}!CdJJqe9cyELYvaahcy{I(cv^Z<GIdG_x$eFfFRUdXtvwcW3Er9<~
z?z+m;jJH`w+eA9l7TfD(BHsLDwAmc`_!@WM+mK^A2YN&Jm16BphQz>IDQ2-jkZSxD
zoo~;P){*ZfF%_KA1JCN*1U!#oD!2r%5~v8V?-tIE{z|GKA_rBO{0u{m){TAo0(!cj
zqOEciW4bwtJ2|vw<ISey`G0DQt!XC*=3)YKb!)niHAZ>E&Jn{R#_r{s?kok0mK1tX
zC&%&G__NdTd_NmS*BX-o?J$9OJKdTxWQ}y*utmf$*4X{2raN7MqFIh&WH-mZ`C@C0
z$${gTz;WH0Wn_(K-mrhfu#&NRwWd2~f#QW6#e{B-l1>ht*?9Bmc)K+Pqk=27Eo`3$
zuJ<tsiVtMW{W@=vrjf;>d0n2fBzRm6-XuEOmssD0RKowZ^C(7Ed|7W$d8yfvcOScO
zkj-m$cWR}*@`K7N_l^chto+H`p@i+BPJ-&}c+D-xPeaEQGRCULj?$L%{J4K){=4_1
zL!LsG501>Q(blLF94=<uZ;%|hX`THz`0%`x#fR$IoRJ4y^Mm~oO|`afXHWUp=)E4!
zGjab^tT@w?fnS?D1%D}o#tfJn%+{Qo`@gT2*_!|FnyYE~?@Mj<N05c~#LD+_!)0Q!
zyv4~mH3)CUsxdPxFRr>_)M^*LvGLB2{qtmgF41GPx2tOxviGJ*Lw?hIF%Rv5(UM*%
z&22KAtq-Msq!q+B!M_PQ&ikxXe!eT0IwaU}RHmxYRpVib?mY45by&WqvGrxc-}ba8
zzj4kCUuTdaR*QPA(CK?0cGU1!Lektal{xbK+|ruAtP;KI11<xtsz5GGy!N;T_CTiS
znz+S56QPE&mX;R2T<a3_qmPlh?^8dI=WyZPRW^*y2Pe%i;YD81UtzToVJr_mSJ!&1
zKnbNQ8UeZFsPX88@z|sAtj;9vGeTh>{ExA7zHjOZZlAH0V%NY*o=$L<%ZIT0mVC&T
zYbie4kR=c=Cs+HJ-TI?`dhy}hEE8nabLJm~whV=KjXr%TSu%H3y;2(-`JiInz9shg
z&PJmOsaB%Tk-d0+MSnkS`X6ON)=8^zT{ETJ7bGic+D$vZmy{2RM`vCC5W$z(7WzsS
z3u_x`3${{@s;=qe(N^)>2&$QhRO=GWg89yOT0GgkQ!zT`>JqbkO*l&8?Z`v)dTy<e
zzqzrYo%&Dp^dmaCOI#IM9uIBie$-OA@|}l_yVUr(L#}Dy`)NggW4d3f4A9E@h6R+^
zXqYV3Vb`1dCnA?6r5YP2!*V_Xt960pY(;hk30yMB`V=WXf=q*YGa<FW=~lw|<7<6x
z7Z;xtu(Vy%RFL4G<<D2~-KfCJWme?u@LQzyyBW~1N>uW$%5Mg=K{xgA6OXSp?}k+4
zcJpA{bm8^*P}EgP=81>>eB38aZ!zDkV65CR>dMTxrrFP$6UtbZ080$X3wAv$<)Y$m
z@Oza;C!s9Qf$wbPL{*(^z(TjrGif&L>bC<4$CSdaavphfz_5v_5##&j?8DO$XTm*+
z{bh0fMpMHNS$stv$qMT%SBJ$Z93Fn9n#^|f&a|e%Sz$b?H}bK3f!t%uUW@`E?MqmC
zRDWcG*Os4F#26|;OM&l9sFiR$rb6!lCPmYfQ_{b5sdK#3D5->ZGOpcQw>jcA&ag|$
z#(zi^n`Hcf#o|$2RC7?-@G1Lw?Fm*tPV~c_0(S9$SJd)JF(Lf1r&czSraR|@5(JL<
zmU9{v$JXNISBcv?eK`w9OO^FEB_yWeEam0&ud-xf_3q70q)fS_nX3*g^3CSt7LGfD
z*>r?S!mxkmDe;__U$XDtY$=Y)j7kU$g0U5T8#&?4WZgX}cM;uMMV--;x5;s~raUuz
zd2)hpAvw1kpN4Gtj6-fTrtmVkvB2-X(mrV=afKZ}b*lQ&@G@(_^v#JU>ueUbv7#f>
zcH@VoJ22(6dA%Y65oi=TB9Rlb6KfGnm262n7AK~w*kpf(+97DQ1VM|IPvq>`*6Uuj
zORJVmI@t02iPw$iDTV5fpQ^|TuNba38x3_GKeAGY%jkV|>Rw?+K7tD!pU5e{6Y7M9
z>vK5azXGzkf(MavZ;gpgN;lIdbe^T~2u~ox<rY5o9zR+7pi`$^lLv<+DpdJd>@HpM
z#|Afd0oETM-o8he=LUb}yh-KjeWGa<rs5w^5!&2^IcCuy(%B|B;q)Rvr%UwI`Qc8+
z+ZHv&?sNGI^`9Dq-zBJyWq$2to#_vZ$alc~z$?|QhZnDIslO?Ux_N8pB3s``%v7(M
z=#If^erN3mJ?D|xZb>?IMIQNCy<fGycMx4fhK4fj#;%=%0T=G@VlVzIiu8<1?hAR}
zrEtvD+pVJDAc8RT;^H~FFNx@qu;rkU(W)_>EyeB7{E?bBjqkYL*dRD{*gWnBv8^0J
z+|iH>A*_D=Nc{bVqj)@HlVb+qxofpSAXb^<wKDq?%bgIr(En|r5u_H{CjRRSJ^9bL
z&RXKK1_S_pgY^zj7J>{t$^=6GA5UQ5fd&4t#GIg$bQH{L170slvF@ZpO;jmXEH4ag
zPO(&AROv8^)rX{-K1Z?C#t|`hD3*B~WZWN3o|1U)m#~Z?0JQ&tfH?>VGeNchah!5^
zKo}T9T>3L<BNWmKrO?Il8DGGx0H8Ar`iGu^K(bm<e9og$`kWM!Lw9K7U=aXB`62$0
z!mMZ)iYTOI6Iu@h#o`e`tOQdmNile(HpRk;qr9LLt92S?qe-!{{9xjqf3N@=p(X~h
z=wFG($xjUcK*k5mNry5M#_Xxy7*IHA2uN)>g_HJk@VTKN0CWt1T~Jb7(mqgIK?;Z9
z0QLM6*Rmb70YZ@+HC?R5`5XYk#Azv#L2d;Ug3w$>CG?y!CSVkC@z0p4lhk?|6zmoQ
z>TiBz;;E<pU>qIPOJ^ugi)@jOg%l<H6}+w=m;m5(Em;W*fklJ1pNYbm^Mt!aQmpwe
z&~+c^HBvF)1Q@8GJ|x3}XBbLB^bZ}Nq8N$njWCLFUYM4OJnV(b;d4-W2o($TpOYWZ
zL>eVaeg;NMqZBEJKlfBo98@Dv@V*pEQrz(59-VR!WNxXQELjWyz&7b-CEa_UypSAf
zutpMv1!GlFbpIR`fvPenR;o}KXeNW=<|VHM%*06XDGUHgNf9#ajVAr(h3uliQE3z>
z?>{dGBo+fV0MPvhs}}=u%AgKHNgDw~%aN1{ae(4-C@DU&^M5u3X;WbSV;Ij00NSab
z_$i?#Dv`#eu7X@VFgEnRBP8dcN&&?IJ@69%`xO4t`IJe>1_T1CDgQ;(6-h|7Gz7e$
zh~lTryf#`lHDU$;IV#lqW@hq$fJ;h$X&L6(fzG73;K=;~1)CtCw)|iJm*q+RYg-{;
z^d91Il!O!tQGsX15v&sXG@E~$9k~6%pR_9HVEblQtf2y-BqtP+|JuC!Xj}?V@cmwN
z66Co;-Jsyfqkr{WBqbU;brlNUl>3X+9wQ+yy`bRGvA;-*3JF<ggMu@AX}&?`D9=K{
zdwU!l8PU5#4MI$5SwXjBC_0KRZt%9?+h70)wA?ShI*S^V6hW|p&I%|>8v`?NBo}4e
zFi=el&I)$m{=y8TqJ_FSz(8?TlrW{xlGOwUq%;8_?gZ7oV81zo*KjBS3acYJUUAz4
z09L#9ubWm8C_`dV1e#qvs`aZ80AfGT?DOTr2?x9O()5hHY+2)Quyrrv(aXXjiQxd?
z8M;5R8&U|cZZDfea?Po}M1UN7^@OpA`buu?KmV(e>%StvG*W3&go#;lvZj(KvsC-*
zNqztULhPac%G@$p-PRxiMDG>$EV;1t6KOyiQUnx#H(zKDuxkK7iu(SfJx!tkC-&4S
zMukO7lcpX1FLfJTG+_Q-0nn268PxhS4Jb^if6C4?AR}5BTF`ZGNA$pacoYf&04GPg
zFSSYzv>-3Z6-C(pHpTsc=Ae-v%U*#EldB_(9|>;b{tiUOy+76D0|1Bk_OAea0TRq1
zMMQ3qAW?=i5W$TCIb=x)sh@&XWCY8L0{dkCa@1u>$ff`ayg=gckw%#}k4}Z&A#G=A
z)P7ZTLa5XS?5tps45`M+RH*css;{JU`BLwv_K2at9I{7p2m5&1Z&3_N$}9o^IR2x9
djY*(V0}gYt8lHr~$q(d6--q-7phcb>_#X)^9NGW?

delta 6075
zcmaJ_2{=@5`#!T{EM*zH>}21^nte$`Dul8Z$u6?gFqTmE<>*H!N|Le<DnePZYq1YW
zvXc-(-^^6s_tp2m{<B=?zMgYG&-*<0`@HXU&bzlKvAZWhXMPL@X9fT&0LVsIr_f<x
zq)WNsT^RXVNqgWOf;tspZPotBg+nlHo<$Icf(0I7Q@b6u93b57g6;U4c=K_&P4WXl
z#!%eexd`{1w~rM?uU13}`6dReXrQvf&SfHkk@xDD-|(t(A>n$$?5x`gS3;h#=fLxN
z>4o`i8xrHMw|wEHp*qeI!Xa_9ct9pBI9SCcec|1mQ^8yIej$F$BPo16bdi-X9bt4n
zu1l%x4E~N@ALD(9d}Y;)1n(_oWYjHWHKTh1IH2r&RLQBIH$sBvW@1uX<Qo?wRKJf>
zZqj+fO4%+bqnCY}wkw9S#6ZoE!`;o-%)d6hT88svj9O88fV;@pyHB)lGuhM11k@bm
zLZ|PCZ|ER1XBN+O*!5Su^b{tXnpS+QkMmkxzR5A>Y+B3vS*0MYjGZV^Ti2u4_xVYc
zjda}Y(2i)n9Mj0h@@&YZiKTE`)yTU~`wkh%W5XJWF5P)<8Ky8bB?ZiUBa76PTDz=@
zE8`tyx?8sE{nys9G%Lo&7ik~xP*uM2VS5fEFdgT*G`44@#a$@wpzg7`ESc|_9Eiim
z;}9EOy@AapV-7^|tT(jkGQxYZiDNSRh}NOnFqu>A4m{R|q2;Qr(?fg(2PEPw{KWlf
zqnzY#g~ZGbDe5JSZEhs~W7Drw<TB2G_psB5^Yx@1!<KT+d1?H+TjQ<i4*jYAa<(aX
zgX+nLz8PMdirGCRI`Y*_?M1H^TUQ-!a#K!Q>LKTp_H?0U%1JE$pyovzpGxDSgZ!st
zphM-8vdPTmk_h2aRMMM$^}BbRCEU*#pO&nZ`eJfUjqbKb7ozo<vYsvjeG2FGV~61i
z<x#%Tx4o;~EIu$f+BF7B2%NKwCWz|WrVrdoE4V_`K0eC4Vw2a7#-aoG?t7(1<2+g_
zV@_F`muA!04jC_Kcj<Zx7}o7Qz2Cg5(#D^iD$-P%)=D#WznAeSpI9QRy7iS=-)Yfy
zt7Kn;3y8vLo!8I@ZtOD8ybjSC-E%=cvYga)X|!GumJ1Z{yP=kd>fcqM#i-kda~QqS
zO4(Ko4l}yczj!TCK-I5`%eUZ0qayC>-mYPl{%DZH<@7aMn;y36i*D(5;>xnARf8Qu
zk`?t2uGUQGz7;S$-PZkBi`}c!yYfr^sI`tqskX-VOj`z(B(9BJ8mUv=jd7cTwQjH7
z%Q>=6Ba}*xe#brxaaE!I*x8{w;%w;tLyRS}$e($&T1Z=PM3h#}Ga<9aW=K{7H*%%(
z*+<FEzVAaPR;0^bW?n9T-}e5bQ?B?dqtO#{1LH#&9-2dHV!N!eC<K2cV>7!|a%oaW
zF4gPZ9eV~wo{Kzc54Y3YrrN}|-)mje=zJ!%+F|^V@pi>#SI&^`xU=D9Lk1P;`OQn`
zMwQ&>mlQN+uegORKKR0_j*~GTR_?^1ve;Sr&23mS=QLa9S_Cx%Gj;`qtauCOavOM5
z@q1B60x>&7CuXtz&s%n`Gqkh-FB6fI7MU4upE-Z4Eo0cQW%o-EtCAgx1h0$7a-VIA
zRJ;itH!;4ZG#bQwdqCk69k+J$yV0GRr78{Ukgcef{USN?-$(du&phd?k!a(_p|*0%
zE?+y;j{Q=`5chon`rY=;)Q(|yo_jxL2dhFoZhLzs8Zx_CU?AVIKiIv-TR-8b{Jvd~
zXfM!PLIeNUdF`Fdu#;e*gKrfb!-ff`*Zlh?&&@?EOytJLmIa5332d#`mfMdQ`@Y4e
zgM(QvH>8IkZT*Ox3lq^{hr>Ua%TFzZ)%Z0wtQah8o!>Xu(H{GO+4pRmQ?x%QvMI1M
z-1Ou3hDt@=P_48*1FX~15fYHpv?c@w3ZT-45mLBjW{Z;kv@&jWJ{^74%!^7P79;K+
ztJ9yqn0;4Cnh6u8vMzC&7J5Gu+JN)-f0OBZ#M49mtNVfVtGCUbqm+}XVM*!6`<C&U
zH=`^3#G=`Q`K3kr`e-y#Ib}0CQ$$2;dT(e{XrG&nHG7?&ecE=!BJOVYS9O*pqYDjj
zMf)RRxVA?^nU<o1p8fbUTf{99olSYi;4Vq~q)_QZo|s%vxHN{_u)#<l87aP7#=S#q
z#hf3IF&l)fA2bXdtvkrRa@^aFquMG{j#zM_>+W%`nygs2k~b?swz`;AOE#1GH$8>e
zx%iHTAMEcj6UN!`k^z_J`s_J1<kdSJ%G=qkaFqj+{U^_gWmSHKr^Iu0Ih})8nJGG0
za0zEEYSoK-o4{T>WM<TP4BHfOu9us?8^6AQy3tPMwUKxdOZRS!>DKF<XCHjUOg46B
zW@dZ|>n~H#?ec5;>rdMvf>c>s9~<QM7q1!}6w<<{fWAyi>?x{Gn>oJ@EPtn;=R_iU
zLU97jD(}A5ZS_F<HC?p2I2#WbxQP1=2!j?~jsB+=8Q4!31ur#hUir3gZhxfUx%cXI
zkG|I&Du*@OhLlt{5uI6=r`!*`^tib+zVZUn%=KVs?5e1P>W!xiCnA8zS4S{-yBl)4
z`7fq&Iz>P53z=yr$?EyRIUc>E&hynze1-4D6{b*0SgW(fTxhPhj7{MWe5#!dQuQ@p
zueBzmL|ab3tUb#BQCe*+k~0<R`ZlN(oSn`AQCe?(V!;}jRIC3YDgxU8jl;J%;9Vn{
zp~N3Tw^Koms640eF{J|A!BjgIu9mn1Mz{lCZ`wgmi!^t&OB?i{txah~-6nZ6^qV?x
zr;E?C6?#?2CeuR(iWm;JIcz93O*upEh))T7on2jAo-i15GXGA08be(-AlC3<E{Btr
z%V_dIR$x~*ov|@r-;dY}&EZnL8#GML+JIqP&cszgR9dPCo9HA?Q1XGO_~|GezZ6ZZ
zoREmk_+DBOI)b{gDt^zHm>Q`d(sr){ryRq~4EO0`l@pe()sYlfQWX^9Yii90HlzcP
zjvJ>q_%NhU->F~5nf>4m!eM2FH~S(Y@p!G&%F`+bjSG-U0k-$}!MGR7Igru340+R@
zW3l+@!f7w2Hj^~SoV^c0^9WNJ{6Q0B!G0Fb+)W2QD2;`DG^;E3qi-_rX2c~9C$g<x
zeSDb}2GMJ*a++7Z7{2;o_C@$gk<MX9CZE%AO>ZFs%||PlGE9iz0!3kaR~SJ)-Zg_Y
zwX-hAAy5ICu9;RA+!*3lm@$x*P{gDx!NTgKf4tK!zbyRAh2*IRwx&HUx&8ty2HM>D
zdv!90#Zm*aj&-f<yS~cdT2sLxsfYG0?juwlRD@O}_O|B~!*(^Fey2K!Vs!Ady`U~m
z7gNdI_o7p&ZZdx<I{X=`rRq5DtY4~iGHbn^Q@$2dy3SOrNZZRRU!wJ8E`2PoG~FpX
zwr@c&f^MsU&a@`8fp%bQu||D<cqA=zj|eg?^m4>@^r!Re`fSXWuikUv?DXh2XzndN
z?p#V>VGpKLiA$}qzOzeT^`j(*b2&AwKo9h_m{LbpHJWTgTQ<FLwk>(OT#=3}Y=;9Q
z)&`qbtufP=IqxRja(j^Az=TcCa}K{Q#i+0PsZ8GS;TBKd56Pq%^A9>Pcnb^ZfSzo0
zd!US{*6wG-=Y!iqruS;HaHons^J@~6QYP;+nG3>sXt_iuEn0n{!%V_Q=jv{Xu!`YL
zCX+#VW=z=;yg|ZR+OefkbI849TPL6J<=zZ*VR39Kzp)&9L93#jh-n6f#X$OM{<eqX
zxVsL2dB+vavBwkHdUr)fQ1$j1F=qJ=Id|!|cOF^z>Ch)MXqz&);dp#22lNF87+bDi
z3(BU?eVPiZ2z@KIsT6|29&ou5KP<JAZO)Lw6WG3ntj2CeY<<3$QrtOprBL3nRFIV;
zkdaob568IoO*6~?^yJ>XtkvfFf_MJY?#;Z9UehajoITxEQi~7OI%Ld$66)a^F>(#L
zoRMI88h<qLb==JpC|w-v+hhHg$gBmo8!F5k;k0XdF&eb3^<{`=W4~~<ZEoPJJv$^_
zw7t&gv(3?*j}g0#e&7e6PL^fn03f~5<Ysu(G)K!@zSaHu>DQ{cx&CiQ;X&~yp~cE7
zAM<??qd!7TUMs?hX4}nm+>uj$oQB8!Z{X)@<<Ie?fm&3jXt{9E&ODt<)<@ScYv*Y#
zytAY2sUlPY*`b3^f={Gk6SKqcQ_QQoI%9r*P}*dsoAB#eUkOYqk;YrdnnP@7_>OgT
z=&`}QJQVy*6J0lRaXY-2H5{(QFlv&G{npc7##U6kkxaiYd!2_<b!gDus!+=w0Ri7U
z>uFgiVJB{<ERNF<dL}BE{_wTsgi_U@z4+n_Z_RA$PflS%nG0dX^&z#WjUcBRUs6Kv
zNU-9$<|O>>O}K_OhQ@1Em%`Pp-m}at|5G$=VxZ$GRz=s`Q?k8;-crUFRX9n%DgUl6
zcx|iduD+U;cG=+E;$<~&!jlh!jbnq-3ucbBsVDo|kaqPr{vpZ8_)MM%H%0DXOT(pk
zIi~VyNo-xp=Z2>#Clsx5!|_XSiT!6?7QMKrm#p86Rx6*INLasft{Y|P+vB?T9oiJ3
zt|PT5#-h(3MYj@ajonrY8aZ(yjCecRb?xkez>E2(89^!srpC`_aWd43)L<L0(kF$)
zrt(rX0_Um)aK7$zQu<RB9Ck4;m)=eWCfAO0j7c#PtRhEsr#3x&z8j5c(=7vWYLA+@
zr+iu_J8K=oUzYaU#=f<+E+8BzCX^X?^I3R1CJ=QBiOn3(qm7<ND~6y`LeL)T82$~+
z`&mi7dC5m)2hP%dPW}0W_p=H78wMWh1}Py0iXpfHqv!n`&rcK*-4ckR7T#3`-ps{V
zn*wb7AN<yf>#fNl&Wa(<M$gMRp34>ztrLiB7T%8xylIQEmIc_Dx11&YoVxP~?`9Jm
z*OfAgXP=2<Dn~<yXkI=U8C}>sYkf=m_Ox!O23JXhvnJBeV{$gBDO%A7_aUhXq3F}}
ztwlr8t~>gli>|h;PBZ&6Yds@#8Z{o$yV7jc;sxW0V`nF-kIaA6NSbLT>eh_z*MCr>
zu3A~im0D!2JB7FAE;VBf+=)7uKl<>AY41L`azv`{<csO^)1`VRzV)s2(g%7iWq!1m
zz0)oHXt?mrr2$W+ImPVtY*QSvTe!s_?Rxx@xNtX-F8evBQYiM)rq|Hoc-in%$I76V
z^D8mk#C!km&$XNQfBf=-gC?Hv`)&AJzTVnz=XezDn+GI!2Nx%*Tj&#0zLnx&VPRA3
zPv`vJ^fxqaFU)TJ*YjdL!kWM?jBZ8HlaN(wZjH@j7yt}Xfd>WAEMTt&8c8_Di>`&y
z-5}jwz80WQgaE)r@PHs1Lr~yBFGFCY8w8{v`T&$dfytWH50fZ?KPgZN^c;lzT2EM(
zM4y47f4=uq0soL*^yN7>-_w(ySF2vXx|%~8)ddAQX2O{XjNY(P%2@y*P6pK&#X#mv
z&5x#6UIBpJGYIhD02LFsqKHNjE<T4ozd{Kw+Xl%(P*7JFWcCaNJ^Y9qGoc`=ag<2~
zWh`+UE=(FJzj-KmEGB}(DC*wN1bc>2z7$l+z43{b;&!YW6)s3Y9kP&<M<|G+nC4pm
z1=S@}9o42F_cv5CKam9s^{N@!R+;}b<Y(MNJ`e^gN)5en3D{j90QlMu2M<CaOa$K&
z1f4G>!ipQhL5G4Gco2046!egv#xsV35Ku^yGzE3shOdQFkeCw8iE?m4uu7t`|2b5W
zC(Q9DA_zm{Gby|XE~Ic91wCe<*=D35%S^Zrih>O1VYH7ZsM!yuXiGu*uGHrrl2N6^
znlFTotUmU7WSlHXH6rMkM8!-H7@*SqInGWu%$SSf72=BUgTYAWHffLHM9Os$MxcX0
znPLAv=>bp4qUFhCFkTi-$sN2ShvtM%z`zDMG#Br`4}A~-K+gjJw7`Epg%Jd5a7PZ!
z!As7E{Dxyj0{|YX0C3<xB%m+?!2pKKp?Ubo-P}GogU=+zl0^dm%O5N}I{@k*LG!~%
zH1LiFniF>H5CAr6kSwHj2G5Z#5&{4iMzZjcJKwYB?2Sp10CDiYLum*BAe0=6?0E4A
zsT^|=@QXN_70f+?rnC`QO19b^2KOY<+!E%;errNm1y-iFl9ub<13;KJ6yX0O$rlo!
zf;?J=BG?TjQbu(!2w1E{%7`pM+!qniq$mLJ#UuVIE*1p=2ULF1{%hU*MKit$0Vfqn
ziIXQ}TY(f`1_1@N+aMTFQt?;j>WU<DCk+&|`AzgyAz5l%pkNYd1d8hmRgxv6910Ru
ze_5`QEz{00F#ESfm27$F3ImD5C=BSO`YZgBJju*+0S2NKex;kSF;-zN2mrmKf9s44
zfPpNec$DI6b(R7IjsU;}2>q+7xGWf$LW)L7jgvf&6YpW53V9yMs$H$r8D-Z7fK;u&
z9fyy>K^L`Oj$LXbN1+5bIRD$ipiZ*T_rgI*^<SKa<m4fT5NTy!F(6SMO-mVIee%W3
zge3sn(SZMz*)?7SDD6X1cV6LF`3uUVzDN!NsZ`Jc6z3F8!BH6<0Jy35cXo}l2=Ip+
z0t1dI|8nLgIm7tHkzfxG$sCLQHGb7r`H)5o0N}U&ZVRF>65RZqybO81k8dHt<G-~U
z!ICVDq9||+`%A06e>O$rumI4r3HhrOR51z^_}z$Zw+M~Wq@_V#9)GT~OOq&&k0c<a
zHn@QGW%3p>@jtYl4=6Ct6NUl9lz!EQBe$L0M-+JbciTyk+paN~3QXZbVkG~24UuP+
zzn1r62O|I+Z~QxjSuJX?fq@1CcBuanXtPRbUJC^Pj3oY_=}w=d2CIJ;@A?+sI#vPz
z*Mm@h(X4E#K|d0W(qTR1b$K2|11|oS;~gU4kkUf{P*I@%%Q4r92J|6K07VYN^`tM_
zBq?_OM-CJn8jP0z6+e#Lh@tdou;_Oq9wg7x1OpnB{+)vZxf3KL(BL&?v<P|U1rL#S
zQ>ZjLtpU#ZhgRebHiW}vH;A;)+#&rX|JZNvGU&8jm=wnR7y?PYp+NfHr2_yx^8N|@
E3sHp1TmS$7

diff --git a/rss.xml b/rss.xml
index 57cb62663..fc3ba60db 100644
--- a/rss.xml
+++ b/rss.xml
@@ -8,7 +8,7 @@
     </description>
     <language>en</language>
     <atom:link href="https://plfa.github.io//rss.xml" rel="self" type="application/rss+xml" />
-    <lastBuildDate>Tue, 24 Oct 2023 00:35:15 +0000</lastBuildDate>
+    <lastBuildDate>Thu, 26 Oct 2023 11:54:52 +0000</lastBuildDate>
         <item>
       <title>Migration to Agda 2.6.3</title>
       <link>https://plfa.github.io//2023/02/26/migration-to-agda-2-6-3/index.html</link>

Week	Mon	Wed	Fri
1	18 Sep Naturals	20 Sep Induction	22 Sep Relations
2	25 Sep	28 Sep
3	2 Oct Equality (no class, read on your own)	4 Oct Isomorphism (no class, read on your own)
4	9 Oct Connectives	11 Oct Negation
5	16 Oct Quantifiers	18 Oct Decidable
6	23 Oct Lambda	25 Oct Properties
7	30 Oct DeBruijn	1 Nov More
8	6 Nov Inference	8 Nov Untyped
9	13 Nov Eval	15 Nov
10	20 Nov	23 Nov
11	27 Nov agda2hs (guest: Orestis Melkonian)	29 Nov Propositions as Types