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