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