329 lines
15 KiB
HTML
329 lines
15 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>Table of Contents | 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="Table of Contents" />
|
||
<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/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/","headline":"Table of Contents","description":"Programming Language Foundations in Agda","name":"Programming Language Foundations in Agda","@type":"WebSite","@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">Table of Contents</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<p>This book is an introduction to programming language theory using the
|
||
proof assistant Agda.</p>
|
||
|
||
<p>Comments on all matters—organisation, material to add, material to
|
||
remove, parts that require better explanation, good exercises, errors,
|
||
and typos—are welcome. The book repository is on <a href="https://github.com/plfa/plfa.github.io/">GitHub</a>.
|
||
Pull requests are encouraged.</p>
|
||
|
||
<h2 id="front-matter">Front matter</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Dedication/">Dedication</a></li>
|
||
<li><a href="/20.07/Preface/">Preface</a></li>
|
||
</ul>
|
||
|
||
<h2 id="part-1-logical-foundations">Part 1: Logical Foundations</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Naturals/">Naturals</a>: Natural numbers</li>
|
||
<li><a href="/20.07/Induction/">Induction</a>: Proof by induction</li>
|
||
<li><a href="/20.07/Relations/">Relations</a>: Inductive definition of relations</li>
|
||
<li><a href="/20.07/Equality/">Equality</a>: Equality and equational reasoning</li>
|
||
<li><a href="/20.07/Isomorphism/">Isomorphism</a>: Isomorphism and embedding</li>
|
||
<li><a href="/20.07/Connectives/">Connectives</a>: Conjunction, disjunction, and implication</li>
|
||
<li><a href="/20.07/Negation/">Negation</a>: Negation, with intuitionistic and classical logic</li>
|
||
<li><a href="/20.07/Quantifiers/">Quantifiers</a>: Universals and existentials</li>
|
||
<li><a href="/20.07/Decidable/">Decidable</a>: Booleans and decision procedures</li>
|
||
<li><a href="/20.07/Lists/">Lists</a>: Lists and higher-order functions</li>
|
||
</ul>
|
||
|
||
<h2 id="part-2-programming-language-foundations">Part 2: Programming Language Foundations</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Lambda/">Lambda</a>: Introduction to Lambda Calculus</li>
|
||
<li><a href="/20.07/Properties/">Properties</a>: Progress and Preservation</li>
|
||
<li><a href="/20.07/DeBruijn/">DeBruijn</a>: Intrinsically-typed de Bruijn representation</li>
|
||
<li><a href="/20.07/More/">More</a>: Additional constructs of simply-typed lambda calculus</li>
|
||
<li><a href="/20.07/Bisimulation/">Bisimulation</a>: Relating reductions systems</li>
|
||
<li><a href="/20.07/Inference/">Inference</a>: Bidirectional type inference</li>
|
||
<li><a href="/20.07/Untyped/">Untyped</a>: Untyped lambda calculus with full normalisation</li>
|
||
<li><a href="/20.07/Confluence/">Confluence</a>: Confluence of untyped lambda calculus</li>
|
||
<li><a href="/20.07/BigStep/">BigStep</a>: Big-step semantics of untyped lambda calculus</li>
|
||
</ul>
|
||
|
||
<h2 id="part-3-denotational-semantics">Part 3: Denotational Semantics</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Denotational/">Denotational</a>: Denotational semantics of untyped lambda calculus</li>
|
||
<li><a href="/20.07/Compositional/">Compositional</a>: The denotational semantics is compositional</li>
|
||
<li><a href="/20.07/Soundness/">Soundness</a>: Soundness of reduction with respect to denotational semantics</li>
|
||
<li><a href="/20.07/Adequacy/">Adequacy</a>: Adequacy of denotational semantics with respect to operational semantics</li>
|
||
<li><a href="/20.07/ContextualEquivalence/">ContextualEquivalence</a>: Denotational equality implies contextual equivalence</li>
|
||
</ul>
|
||
|
||
<h2 id="appendix">Appendix</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Substitution/">Substitution</a>: Substitution in untyped lambda calculus</li>
|
||
</ul>
|
||
|
||
<h2 id="backmatter">Backmatter</h2>
|
||
|
||
<ul>
|
||
<li><a href="/20.07/Acknowledgements/">Acknowledgements</a></li>
|
||
<li><a href="/20.07/Fonts/">Fonts</a>: Test page for fonts</li>
|
||
<li><a href="/20.07/Statistics/">Statistics</a>: Line counts for each chapter</li>
|
||
</ul>
|
||
|
||
<h2 id="related">Related</h2>
|
||
|
||
<ul>
|
||
<li>Mailing lists for PLFA:
|
||
<ul>
|
||
<li><a href="http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-interest">plfa-interest@inf.ed.ac.uk</a>: <br />
|
||
A mailing list for users of the book. <br />
|
||
This is the place to ask and answer questions, or comment on the content of the book.</li>
|
||
<li><a href="http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-dev">plfa-dev@inf.ed.ac.uk</a>: <br />
|
||
A mailing list for contributors. <br />
|
||
This is the place to discuss changes and new additions to the book in excruciating detail.</li>
|
||
</ul>
|
||
</li>
|
||
<li>Courses taught from the textbook (please tell us of others):
|
||
<ul>
|
||
<li>Philip Wadler, University of Edinburgh,
|
||
<a href="/20.07/TSPL/2018/">2018</a>,
|
||
<a href="/20.07/TSPL/2019/">2019</a></li>
|
||
<li>David Darais, University of Vermont,
|
||
<a href="https://web.archive.org/web/20190324115921/http://david.darais.com/courses/fa2018-cs295A/">2018</a></li>
|
||
<li>John Leo, Google Seattle, 2018–2019</li>
|
||
<li>Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
|
||
<a href="/20.07/PUC/2019/">2019</a></li>
|
||
<li>Prabhakar Ragde, University of Waterloo,
|
||
<a href="https://cs.uwaterloo.ca/~plragde/842/">2019</a></li>
|
||
<li>Adrian King,
|
||
San Francisco Types, Theorems, and Programming Languages Meetup
|
||
<a href="http://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">2019–2020</a></li>
|
||
<li>Dan Ghica, University of Birmingham
|
||
<a href="https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/">2019</a></li>
|
||
<li>Jeremy Siek, Indiana University,
|
||
<a href="https://jsiek.github.io/B522-PL-Foundations/">2020</a></li>
|
||
<li>William Cook, University of Texas,
|
||
<a href="https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf">2020</a></li>
|
||
</ul>
|
||
</li>
|
||
<li>Shortlisted for Outstanding Course by Edinburgh University Student
|
||
Association (second place) <a href="https://www.eusa.ed.ac.uk/representation/campaigns/teachingawards2020/">2020</a>
|
||
<ul>
|
||
<li>“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.”</li>
|
||
<li>“One of the most inspiring courses. Philip designed a course
|
||
that is both very theoretical and very practical.”</li>
|
||
</ul>
|
||
</li>
|
||
<li>A paper describing the book appeared in <a href="https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf">SBMF</a> and <a href="https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scf">SCP</a>.</li>
|
||
<li><a href="https://nextjournal.com/plfa/ToC">NextJournal</a> has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.</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>
|