388 lines
14 KiB
HTML
388 lines
14 KiB
HTML
<!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">
|
||
<title>TSPL: Course notes | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="TSPL: Course notes" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/TSPL/2019/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/TSPL/2019/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/TSPL/2019/","headline":"TSPL: Course notes","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg 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 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 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"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">TSPL: Course notes</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<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 assistants</strong>
|
||
<ul>
|
||
<li><a href="mailto:wen.kokke@ed.ac.uk">Wen Kokke</a></li>
|
||
<li><a href="mailto:o.melkonian@sms.ed.ac.uk">Orestis Melkonian</a></li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="lectures">Lectures</h2>
|
||
|
||
<p>Lectures take place Monday, Wednesday, and Friday in AT 5.07.</p>
|
||
<ul>
|
||
<li><strong>10.00–10.50am</strong> Lecture</li>
|
||
<li><strong>11.10–12.00noon</strong> Tutorial</li>
|
||
</ul>
|
||
|
||
<table>
|
||
<tr>
|
||
<th>Week</th>
|
||
<th>Mon</th>
|
||
<th>Wed</th>
|
||
<th>Fri</th>
|
||
</tr>
|
||
<tr>
|
||
<td>1</td>
|
||
<td><b>16 Sep</b> <a href="/20.07/Naturals/">Naturals</a></td>
|
||
<td><b>18 Sep</b> <a href="/20.07/Induction/">Induction</a></td>
|
||
<td><b>20 Sep</b> <a href="/20.07/Relations/">Relations</a></td>
|
||
</tr>
|
||
<tr>
|
||
<td>2</td>
|
||
<td><b>23 Sep</b> (no class)</td>
|
||
<td><b>25 Sep</b> (tutorial only)</td>
|
||
<td><b>27 Sep</b> (no class)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>3</td>
|
||
<td><b>30 Sep</b> <a href="/20.07/Equality/">Equality</a> &
|
||
<a href="/20.07/Isomorphism/">Isomorphism</a></td>
|
||
<td><b>2 Oct</b> <a href="/20.07/Connectives/">Connectives</a></td>
|
||
<td><b>4 Oct</b> <a href="/20.07/Negation/">Negation</a></td>
|
||
</tr>
|
||
<tr>
|
||
<td>4</td>
|
||
<td><b>7 Oct</b> <a href="/20.07/Quantifiers/">Quantifiers</a></td>
|
||
<td><b>9 Oct</b> <a href="/20.07/Decidable/">Decidable</a></td>
|
||
<td><b>11 Oct</b> (tutorial only, 10.00–10.50)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>5</td>
|
||
<td><b>14 Oct</b> <a href="/20.07/Lists/">Lists</a></td>
|
||
<td><b>16 Oct</b> <a href="/20.07/Lambda/">Lambda</a></td>
|
||
<td><b>18 Oct</b> <a href="/20.07/Lambda/">Lambda</a> and
|
||
<a href="/20.07/Properties/">Properties</a></td>
|
||
</tr>
|
||
<tr>
|
||
<td>6</td>
|
||
<td><b>21 Oct</b> <a href="/20.07/Properties/">Properties</a></td>
|
||
<td><b>23 Oct</b> <a href="/20.07/DeBruijn/">DeBruijn</a></td>
|
||
<td><b>25 Oct</b> <a href="/20.07/More/">More</a></td>
|
||
</tr>
|
||
<tr>
|
||
<td>7</td>
|
||
<td><b>28 Oct</b> <a href="/20.07/Inference/">Inference</a></td>
|
||
<td><b>30 Oct</b> <a href="/20.07/Untyped/">Untyped</a></td>
|
||
<td><b>1 Nov</b> (no class) </td>
|
||
</tr>
|
||
<tr>
|
||
<td>8</td>
|
||
<td><b>4 Nov</b> (no class) </td>
|
||
<td><b>6 Nov</b> Blame and Coercions </td>
|
||
<td><b>8 Nov</b> (no class) </td>
|
||
</tr>
|
||
<tr>
|
||
<td>9</td>
|
||
<td><b>11 Nov</b> (no class) </td>
|
||
<td><b>13 Nov</b> Additional Reading </td>
|
||
<td><b>15 Nov</b> (no class) </td>
|
||
</tr>
|
||
<tr>
|
||
<td>10</td>
|
||
<td><b>18 Nov</b> (no class) </td>
|
||
<td><b>20 Nov</b> Propositions as Types </td>
|
||
<td><b>22 Nov</b> (no class) </td>
|
||
</tr>
|
||
<tr>
|
||
<td>11</td>
|
||
<td><b>25 Nov</b> Quantitative (Wen) </td>
|
||
<td><b>27 Nov</b> (no class) </td>
|
||
<td><b>29 Nov</b> Mock Exam </td>
|
||
</tr>
|
||
</table>
|
||
|
||
<h2 id="assessment">Assessment</h2>
|
||
|
||
<p>Assessment for the course is as follows.</p>
|
||
|
||
<ul>
|
||
<li>five courseworks, five points each, including a take-home mock exam
|
||
(the “mock mock”), <b>25%</b></li>
|
||
<li>optional project, take a research paper and formalise its development, <b>25%</b></li>
|
||
<li>mock exam, online with Agda proof assistant under exam conditions, <b>0%</b></li>
|
||
<li>final exam, online with Agda proof assistant, <b>50%</b></li>
|
||
</ul>
|
||
|
||
<p>Students are expected to get 3–5 points each (out of 5) on the
|
||
courseworks. Students who undertake the coursework and mock exam typically
|
||
get 50 points (out of 50) on the final exam. In order to conform with
|
||
the University’s Common Marking Scheme, students may typically
|
||
get only 10 points (out of 25) 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="/20.07/GettingStarted/">Getting Started</a>.</p>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/TSPL/2019/Assignment1/">Assignment 1</a> cw1 due 4pm Thursday 3 October (Week 3)</li>
|
||
<li><a href="/20.07/TSPL/2019/Assignment2/">Assignment 2</a> cw2 due 4pm Thursday 17 October (Week 5)</li>
|
||
<li><a href="/20.07/TSPL/2019/Assignment3/">Assignment 3</a> cw3 due 4pm Thursday 31 October (Week 7)</li>
|
||
<li><a href="/20.07/TSPL/2019/Assignment4/">Assignment 4</a> cw4 due 4pm Thursday 14 November (Week 9)</li>
|
||
<li>Assignment 5 cw5 due 4pm Thursday 21 November (Week 10)<br />
|
||
Use file <a href="/20.07/TSPL/2019/Exam/">Exam</a>. Despite the rubric, do <strong>all three questions</strong>.</li>
|
||
</ul>
|
||
|
||
<p>Assignments are submitted by running</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>submit tspl cwN AssignmentN.lagda.md
|
||
</code></pre></div></div>
|
||
<p>where N is the number of the assignment.</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. I suggest formalising the paper
|
||
<a href="http://homepages.inf.ed.ac.uk/wadler/topics/blame.html#coercions">here</a>,
|
||
but talk to me if you want to formalise something else.
|
||
(A more recent draft of the same paper is
|
||
<a href="http://homepages.inf.ed.ac.uk/wadler/papers/coercions-jfp/coercions-jfp.pdf">here</a>.)</p>
|
||
|
||
<ul>
|
||
<li>Optional project cw6 due 4pm Thursday 28 November (Week 11)</li>
|
||
</ul>
|
||
|
||
<p>Submit the optional project by running</p>
|
||
<div class="language-bash highlighter-rouge"><div class="highlight"><pre class="highlight"><code>submit tspl essay Essay.lagda.md
|
||
</code></pre></div></div>
|
||
|
||
<h2 id="mock-exam">Mock exam</h2>
|
||
|
||
<p>10am-12noon Friday 29 November, AT 5.05 West Lab. An online
|
||
examination with the Agda proof assistant, under DICE to let you
|
||
practice for the exam and familiarise yourself with exam conditions.</p>
|
||
|
||
<h2 id="additional-reading">Additional reading</h2>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>John Reynolds,
|
||
<a href="http://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="http://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="http://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>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></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">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></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:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></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">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></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>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|