Programming Language Foundations in Agda
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.
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.
Links
http://homepages.inf.ed.ac.uk/wadler/topics/agda.html#sbmf
Programming Language Foundations in Agda:
http://plfa.inf.ed.ac.uk
http://github.com/plfa/plfa.github.io/
schedule Submitted 3 years ago
Recent Activities
Call for Proposals CLOSED
Ended on Mar 26 '19 12:00 AM AEDT
YOW! Lambda Jam is a conference for applied functional software developers. The conference provides the opportunity to share experiences so that attendees can improve software development using the principles, practices and tools of functional programming.
Lessons learned and specific practices are very important for this pragmatic conference, hence we encourage submissions which deal with the practical challenges of functional programming such as: developing commercial FP proficiency; leveraging good theory or algorithms to make better practice; pragmatics of applying a specific language or technique in the real world; production challenges such as deployment speed / space; lessons learned taking the wrong road.
The first day is tutorial day which provides a small number full day tutorials on topics for novices, and intermediate to advanced functional programmers. This was a very and popular feature of our 2018 conference.
We welcome submissions for talks (30 minutes), workshops or code jams (90 minutes) or full-day tutorials. .
| Call for Presentations Open Until | 22 March, 2019 |
| Speaker Notifications | 1 April, 2019 |
| Conference Dates – Melbourne | 13 – 15 May, 2019 |
Please see the submission guidelines before submitting your proposal.
Craig Smith
Aamir Nazir
Tristan LE GUILLOU
