From a77284a415da5786a5953c44ee26c9afc7c97001 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 28 Dec 2019 16:47:01 -0300 Subject: [PATCH 1/8] added icfp tutorial --- courses/icfp/icfp19-tutorials-form.txt | 158 +++++++++++++++++++++++++ 1 file changed, 158 insertions(+) create mode 100644 courses/icfp/icfp19-tutorials-form.txt diff --git a/courses/icfp/icfp19-tutorials-form.txt b/courses/icfp/icfp19-tutorials-form.txt new file mode 100644 index 00000000..f7205bb5 --- /dev/null +++ b/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. + + + + + + + + + + From 461c574f8dc3591aebbfe084ee358e1af63ae177 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 28 Dec 2019 22:40:02 +0100 Subject: [PATCH 2/8] Lambda: give the suc constructor is the text with an argument --- src/plfa/part2/Lambda.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index f5c5616e..651b84da 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/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 N `` * Case `` case L [zero⇒ M |suc x ⇒ N ] `` And one is for recursion: From 35e66258cc9c787731c43722ec39543303ce36a4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sat, 28 Dec 2019 22:47:03 +0100 Subject: [PATCH 3/8] Lambda: make the argument name consistent with the latter text --- src/plfa/part2/Lambda.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 651b84da..699bdfd1 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/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 N `` + * Successor `` `suc M `` * Case `` case L [zero⇒ M |suc x ⇒ N ] `` And one is for recursion: From ed9778325283928443ae2f0fde671e527b72357c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Sun, 29 Dec 2019 22:37:49 +0100 Subject: [PATCH 4/8] Lambda: fix indentation for correct rendering --- src/plfa/part2/Lambda.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index 699bdfd1..dc87fbbb 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -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 From 3a3539bb7709b5743f9fb06808a20c6c511a56a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marko=20Dimja=C5=A1evi=C4=87?= Date: Fri, 3 Jan 2020 08:50:22 +0100 Subject: [PATCH 5/8] Lambda: fix the term in an example showing typing relation is not injective --- src/plfa/part2/Lambda.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md index dc87fbbb..08798dc3 100644 --- a/src/plfa/part2/Lambda.lagda.md +++ b/src/plfa/part2/Lambda.lagda.md @@ -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 From 9f6e3125e71192f54034de7e9b3328ef2c5d98d3 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Fri, 3 Jan 2020 15:24:02 +0000 Subject: [PATCH 6/8] Fixed #445 --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 8f4a342c..562cb668 100644 --- a/.travis.yml +++ b/.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 From 733f1d9212ed61593cba541226b91d345c52edad Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Fri, 3 Jan 2020 15:56:50 +0000 Subject: [PATCH 7/8] Fix #446 --- Gemfile | 1 + 1 file changed, 1 insertion(+) diff --git a/Gemfile b/Gemfile index 1eac9d04..a34a47d0 100644 --- a/Gemfile +++ b/Gemfile @@ -2,6 +2,7 @@ source "https://rubygems.org" group :jekyll_plugins do gem 'github-pages' + gem 'octokit', "~> 4.15.0" end group :development do From 4bcd2f4f0b161b420b6ef4e6b15d6948b8ecbb8e Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Fri, 3 Jan 2020 16:24:41 +0000 Subject: [PATCH 8/8] Travis CI deployment is broken. --- Gemfile | 1 - 1 file changed, 1 deletion(-) diff --git a/Gemfile b/Gemfile index a34a47d0..1eac9d04 100644 --- a/Gemfile +++ b/Gemfile @@ -2,7 +2,6 @@ source "https://rubygems.org" group :jekyll_plugins do gem 'github-pages' - gem 'octokit', "~> 4.15.0" end group :development do