updated index with Ghica course
This commit is contained in:
wadler
commit
36ef980840
16 changed files with 349 additions and 129 deletions
5
.gitignore
vendored
5
.gitignore
vendored
|
|
@ -21,5 +21,8 @@ Gemfile.lock
|
|||
*.spl
|
||||
*.synctex.gz
|
||||
|
||||
## EPUB files
|
||||
*.epub
|
||||
|
||||
## Emacs files
|
||||
auto/
|
||||
auto/
|
||||
|
|
|
|||
|
|
@ -39,6 +39,7 @@ script:
|
|||
- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
|
||||
- agda --version
|
||||
- acknowledgements --version
|
||||
- pandoc --version
|
||||
- make test-offline # disable to only build cache
|
||||
|
||||
before_deploy:
|
||||
|
|
|
|||
49
Makefile
49
Makefile
|
|
@ -1,6 +1,7 @@
|
|||
SHELL := /usr/bin/env bash
|
||||
AGDA := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.lagda.md')
|
||||
AGDAI := $(shell find . -type f -and \( -path '*/src/*' -or -path '*/courses/*' \) -and -name '*.agdai')
|
||||
LUA := $(shell find . -type f -and -path '*/epub/*' -and -name '*.lua')
|
||||
MARKDOWN := $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(AGDA))))
|
||||
PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
|
||||
|
||||
|
|
@ -12,7 +13,7 @@ endif
|
|||
|
||||
|
||||
# Build PLFA and test hyperlinks
|
||||
test: build
|
||||
test: build epub
|
||||
ruby -S bundle exec htmlproofer '_site'
|
||||
|
||||
|
||||
|
|
@ -35,6 +36,42 @@ statistics:
|
|||
out/:
|
||||
mkdir -p out/
|
||||
|
||||
# EPUB generation notes
|
||||
#
|
||||
# - The "Apple Books" app on Mac does not show syntax highlighting.
|
||||
# The Thorium app on Mac, however, does.
|
||||
#
|
||||
# - Regarding --epub-chapter-level, from the docs (https://pandoc.org/MANUAL.html):
|
||||
#
|
||||
# "Specify the heading level at which to split the EPUB into separate “chapter”
|
||||
# files. The default is to split into chapters at level-1 headings. This option
|
||||
# only affects the internal composition of the EPUB, not the way chapters and
|
||||
# sections are displayed to users. Some readers may be slow if the chapter
|
||||
# files are too large, so for large documents with few level-1 headings, one
|
||||
# might want to use a chapter level of 2 or 3."
|
||||
#
|
||||
#TODO: embedded fonts not working (path problem?)
|
||||
|
||||
epub: out/plfa.epub
|
||||
|
||||
out/plfa.epub: out/ $(AGDA) $(LUA) epub/main.css
|
||||
pandoc --strip-comments \
|
||||
--css=epub/main.css \
|
||||
--epub-embed-font='assets/fonts/mononoki.woff' \
|
||||
--epub-embed-font='assets/fonts/FreeMono.woff' \
|
||||
--epub-embed-font='assets/fonts/DejaVuSansMono.woff' \
|
||||
--lua-filter epub/include-files.lua \
|
||||
--lua-filter epub/rewrite-links.lua \
|
||||
--lua-filter epub/default-code-class.lua -M default-code-class=agda \
|
||||
--standalone \
|
||||
--fail-if-warnings \
|
||||
--toc --toc-depth=2 \
|
||||
--epub-chapter-level=2 \
|
||||
-o "$@" \
|
||||
epub/index.md
|
||||
|
||||
|
||||
|
||||
|
||||
# Convert literal Agda to Markdown
|
||||
define AGDA_template
|
||||
|
|
@ -120,7 +157,8 @@ travis-setup:\
|
|||
$(HOME)/.local/bin/acknowledgements\
|
||||
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
|
||||
$(HOME)/.agda/defaults\
|
||||
$(HOME)/.agda/libraries
|
||||
$(HOME)/.agda/libraries\
|
||||
/usr/bin/pandoc
|
||||
|
||||
.phony: travis-setup
|
||||
|
||||
|
|
@ -133,6 +171,11 @@ $(HOME)/.local/bin/acknowledgements:
|
|||
cd $(HOME)/acknowledgements-master;\
|
||||
stack install
|
||||
|
||||
# The version of pandoc on Xenial is too old.
|
||||
/usr/bin/pandoc:
|
||||
curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $(HOME)/pandoc.deb
|
||||
sudo dpkg -i $(HOME)/pandoc.deb
|
||||
|
||||
travis-uninstall-acknowledgements:
|
||||
rm -rf $(HOME)/acknowledgements-master/
|
||||
rm $(HOME)/.local/bin/acknowledgements
|
||||
|
|
@ -185,4 +228,4 @@ travis-uninstall-agda-stdlib:
|
|||
|
||||
travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-stdlib
|
||||
|
||||
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib
|
||||
.phony: travis-install-agda-stdlib travis-uninstall-agda-stdlib travis-reinstall-agda-stdlib epub
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ authors:
|
|||
corresponding: true
|
||||
github_username: wenkokke
|
||||
twitter_username: wenkokke
|
||||
- name: Jeremy Siek
|
||||
- name: Jeremy G. Siek
|
||||
email: jsiek@indiana.edu
|
||||
corresponding: true
|
||||
github_username: jsiek
|
||||
|
|
|
|||
97
beta.md
97
beta.md
|
|
@ -1,97 +0,0 @@
|
|||
---
|
||||
title : Table of Contents (Beta)
|
||||
layout : page
|
||||
permalink : /beta/
|
||||
---
|
||||
|
||||
This book is an introduction to programming language theory using the
|
||||
proof assistant Agda.
|
||||
|
||||
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 [GitHub].
|
||||
Pull requests are encouraged.
|
||||
|
||||
## Front matter
|
||||
|
||||
- [Dedication]({{ site.baseurl }}/Dedication/)
|
||||
- [Preface]({{ site.baseurl }}/Preface/)
|
||||
|
||||
## Part 1: Logical Foundations
|
||||
|
||||
- [Naturals]({{ site.baseurl }}/Naturals/): Natural numbers
|
||||
- [Induction]({{ site.baseurl }}/Induction/): Proof by induction
|
||||
- [Relations]({{ site.baseurl }}/Relations/): Inductive definition of relations
|
||||
- [Equality]({{ site.baseurl }}/Equality/): Equality and equational reasoning
|
||||
- [Isomorphism]({{ site.baseurl }}/Isomorphism/): Isomorphism and embedding
|
||||
- [Connectives]({{ site.baseurl }}/Connectives/): Conjunction, disjunction, and implication
|
||||
- [Negation]({{ site.baseurl }}/Negation/): Negation, with intuitionistic and classical logic
|
||||
- [Quantifiers]({{ site.baseurl }}/Quantifiers/): Universals and existentials
|
||||
- [Decidable]({{ site.baseurl }}/Decidable/): Booleans and decision procedures
|
||||
- [Lists]({{ site.baseurl }}/Lists/): Lists and higher-order functions
|
||||
|
||||
## Part 2: Operational Semantics
|
||||
|
||||
- [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
|
||||
- [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
|
||||
- [DeBruijn]({{ site.baseurl }}/DeBruijn/): Intrinsically-typed de Bruijn representation
|
||||
- [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
|
||||
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
|
||||
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
|
||||
- [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
|
||||
- [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus 🚧
|
||||
- [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus 🚧
|
||||
|
||||
## Part 3: Denotational Semantics
|
||||
|
||||
- [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus 🚧
|
||||
- [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional 🚧
|
||||
- [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics 🚧
|
||||
- [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics 🚧
|
||||
- [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence 🚧
|
||||
|
||||
## Appendix
|
||||
|
||||
- [Substitution]({{ site.baseurl }}/Substitution/): Substitution in untyped lambda calculus
|
||||
|
||||
## Backmatter
|
||||
|
||||
- [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
|
||||
- [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts
|
||||
- [Statistics]({{ site.baseurl }}/Statistics/): Line counts for each chapter
|
||||
|
||||
## Related
|
||||
|
||||
- Mailing lists for PLFA:
|
||||
* [plfa-interest@inf.ed.ac.uk](http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-interest): <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.
|
||||
* [plfa-dev@inf.ed.ac.uk](http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-dev): <br />
|
||||
A mailing list for contributors. <br />
|
||||
This is the place to discuss changes and new additions to the book in excruciating detail.
|
||||
- Courses taught from the textbook:
|
||||
* Philip Wadler, University of Edinburgh,
|
||||
[2018]({{ site.baseurl }}/TSPL/2018/),
|
||||
[2019]({{ site.baseurl }}/TSPL/2019/)
|
||||
* David Darais, University of Vermont,
|
||||
[2018][UVM-CS-295A-2018]
|
||||
* John Leo, Google Seattle, 2018--2019
|
||||
* Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
|
||||
[2019]({{ site.baseurl }}/PUC/2019/)
|
||||
* Prabhakar Ragde, University of Waterloo,
|
||||
[2019][UW-CS-842-2019]
|
||||
* Adrian King,
|
||||
San Francisco Types, Theorems, and Programming Languages Meetup
|
||||
[2019--2020][SFPL-Meetup-2020]
|
||||
* Jeremy Siek, Indiana University,
|
||||
[2020][IU-B522-2020]
|
||||
- A paper describing the book appeared in [SBMF][SMBF].
|
||||
- [NextJournal][NextJournal] has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.
|
||||
|
||||
[GitHub]: https://github.com/plfa/plfa.github.io/
|
||||
[SMBF]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
||||
[NextJournal]: https://nextjournal.com/plfa/ToC
|
||||
[UVM-CS-295A-2018]: https://web.archive.org/web/20190324115921/http://david.darais.com/courses/fa2018-cs295A/
|
||||
[IU-B522-2020]: https://jsiek.github.io/B522-PL-Foundations/
|
||||
[SFPL-Meetup-2020]: 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
|
||||
[UW-CS-842-2019]: https://cs.uwaterloo.ca/~plragde/842/
|
||||
26
epub/default-code-class.lua
Normal file
26
epub/default-code-class.lua
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
-- Source:
|
||||
-- https://github.com/jgm/pandoc/issues/2104#issuecomment-595878750
|
||||
--
|
||||
-- Assign a code class to all code blocks lacking one. Unlike the
|
||||
-- command-line flag "--indented-code-classes", which only applies
|
||||
-- to indented code blocks, this lua filter applies to all inline
|
||||
-- code elements, including fenced code blocks.
|
||||
|
||||
local default_code_classes = {}
|
||||
|
||||
function add_default_code_class(el)
|
||||
if #(el.classes) == 0 then
|
||||
el.classes = default_code_classes
|
||||
return el
|
||||
end
|
||||
end
|
||||
|
||||
function get_default_code_class(meta)
|
||||
if meta['default-code-class'] then
|
||||
default_code_classes = {pandoc.utils.stringify(meta['default-code-class'])}
|
||||
end
|
||||
end
|
||||
|
||||
return {{Meta = get_default_code_class},
|
||||
{Code = add_default_code_class},
|
||||
{CodeBlock = add_default_code_class}}
|
||||
61
epub/include-files.lua
Normal file
61
epub/include-files.lua
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
--- include-files.lua – filter to include Markdown files
|
||||
---
|
||||
--- Copyright: © 2019–2020 Albert Krewinkel
|
||||
--- Copyright: © 2020 Michael Reed
|
||||
--- License: MIT – see LICENSE file for details
|
||||
---
|
||||
--- Created by Albert Krewinkel. Slightly modified by Michael Reed for use in
|
||||
--- generating the EPUB for "Programming Language Foundations in Agda".
|
||||
---
|
||||
--- For documentation, see: https://github.com/pandoc/lua-filters/tree/master/include-files
|
||||
|
||||
-- pandoc's List type
|
||||
local List = require 'pandoc.List'
|
||||
|
||||
--- Shift headings in block list by given number
|
||||
function shift_headings(blocks, shift_by)
|
||||
if not shift_by then
|
||||
return blocks
|
||||
end
|
||||
|
||||
local shift_headings_filter = {
|
||||
Header = function (header)
|
||||
header.level = header.level + shift_by
|
||||
return header
|
||||
end
|
||||
}
|
||||
|
||||
return pandoc.walk_block(pandoc.Div(blocks), shift_headings_filter).content
|
||||
end
|
||||
|
||||
--- Filter function for code blocks
|
||||
function CodeBlock(cb)
|
||||
-- ignore code blocks which are not of class "include".
|
||||
if not cb.classes:includes 'include' then
|
||||
return
|
||||
end
|
||||
|
||||
-- Markdown is used if this is nil.
|
||||
local format = cb.attributes['format']
|
||||
local shift_heading_level_by =
|
||||
tonumber(cb.attributes['shift-heading-level-by'])
|
||||
|
||||
|
||||
local blocks = List:new()
|
||||
for line in cb.text:gmatch('[^\n]+') do
|
||||
if line:sub(1,2) ~= '//' then
|
||||
-- Read in the document at the file path specified by `line`.
|
||||
local fh = io.open(line)
|
||||
local document = pandoc.read(fh:read '*a', format)
|
||||
-- Before shifting headings, add a title heading at the beginning of the chapter.
|
||||
local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title)))
|
||||
document.blocks:insert(1, heading)
|
||||
-- Shift all headings by the user-specified amount, which is 0 by default.
|
||||
local chapter = shift_headings(document.blocks, shift_heading_level_by)
|
||||
-- Concatenate the chapter blocks (discarding the metadata) to the current document.
|
||||
blocks:extend(chapter)
|
||||
fh:close()
|
||||
end
|
||||
end
|
||||
return blocks
|
||||
end
|
||||
73
epub/index.md
Normal file
73
epub/index.md
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
---
|
||||
title: Programming Language Foundations in Agda
|
||||
author:
|
||||
- Philip Wadler
|
||||
- Wen Kokke
|
||||
- Jeremy G. Siek
|
||||
description: This book is an introduction to programming language theory using the proof assistant Agda.
|
||||
rights: Creative Commons Attribution 4.0 International License
|
||||
language: en-US
|
||||
---
|
||||
|
||||
# Front matter
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/dedication.md
|
||||
src/plfa/preface.md
|
||||
```
|
||||
|
||||
# Part 1: Logical Foundations
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/part1/Naturals.lagda.md
|
||||
src/plfa/part1/Induction.lagda.md
|
||||
src/plfa/part1/Relations.lagda.md
|
||||
src/plfa/part1/Equality.lagda.md
|
||||
src/plfa/part1/Isomorphism.lagda.md
|
||||
src/plfa/part1/Connectives.lagda.md
|
||||
src/plfa/part1/Negation.lagda.md
|
||||
src/plfa/part1/Quantifiers.lagda.md
|
||||
src/plfa/part1/Decidable.lagda.md
|
||||
src/plfa/part1/Lists.lagda.md
|
||||
```
|
||||
|
||||
# Part 2: Operational Semantics
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/part2/Lambda.lagda.md
|
||||
src/plfa/part2/Properties.lagda.md
|
||||
src/plfa/part2/DeBruijn.lagda.md
|
||||
src/plfa/part2/More.lagda.md
|
||||
src/plfa/part2/Bisimulation.lagda.md
|
||||
src/plfa/part2/Inference.lagda.md
|
||||
src/plfa/part2/Untyped.lagda.md
|
||||
src/plfa/part2/Confluence.lagda.md
|
||||
src/plfa/part2/BigStep.lagda.md
|
||||
```
|
||||
|
||||
# Part 3: Denotational Semantics
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/part3/Denotational.lagda.md
|
||||
src/plfa/part3/Compositional.lagda.md
|
||||
src/plfa/part3/Soundness.lagda.md
|
||||
src/plfa/part3/Adequacy.lagda.md
|
||||
src/plfa/part3/ContextualEquivalence.lagda.md
|
||||
```
|
||||
|
||||
# Appendix
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/part2/Substitution.lagda.md
|
||||
```
|
||||
|
||||
|
||||
# Backmatter
|
||||
|
||||
``` {.include shift-heading-level-by=1}
|
||||
src/plfa/acknowledgements.md
|
||||
src/plfa/Fonts.lagda.md
|
||||
src/plfa/statistics.md
|
||||
```
|
||||
|
||||
<!-- TODO: include the rest of the stuff on https://plfa.github.io/ -->
|
||||
42
epub/main.css
Normal file
42
epub/main.css
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
/* This is Pandoc's default ebook CSS, modified slightly. */
|
||||
/* https://github.com/jgm/pandoc/blob/master/data/epub.css */
|
||||
@font-face {
|
||||
font-family: 'mononoki';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/mononoki.woff');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'FreeMono';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/FreeMono.woff');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'DejaVuSansMono';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/DejaVuSansMono.woff');
|
||||
}
|
||||
body { margin: 5%; text-align: justify; font-size: medium; }
|
||||
code { font-family: 'mononoki', 'FreeMono', 'DejaVuSansMono', monospace; }
|
||||
h1, h2, h3, h4, h5, h6 { text-align: left; }
|
||||
nav#toc ol, nav#landmarks ol { padding: 0; margin-left: 1em; }
|
||||
nav#toc ol li, nav#landmarks ol li { list-style-type: none; margin: 0; padding: 0; }
|
||||
a.footnote-ref { vertical-align: super; }
|
||||
em, em em em, em em em em em { font-style: italic;}
|
||||
em em, em em em em { font-style: normal; }
|
||||
code{ white-space: pre-wrap; }
|
||||
span.smallcaps{ font-variant: small-caps; }
|
||||
span.underline{ text-decoration: underline; }
|
||||
q { quotes: "“" "”" "‘" "’"; }
|
||||
div.column{ display: inline-block; vertical-align: top; width: 50%; }
|
||||
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
|
||||
|
||||
/* Workaround for iBooks issue; see #6242 */
|
||||
@media screen {
|
||||
.sourceCode {
|
||||
overflow: visible !important;
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
}
|
||||
43
epub/rewrite-links.lua
Normal file
43
epub/rewrite-links.lua
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
local currentChapter = nil
|
||||
|
||||
-- Reassigns identifiers for all all Headers level 2 and higher. Level 2 Headers
|
||||
-- correspond to chapters, and are identified by the first word in their content
|
||||
-- field. Headers of level more than 2 are identified by "#<chapter>-<anchor>",
|
||||
-- where "<chapter>" is the identifier of the chapter this header is nested in,
|
||||
-- and "<anchor>" is this Header's existing identifier.
|
||||
function Header (el)
|
||||
if el.level == 2 then
|
||||
local title = pandoc.utils.stringify(el.content[1])
|
||||
currentChapter = title:match("%w+")
|
||||
el.identifier = currentChapter
|
||||
elseif el.level > 2 then
|
||||
el.identifier = currentChapter .. '-' .. el.identifier
|
||||
end
|
||||
return el
|
||||
end
|
||||
|
||||
|
||||
|
||||
-- Performs the following transformations on Link targets:
|
||||
--
|
||||
-- Case 1:
|
||||
-- [text]({{ site.baseurl }}/chapter/#more-stuff) -> [text](#chapter-more-stuff)
|
||||
--
|
||||
-- Case 2:
|
||||
-- [text]({{ site.baseurl }}/chapter/) -> [text](#chapter)
|
||||
--
|
||||
-- All other Links are ignored.
|
||||
function Link (el)
|
||||
local n
|
||||
-- When parsing a markdown link such as "[stuff]({{ site.baseurl }}/Naturals",
|
||||
-- pandoc encodes the link's URL with percent-encoding, resulting in the
|
||||
-- link "[stuff](%7B%7B%20site.baseurl%20%7D%7D/Naturals)".
|
||||
local baseurl = "%%7B%%7B%%20site%.baseurl%%20%%7D%%7D"
|
||||
el.target, n = el.target:gsub("^" .. baseurl .. "/(%w+)/#([%w-]+)$", -- case 1
|
||||
"#%1-%2")
|
||||
if n == 0 then
|
||||
el.target = el.target:gsub("^" .. baseurl .. "/(%w+)/$", -- case 2
|
||||
"#%1")
|
||||
end
|
||||
return el
|
||||
end
|
||||
25
index.md
25
index.md
|
|
@ -38,6 +38,21 @@ Pull requests are encouraged.
|
|||
- [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
|
||||
- [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
|
||||
- [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
|
||||
- [Confluence]({{ site.baseurl }}/Confluence/): Confluence of untyped lambda calculus 🚧
|
||||
- [BigStep]({{ site.baseurl }}/BigStep/): Big-step semantics of untyped lambda calculus 🚧
|
||||
|
||||
## Part 3: Denotational Semantics
|
||||
|
||||
- [Denotational]({{ site.baseurl }}/Denotational/): Denotational semantics of untyped lambda calculus 🚧
|
||||
- [Compositional]({{ site.baseurl }}/Compositional/): The denotational semantics is compositional 🚧
|
||||
- [Soundness]({{ site.baseurl }}/Soundness/): Soundness of reduction with respect to denotational semantics 🚧
|
||||
- [Adequacy]({{ site.baseurl }}/Adequacy/): Adequacy of denotational semantics with respect to operational semantics 🚧
|
||||
- [ContextualEquivalence]({{ site.baseurl }}/ContextualEquivalence/): Denotational equality implies contextual equivalence 🚧
|
||||
|
||||
## Appendix
|
||||
|
||||
- [Substitution]({{ site.baseurl }}/Substitution/): Substitution in untyped lambda calculus
|
||||
|
||||
|
||||
## Backmatter
|
||||
|
||||
|
|
@ -86,16 +101,16 @@ Pull requests are encouraged.
|
|||
- A paper describing the book appeared in [SBMF][SBMF] and [SCP][SCP].
|
||||
- [NextJournal][NextJournal] has built a notebook version of PLFA, which lets you edit and execute the book via a web interface.
|
||||
|
||||
[BHAM-2019]: https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/
|
||||
[GitHub]: https://github.com/plfa/plfa.github.io/
|
||||
[SBMF]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
||||
[SCP]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scp
|
||||
[NextJournal]: https://nextjournal.com/plfa/ToC
|
||||
[UVM-2018]: https://web.archive.org/web/20190324115921/http://david.darais.com/courses/fa2018-cs295A/
|
||||
[IU-2020]: https://jsiek.github.io/B522-PL-Foundations/
|
||||
[SFPL-Meetup-2020]: 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
|
||||
[UT-2020]: https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf
|
||||
[UW-2019]: https://cs.uwaterloo.ca/~plragde/842/
|
||||
[UT-2020]: https://www.cs.utexas.edu/~wcook/Courses/386L/Sp2020-GradPL.pdf
|
||||
[BHAM-2019]: https://www.cs.bham.ac.uk/internal/modules/2019/06-26943/
|
||||
[EUSA-2020]: https://www.eusa.ed.ac.uk/representation/campaigns/teachingawards2020/
|
||||
[SBMF]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
|
||||
[SCP]: https://homepages.inf.ed.ac.uk/wadler/topics/agda.html#scf
|
||||
[NextJournal]: https://nextjournal.com/plfa/ToC
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -13,17 +13,18 @@ Thank you to:
|
|||
|
||||
A special thank you, for inventing ideas on which
|
||||
this book is based, and for hand-holding:
|
||||
* Conor McBride
|
||||
* James McKinna
|
||||
* Ulf Norell
|
||||
* Andreas Abel
|
||||
<ul class="list-of-contributors">
|
||||
<li>Andreas Abel</li>
|
||||
<li>Catarina Coquand</li>
|
||||
<li>Thierry Coquand</li>
|
||||
<li>David Darais</li>
|
||||
<li>Per Martin-Löf</li>
|
||||
<li>Lena Magnusson</li>
|
||||
<li>Conor McBride</li>
|
||||
<li>James McKinna</li>
|
||||
<li>Ulf Norell</li>
|
||||
</ul>
|
||||
|
||||
|
||||
For a note showing how much more compact it is to avoid raw terms:
|
||||
* David Darais
|
||||
|
||||
|
||||
<span class="force-end-of-list"></span>
|
||||
{%- if site.contributors or site.extra_contributors -%}
|
||||
For pull requests big and small, and for answering questions on the Agda mailing list:
|
||||
<ul class="list-of-contributors">
|
||||
|
|
@ -50,6 +51,6 @@ For pull requests big and small, and for answering questions on the Agda mailing
|
|||
|
||||
For support:
|
||||
* EPSRC Programme Grant EP/K034413/1
|
||||
* NSF Grant No. 1814460
|
||||
* NSF Grant No. 1814460
|
||||
* Foundation Sciences Mathematiques de Paris (FSMP)
|
||||
Distinguised Professor Fellowship
|
||||
|
|
|
|||
|
|
@ -5,9 +5,9 @@ permalink : /Dedication/
|
|||
next : /Preface/
|
||||
---
|
||||
|
||||
<center>
|
||||
<h2>de Philip, para Wanda</h2>
|
||||
<h3><em>amor da minha vida</em></h3>
|
||||
<h4><em>knock knock knock</em></h4>
|
||||
<h4><em>...</em></h4>
|
||||
</center>
|
||||
<p style="text-align:center;">
|
||||
<p style="font-size:1.5em">de Philip, para Wanda</p>
|
||||
<p style="font-size:1.17em">amor da minha vida</p>
|
||||
<p style="font-size:1em">knock knock knock</p>
|
||||
<p style="font-size:1em">...</p>
|
||||
</p>
|
||||
|
|
|
|||
|
|
@ -1236,8 +1236,8 @@ to use them inside other binding contexts as well as at the top level.
|
|||
Here the two lookup judgments `∋m` and `∋m′` refer to two different
|
||||
bindings of variables named `"m"`. In contrast, the two judgments `∋n` and
|
||||
`∋n′` both refer to the same binding of `"n"` but accessed in different
|
||||
contexts, the first where "n" is the last binding in the context, and
|
||||
the second after "m" is bound in the successor branch of the case.
|
||||
contexts, the first where `"n"` is the last binding in the context, and
|
||||
the second after `"m"` is bound in the successor branch of the case.
|
||||
|
||||
And here are typings for the remainder of the Church example:
|
||||
```
|
||||
|
|
|
|||
|
|
@ -1234,7 +1234,7 @@ side to be well typed.
|
|||
|
||||
## Test examples
|
||||
|
||||
We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn),
|
||||
We repeat the [test examples]({{ site.baseurl }}/DeBruijn/#examples) from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
|
||||
in order to make sure we have not broken anything in the process of extending our base calculus.
|
||||
```
|
||||
two : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
|
|
|
|||
|
|
@ -74,8 +74,8 @@ other term will itself be closed and well typed. Repeat. We will
|
|||
either loop forever, in which case evaluation does not terminate, or
|
||||
we will eventually reach a value, which is guaranteed to be closed and
|
||||
of the same type as the original term. We will turn this recipe into
|
||||
Agda code that can compute for us the reduction sequence of `plus ·
|
||||
two · two`, and its Church numeral variant.
|
||||
Agda code that can compute for us the reduction sequence of `plus · two · two`,
|
||||
and its Church numeral variant.
|
||||
|
||||
(The development in this chapter was inspired by the corresponding
|
||||
development in _Software Foundations_, Volume _Programming Language
|
||||
|
|
@ -775,6 +775,14 @@ Where the construct introduces a bound variable we need to compare it
|
|||
with the substituted variable, applying the drop lemma if they are
|
||||
equal and the swap lemma if they are distinct.
|
||||
|
||||
For Agda it makes a difference whether we write `x ≟ y` or
|
||||
`y ≟ x`. In an interactive proof, Agda will show which residual `with`
|
||||
clauses in the definition of `_[_:=_]` need to be simplified, and the
|
||||
`with` clauses in `subst` need to match these exactly. The guideline is
|
||||
that Agda knows nothing about symmetry or commutativity, which require
|
||||
invoking appropriate lemmas, so it is important to think about order of
|
||||
arguments and to be consistent.
|
||||
|
||||
#### Exercise `subst′` (stretch)
|
||||
|
||||
Rewrite `subst` to work with the modified definition `_[_:=_]′`
|
||||
|
|
@ -942,6 +950,7 @@ data Steps (L : Term) : Set where
|
|||
The evaluator takes gas and evidence that a term is well typed,
|
||||
and returns the corresponding steps:
|
||||
```
|
||||
{-# TERMINATING #-}
|
||||
eval : ∀ {L A}
|
||||
→ Gas
|
||||
→ ∅ ⊢ L ⦂ A
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue