Programming Language Foundations in Agda

schedule May 15th 01:45 - 03:15 PM place Red Room people 62 Interested

PARTICIPANT PREPARATION:

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/

Outline:

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

The textbook is freely available online:

  • Programming Language Foundations in Agda
    plfa.inf.ed.ac.uk
    github.com/plfa/plfa.github.io/

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

 
1 favorite thumb_down thumb_up 0 comments visibility_off  Remove from Watchlist visibility  Add to Watchlist
 

Learning Outcome

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.

Target Audience

Anyone interested in Type Theory and its applications

Prerequisites for Attendees

No participant prerequisites are 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.
schedule Submitted 1 week ago