Merge branch 'dev' of github.com:plfa/plfa.github.io into dev

.travis.yml

@@ -36,7 +36,7 @@ before_install:
 - make travis-setup
 
 script:
-- curl -L https://raw.githubusercontent.com/MestreLion/git-tools/master/git-restore-mtime | python
+- travis_retry curl -L https://raw.githubusercontent.com/plfa/git-tools/master/git-restore-mtime | python
 - agda --version
 - acknowledgements --version
 - make test-offline # disable to only build cache

beta.md

@@ -64,7 +64,8 @@ Pull requests are encouraged.
 
   - Courses taught from the textbook:
     * Philip Wadler, University of Edinburgh,
-      [2018]({{ site.baseurl }}/TSPL/2018/)
+      [2018]({{ site.baseurl }}/TSPL/2018/),
+	  [2019]({{ site.baseurl }}/TSPL/2019/)
     * David Darais, University of Vermont,
       [2018](http://david.darais.com/courses/fa2018-cs295A/)
     * John Leo, Google Seattle, 2018--2019
@@ -72,6 +73,8 @@ Pull requests are encouraged.
       [2019]({{ site.baseurl }}/PUC/2019/)
     * Prabhakar Ragde, University of Waterloo,
       [2019](https://cs.uwaterloo.ca/~plragde/842/)
+    * Jeremy Siek, Indiana University,
+	  [2020](https://jsiek.github.io/B522-PL-Foundations/)
   - A paper describing the book appeared in [SBMF][sbmf].
 
 [wen]: https://wenkokke.github.io

courses/icfp/icfp19-tutorials-form.txt

@@ -0,0 +1,158 @@
+----------------------------------------------------------------------
+                            ICFP 2019
+ 24th ACM SIGPLAN International Conference on Functional Programming
+
+                       August 18 - 23, 2019 
+                          Berlin, Germany
+                    https://icfp19.sigplan.org/
+
+                         TUTORIAL PROPOSAL FORM
+
+----------------------------------------------------------------------
+
+This form is due May 10th, 2019.
+
+
+NAME OF THE TUTORIAL:
+
+   Programming Language Foundations in Agda
+
+
+PRESENTER(S):
+
+   (Please complete the following table for each presenter.)
+
+   Name    : Philip Wadler
+   Address : LFCS, School of Informatics, University of Edinbugh
+   Email   : wadler@inf.ed.ac.uk
+   Phone   : +44 131 650 5174 (after 21 July)
+   Mobile  : +55 71 99652 2018 (before 13 July)
+             +44 7976 507 543 (after 14 July)
+
+
+ABSTRACT:
+
+   This course is in two parts, each three hours long. Part I is an
+   introduction to formal methods in Agda, covering datatypes,
+   recursion, structural induction, indexed datatypes, dependent
+   functions, and induction over evidence; with focus on formal
+   definitions of naturals, addition, and inequality, and their
+   properties.  Part II is an introduction to formal models of
+   simply-typed lambda calculus in Agda, including reduction, type
+   rules, and progress and preservation, and (as a consequence)
+   evaluation of lambda terms. Part II depends on Part I, but Part I
+   can be skipped by those already familiar with Agda.
+
+   The textbook is freely available online:
+     Programming Language Foundations in Agda
+     plfa.inf.ed.ac.uk
+     github.com/plfa/plfa.github.io/
+
+   The books has been used for teaching by me at:
+     University of Edinburgh (Sep-Dec 2018)
+     Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio) (Mar-Jul 2019)
+     University of Padova (Jun 2019)
+   and by others at
+     University of Vermont
+     Google Seattle.
+   The book is described in a paper (of the same title) at the XXI
+   Brazilian Symposium on Formal Methods, 28--30 Nov 2018, which is
+   available here:
+     http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
+   The paper won the SBMF 2018 Best Paper Award, 1st Place.
+
+
+REQUIRED PARTICIPANT BACKGROUND:
+
+   (What background knowledge and skills will be assumed? Is the
+   tutorial primarily intended for industrial users of functional
+   programming, researchers in functional programming, or some other
+   audience?)
+
+   No prerequisites required. Any or all of the following will be
+   helpful:
+     * Familiarity with functional programming, particularly
+       data types, recursion, and pattern matching.
+     * Familiarity with proof by induction.
+     * Familiarity with a proof assistant.
+     * Familiarity with Emacs.
+
+
+LEARNING OUTCOMES:
+
+   (What will participants be able to do after the tutorial?)
+
+   Part I: Formulate and prove in Agda properties of
+   operations of naturals (such as addition and multiplication), and
+   relations on naturals (such as inequality), using structural
+   induction and induction over evidence of a relation.
+
+   Part II: Formulate and prove in Agda formal models of simply-typed
+   lambda calculus in Agda, including reduction, type rules, and
+   progress and preservation, and (as a consequence) evaluation of
+   lambda terms.
+
+
+SPECIAL REQUIREMENTS:
+
+    (Does the tutorial need Internet access for the presenter? For the
+    participants?)
+
+    If the participants follow the instructions under 'Participant
+    Preparation' in advance, then no internet access is required.
+
+
+
+SCHEDULING CONSTRAINTS:
+    (Are there any days on which you cannot hold the tutorial?)
+
+    None
+
+
+PARTICIPANT PREPARATION:
+
+    (What preparation is required? Do participants need to bring
+    laptops?  If so, do they need to have any particular software?)
+
+    Clone the repository at
+      https://github.com/plfa/plfa.github.io/
+    This is the textbook for the course.
+
+    Install Agda, the Agda standard library, and configure the
+    plfa library. This can be done by following the instructions
+    under the heading
+      Getting Started with PLFA
+    at
+      https://plfa.github.io/GettingStarted/
+
+
+PLANS FOR PUBLICITY:
+
+   (Including, but not limited to, web pages, mailing lists, and
+   newsgroups.)
+
+   I will advertise on my home page and blog, and on the home page for
+   the textbook, and mail to Types and other standard lists.
+
+
+ADDITIONAL INFORMATION:
+
+   (If there is any additional information that you would like
+   to make us aware of, please include the details here.
+
+   For example, you may wish to indicate a preference for particular
+   dates, or that the tutorial should not be run in parallel with
+   certain workshops; in such cases, please also include the
+   reasons for your preference.)
+
+   None.
+
+
+
+
+
+
+
+
+
+

courses/tspl/2019/Exam.lagda.md

@@ -1,5 +1,5 @@
 ---
-title     : "Exam: TSPL Mock Exam file"
+title     : "Exam: TSPL Exam file"
 layout    : page
 permalink : /TSPL/2019/Exam/
 ---
@@ -44,8 +44,6 @@ Remember to indent all code by two spaces.
 
 ### (b)
 
-### (c)
-
 
 ## Problem 2
 

courses/tspl/2019/tspl2019.md

@@ -145,6 +145,11 @@ but talk to me if you want to formalise something else.
 
 * Optional project cw6 due 4pm Thursday 28 November (Week 11)
 
+Submit the optional project by running
+``` bash
+submit tspl essay Essay.lagda.md
+```
+
 ## Mock exam
 
 10am-12noon Friday 29 November, AT 5.05 West Lab. An online

courses/tspl/send_marks.sh

@@ -6,7 +6,7 @@
 #
 # This script assumes the following folder structure:
 #
-#   $DIR/sXXXXXXX/cw$CW/$FILE
+#   $DIR/sXXXXXXX/$CW/$FILE
 #
 # The variable DIR refers to the directory passed in as an argument to the
 # script. The variable XXXXXXX refers to the student ID, and it is assumed
@@ -14,9 +14,9 @@
 #
 #   sXXXXXXX@sms.ed.ac.uk
 #
-# is a valid email address. The variable $CW refers to the number for of the
-# coursework of which the students are meant to be notified. The directory
-# DIR/sXXXXXXX/cwY/ should only contain a single file, which should be
+# is a valid email address. The variable $CW refers to the coursework
+# of which the students are meant to be notified (e.g., cw1). The directory
+# DIR/sXXXXXXX/$CW/ should only contain a single file, which should be
 # specified using the FILE parameter.
 #
 # Usage:
@@ -32,12 +32,12 @@ shift
 FILE="$1"
 shift
 
-for ATTACHMENT in "${DIR%/}/s"*"/cw$CW/$FILE"; do
+for ATTACHMENT in "${DIR%/}/s"*"/$CW/$FILE"; do
     SUBJ="Mark for coursework $CW"
     BODY=""
     SID=$(echo "$ATTACHMENT" | sed 's|.*/\(s[0-9]\{7\}\)/.*|\1|')
     ADDR="$SID@sms.ed.ac.uk"
-    CMD="echo \"$BODY\" | mail -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
+    CMD="echo \"$BODY\" | mail -c wadler@inf.ed.ac.uk -s \"$SUBJ\" -a \"$ATTACHMENT\" \"$ADDR\""
     echo "You are about to run the following command:"
     echo -e "\n$CMD\n"
     read -p "Are you sure? " -n 1 -r

extra/extra/Logic.lagda

@@ -301,7 +301,7 @@ evidence that a disjunction holds.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator.
 \begin{code}
-infix 1 _⊎_
+infixr 1 _⊎_
 \end{code}
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 

index.md

@@ -58,6 +58,8 @@ Pull requests are encouraged.
       [2019]({{ site.baseurl }}/PUC/2019/)
     * Prabhakar Ragde, University of Waterloo,
 	  [2019](https://cs.uwaterloo.ca/~plragde/842/)
+    * Jeremy Siek, Indiana University,
+	  [2020](https://jsiek.github.io/B522-PL-Foundations/)
   - A paper describing the book appeared in [SBMF][sbmf].
   - A notebook version of the textbook
     is available at [NextJournal][nextjournal].

src/plfa/part1/Connectives.lagda.md

@@ -389,7 +389,7 @@ simplify to the same term, and similarly for `inj₂ y`.
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator:
 ```
-infix 1 _⊎_
+infixr 1 _⊎_
 ```
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 

src/plfa/part1/Lists.lagda.md

@@ -115,12 +115,11 @@ _++_ : ∀ {A : Set} → List A → List A → List A
 []       ++ ys  =  ys
 (x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)
 ```
-The type `A` is an implicit argument to append, making it a
-_polymorphic_ function (one that can be used at many types).  The
-empty list appended to another list yields the other list.  A
-non-empty list appended to another list yields a list with head the
-same as the head of the first list and tail the same as the tail of
-the first list appended to the second list.
+The type `A` is an implicit argument to append, making it a _polymorphic_
+function (one that can be used at many types). A list appended to the empty list
+yields the list itself. A list appended to a non-empty list yields a list with
+the head the same as the head of the non-empty list, and a tail the same as the
+other list appended to tail of the non-empty list.
 
 Here is an example, showing how to compute the result
 of appending two lists:
@@ -682,7 +681,7 @@ Show
 
 Show as a consequence of `foldr-++` above that
 
-    xs ++ ys ≡ foldr _∷_ ys xs    
+    xs ++ ys ≡ foldr _∷_ ys xs
 
 
 ```
@@ -816,7 +815,7 @@ foldr-monoid _⊗_ e ⊗-monoid (x ∷ xs) y =
 In a previous exercise we showed the following.
 ```
 postulate
-  foldr-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) (xs ys : List A) → 
+  foldr-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) (xs ys : List A) →
     foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
 ```
 
@@ -1099,7 +1098,7 @@ data merge {A : Set} : (xs ys zs : List A) → Set where
     → merge xs ys zs
       --------------------------
     → merge xs (y ∷ ys) (y ∷ zs)
-```    
+```
 
 For example,
 ```

src/plfa/part2/Lambda.lagda.md

@@ -72,7 +72,7 @@ Terms have seven constructs. Three are for the core lambda calculus:
 Three are for the naturals:
 
   * Zero `` `zero ``
-  * Successor `` `suc ``
+  * Successor `` `suc M ``
   * Case `` case L [zero⇒ M |suc x ⇒ N ] ``
 
 And one is for recursion:
@@ -234,11 +234,11 @@ We intend to apply the function only when the first term is a variable, which we
 indicate by postulating a term `impossible` of the empty type `⊥`.  If we use
 C-c C-n to normalise the term
 
-  ƛ′ two ⇒ two
+    ƛ′ two ⇒ two
 
 Agda will return an answer warning us that the impossible has occurred:
 
-  ⊥-elim (plfa.part2.Lambda.impossible (`` `suc (`suc `zero)) (`suc (`suc `zero)) ``)
+    ⊥-elim (plfa.part2.Lambda.impossible (`` `suc (`suc `zero)) (`suc (`suc `zero)) ``)
 
 While postulating the impossible is a useful technique, it must be
 used with care, since such postulation could allow us to provide
@@ -1315,7 +1315,7 @@ there is at most one `A` such that the judgment holds:
 ```
 
 The typing relation `Γ ⊢ M ⦂ A` is not injective. For example, in any `Γ`
-the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`.
+the term `` ƛ "x" ⇒ ` "x" `` has type `A ⇒ A` for any type `A`.
 
 ### Non-examples
 

src/plfa/part2/Properties.lagda.md

@@ -568,7 +568,7 @@ swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
       --------------------------
     → Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
   ρ Z                   =  S x≢y Z
-  ρ (S y≢x Z)           =  Z
+  ρ (S z≢x Z)           =  Z
   ρ (S z≢x (S z≢y ∋z))  =  S z≢y (S z≢x ∋z)
 ```
 Here the renaming map takes a variable at the end into a variable one