The Scottish Programming Languages and Verification Summer School 2020 will take place virtually, and will be hosted by the Laboratory for Foundations of Computer Science, at the University of Edinburgh.
Courses
The school will feature an invited course, and three core courses.
Invited course
- Maribel Fernandez (King’s College London): Nominal rewriting and unification
Core courses
- Jamie Gabbay (Heriot-Watt University): Nominal datatypes
- Michel Steuwer (University of Edinburgh): Compiler intermediate representations
- Edwin Brady (University of St Andrews): The Implementation of Idris 2
General organisation.
All lectures will take place on-line. The courses will be scheduled during three consecutive weeks as follows (all times are BST (British Summer Time)):Schedule
| Mon | Tues | Wed | Thur | Fri | |
|
Week 1 Nominal Techniques |
3 Aug 10.30am Fernandez 1 noon lunch break 2.00pm Fernandez 2 3.30pm |
4 Aug 10.30am Fernandez 3 noon |
5 Aug 10.30am Gabbay 1 noon |
6 Aug 10.30am Gabbay 2 noon
5.30pm What is an EUTxO blockchain? (external) |
7 Aug 10.30am Gabbay 3 noon |
|
Week 2 Compiler Intermediate Representations |
10 Aug
3.00pm Steuwer 1 4.00pm |
11 Aug
3.00pm Steuwer 2 4.00pm |
12 Aug
3.00pm Steuwer 3 4.00pm |
13 Aug 2.00pm contributed talks Torrens Horta Alvares da Silva Richter Kaleba 2.45pm short break 3.00pm Steuwer 4 4.00pm |
14 Aug |
|
Week 3 The Implementation of Idris 2 |
17 Aug 11.15am contributed talks: Hagedorn Sottile Nia Wood noon lunch break 3.00pm |
18 Aug
3.00pm |
19 Aug
3.00pm |
20 Aug
3.00pm |
21 Aug |
Part 1: Week of 03 – 07 Aug: Nominal techniques:
Maribel Fernandez: Nominal techniques (slides) Syllabus-
-
- Introduction
- First-order languages
- Languages with binding operators
- Specifying binders:
- alpha-equivalence
- Nominal syntax
- Nominal unification (unification modulo alpha-equivalence)
- Nominal matching (matching modulo alpha-equivalence)
- Nominal rewriting
- Extending first-order rewriting to specify binding operators
- Closed rewriting
- Confluence
- Typed Rewriting Systems
- Equational Axioms: AC operators
- Introduction
-
Lecture guide
-
-
- Monday morning: slides 1-61
- Monday afternoon: slides 61-108
-
-
- #edinburgh2020 for questions about the content; and
- #nominaldatatypes for technical support and further information.
Part 2: Week of 10 – 14 August: Language Implementation I:
Michel Steuwer: Compiler intermediate representations Video recordings are available on YouTube.Part 3: Week of 17 – 21 August: Language Implementation II:
Edwin Brady: The Implementation of Idris 2 Course material is available on GitHub Video recordings on YouTube. Each courses will comprise a mix of formal lectures (up to 5 hours), labs and discussions (up to 6 hours). The on-line SPLV forum will be used to ask questions and discuss lectures and exercises.Labs
Labs will happen on-line, using the SPLV forum.Prerequisites
The school is aimed at PhD students in programming languages, verification and related areas. Also researchers and practitioners will be very welcome, as will strong master’s students. Participants will need to have a background in computer science, mathematics or a related discipline, and have basic familiarity with (functional) programming and logic.
Registration
Registration is free, but all participants need to register by following this link:
http://tiny.cc/SPLV20-registration
Schedule
A preliminary schedule can be found here.
Lightning talks
All attendees are invited to give a lightning talk (up to 10 minutes), about their research. Please indicate you are interested in giving a presentation on your registration form.
Sponsorship
The summer school is hosted by the University of Edinburgh and partially supported by ERC grant Skye (grant no 682315) and the UK Manycore Network.
We also offer a range of sponsorship opportunities for industry with attractive benefits — please get in touch if you are interested.
Organisers
| Ekaterina Komendantskaya | Heriot-Watt University |
| James Cheney | University of Edinburgh |
| Ohad Kammar | University of Edinburgh ohad.kammar@ed.ac.uk |