158 lines
4.9 KiB
Text
158 lines
4.9 KiB
Text
----------------------------------------------------------------------
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|