merge

.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

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.
+
+
+
+
+
+
+
+
+
+

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