SPLV 2020, 03-21 August 2020, Edinburgh Informatics

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

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

    Gabbay

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
  Brady 1
4.00pm

18 Aug

 

 

 

 

 

 

 

 

 

3.00pm
  Brady 2
4.00pm

19 Aug

 

 

 

 

 

 

 

 

 

3.00pm
  Brady 3
4.00pm

20 Aug

 

 

 

 

 

 

 

 

 

3.00pm
  Brady 4
4.00pm

 21 Aug

 

Part 1: Week of 03 – 07 Aug: Nominal techniques:

  Maribel Fernandez: Nominal techniques (slides)
Syllabus
      1. Introduction
        • First-order languages
        • Languages with binding operators
      2. Specifying binders:
        • alpha-equivalence
        • Nominal syntax
        • Nominal unification (unification modulo alpha-equivalence)
        • Nominal matching (matching modulo alpha-equivalence)
      3. Nominal rewriting
        • Extending first-order rewriting to specify binding operators
        • Closed rewriting
        • Confluence
        • Typed Rewriting Systems
      4. Equational Axioms: AC operators

Lecture guide

      1. Monday morning: slides 1-61
      2. Monday afternoon: slides 61-108
 
  Jamie Gabbay: Nominal datatypes
Course material is available on GitHub.
Please make sure you can use before the course starts. Please use the Slack channel for questions:
    • #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
 

Part 3: Week of 17 – 21 August: Language Implementation II:

  Edwin Brady: The Implementation of Idris 2
 
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