{"id":426,"date":"2020-02-17T11:45:36","date_gmt":"2020-02-17T11:45:36","guid":{"rendered":"http:\/\/www.macs.hw.ac.uk\/splv\/?page_id=426"},"modified":"2020-08-17T14:10:25","modified_gmt":"2020-08-17T13:10:25","slug":"splv20","status":"publish","type":"page","link":"https:\/\/www.macs.hw.ac.uk\/splv\/splv20\/","title":{"rendered":"SPLV 2020, 03-21 August 2020, Edinburgh Informatics"},"content":{"rendered":"<p>The Scottish Programming Languages and Verification Summer School 2020 will take place virtually, and will be hosted by the <a href=\"http:\/\/web.inf.ed.ac.uk\/lfcs\">Laboratory for Foundations of Computer Science<\/a>,\u00a0at the University of Edinburgh.<\/p>\n<h3>Courses<\/h3>\n<p><!-- \/wp:post-content --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>The school will feature an invited course, and three core courses.<\/p>\n<h4>Invited course<\/h4>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:list --><\/p>\n<ul>\n<li><a href=\"https:\/\/nms.kcl.ac.uk\/maribel.fernandez\/\">Maribel Fernandez<\/a> (King&#8217;s College London): <strong>Nominal rewriting and unification<\/strong><\/li>\n<\/ul>\n<p><!-- \/wp:list --><\/p>\n<p><!-- wp:heading {\"level\":4} --><\/p>\n<h4>Core courses<\/h4>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:list --><\/p>\n<ul>\n<li><a href=\"http:\/\/gabbay.org.uk\/\">Jamie Gabbay<\/a> (Heriot-Watt University): <strong>Nominal datatypes<\/strong><\/li>\n<li><a href=\"https:\/\/michel.steuwer.info\/\">Michel Steuwer<\/a> (University of Edinburgh):\u00a0 <strong>Compiler intermediate representations<\/strong><\/li>\n<li><a href=\"https:\/\/www.type-driven.org.uk\/edwinb\/\" target=\"_blank\" rel=\"noopener noreferrer\"> Edwin Brady<\/a> (University of St Andrews): <strong>The Implementation of Idris 2<\/strong><\/li>\n<\/ul>\n<p><!-- \/wp:list --><\/p>\n<p><!-- wp:heading {\"level\":4} --><\/p>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:heading --><\/p>\n<h4>General organisation.\u00a0<\/h4>\nAll lectures will take place on-line. The courses will be scheduled during three consecutive weeks as follows (all times are BST (British Summer Time)):\n\u00a0\n<h4>Schedule<\/h4>\n<p>\u00a0<\/p>\n<table style=\"width: 117.255%;\">\n<tbody>\n<tr>\n<td style=\"vertical-align: top; width: 23.9992%;\">\u00a0<\/td>\n<td style=\"vertical-align: top; width: 16.6134%;\">Mon<\/td>\n<td style=\"vertical-align: top; width: 16.5395%;\">Tues<\/td>\n<td style=\"vertical-align: top; width: 13.7699%;\">Wed<\/td>\n<td style=\"vertical-align: top; width: 16.8662%;\">Thur<\/td>\n<td style=\"vertical-align: top; width: 26.1505%;\">Fri<\/td>\n<\/tr>\n<tr>\n<td style=\"vertical-align: top; width: 23.9992%;\">\n<p>Week 1<\/p>\n<p>Nominal Techniques<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.6134%;\">\n<p><i>3 Aug<\/i><\/p>\n<p>10.30am<\/p>\n<p><b>\u00a0Fernandez 1<\/b><\/p>\n<p>noon<\/p>\n<p>\u00a0 <em>lunch break<\/em><\/p>\n<p>2.00pm<\/p>\n<p><b>\u00a0 Fernandez 2<\/b><\/p>\n<p>3.30pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.5395%;\">\n<p><i>4 Aug<\/i><\/p>\n<p>10.30am<\/p>\n<p><b>\u00a0Fernandez 3<\/b><\/p>\n<p>noon<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 13.7699%;\">\n<p><i>5 Aug<\/i><\/p>\n<p>10.30am<\/p>\n<p><b>\u00a0 Gabbay 1<\/b><\/p>\n<p>noon<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.8662%;\">\n<p><i>6 Aug<\/i><\/p>\n<p>10.30am<\/p>\n<p><b>\u00a0 Gabbay 2<\/b><\/p>\n<p>noon<\/p>\n<p>\u00a0<\/p>\n<p style=\"text-align: left;\">5.30pm<\/p>\n<p style=\"text-align: left;\">\u00a0\u00a0\u00a0 <b><a href=\"https:\/\/galois.com\/blog\/2020\/07\/public-tech-talk-what-is-an-eutxo-blockchain\/\">Gabbay<\/a><\/b><\/p>\n<p style=\"text-align: left;\"><em>W<\/em><em>hat is an EUTxO blockchain?<\/em><\/p>\n<p style=\"text-align: right;\">(external)<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 26.1505%;\">\n<p><i>7 Aug<\/i><\/p>\n<p>10.30am<\/p>\n<p><b>\u00a0 Gabbay 3<\/b><\/p>\n<p>noon<\/p>\n<\/td>\n<\/tr>\n<tr>\n<td style=\"vertical-align: top; width: 23.9992%;\">\n<p>Week 2<\/p>\n<p>Compiler Intermediate Representations<\/p>\n<\/td>\n<td style=\"vertical-align: bottom; width: 16.6134%;\">\n<p><i>10 Aug<\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<\/p>\n<p>\u00a0 <strong>Steuwer 1<\/strong><\/p>\n<p>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: bottom; width: 16.5395%;\">\n<p><i>11 Aug <\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<\/p>\n<p>\u00a0 <strong>Steuwer 2<br \/><\/strong><\/p>\n<p>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: bottom; width: 13.7699%;\">\n<p><i>12 Aug <\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<\/p>\n<p>\u00a0 <strong>Steuwer 3<br \/><\/strong><\/p>\n<p>4.00pm<\/p>\n<\/td>\n<td style=\"width: 16.8662%; vertical-align: top;\">\n<p><i><i>13 Aug<\/i><\/i><\/p>\n<p>2.00pm<\/p>\n<p>\u00a0 <em>contributed<\/em><\/p>\n<p>\u00a0 <em>talks<\/em><\/p>\n<p>\u00a0 Torrens<\/p>\n<p>\u00a0 Horta Alvares<\/p>\n<p>\u00a0\u00a0\u00a0 da Silva<\/p>\n<p>\u00a0 Richter<\/p>\n<p>\u00a0 Kaleba<\/p>\n<p>2.45pm<\/p>\n<p>\u00a0 <em>short break<\/em><\/p>\n<p>3.00pm<\/p>\n<p>\u00a0 <strong>Steuwer 4<br \/><\/strong><\/p>\n<p>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 26.1505%;\">\n<p><i>14 Aug <\/i><\/p>\n<\/td>\n<\/tr>\n<tr>\n<td style=\"vertical-align: top; width: 23.9992%;\">\n<p>Week 3<\/p>\n<p>The Implementation of Idris 2<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.6134%;\">\n<p><i>17 Aug<\/i><\/p>\n<p>11.15am<\/p>\n<p>\u00a0 <em>contributed<\/em><\/p>\n<p>\u00a0 <em>talks:<\/em><\/p>\n<p>\u00a0 Hagedorn<\/p>\n<p>\u00a0 Sottile<\/p>\n<p>\u00a0 Nia<\/p>\n<p>\u00a0 Wood<\/p>\n<p>noon<\/p>\n<p>\u00a0 <em>lunch break<\/em><\/p>\n<p>3.00pm<br \/><b>\u00a0 Brady 1<\/b><br \/>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.5395%;\">\n<p><i>18 Aug<\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<br \/><b>\u00a0 Brady 2<\/b><br \/>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 13.7699%;\">\n<p><i>19 Aug<\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<br \/><b>\u00a0 Brady 3<\/b><br \/>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 16.8662%;\">\n<p><i>20 Aug<\/i><\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>\u00a0<\/p>\n<p>3.00pm<br \/><b>\u00a0 Brady 4<\/b><br \/>4.00pm<\/p>\n<\/td>\n<td style=\"vertical-align: top; width: 26.1505%;\">\n<p><i>\u00a021 Aug<\/i><\/p>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\u00a0\n<h4>Part 1: Week of 03 &#8211; 07 Aug: Nominal techniques:<\/h4>\n\u00a0 Maribel Fernandez: Nominal techniques (<a href=\"http:\/\/denotational.co.uk\/splv20\/maribel-fernandez-nominal-techniques.pdf\">slides<\/a>)\nSyllabus\n<ol>\n<li style=\"list-style-type: none;\">\n<ol>\n<li style=\"list-style-type: none;\">\n<ol>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Introduction\n<ul>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">First-order languages<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Languages with binding operators<\/li>\n<\/ul>\n<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Specifying binders:\n<ul>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">alpha-equivalence<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Nominal syntax<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Nominal unification (unification modulo alpha-equivalence)<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Nominal matching (matching modulo alpha-equivalence)<\/li>\n<\/ul>\n<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Nominal rewriting\n<ul>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Extending first-order rewriting to specify binding operators<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Closed rewriting<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Confluence<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Typed Rewriting Systems<\/li>\n<\/ul>\n<\/li>\n<li style=\"font-stretch: normal; font-size: 11px; line-height: normal; font-family: Menlo;\">Equational Axioms: AC operators<\/li>\n<\/ol>\n<\/li>\n<\/ol>\n<\/li>\n<\/ol>\n<p style=\"padding-left: 40px;\">Lecture guide<\/p>\n<ol>\n<li style=\"list-style-type: none;\">\n<ol>\n<li style=\"list-style-type: none;\">\n<ol>\n<li>Monday morning: slides 1-61<\/li>\n<li>Monday afternoon: slides 61-108<\/li>\n<\/ol>\n<\/li>\n<\/ol>\n<\/li>\n<\/ol>\n\u00a0\n\u00a0 Jamie Gabbay:\u00a0Nominal datatypes\nCourse material is available on <a href=\"https:\/\/github.com\/bellissimogiorno\/nominal\">GitHub<\/a>.\nVideo recordings are available on <a href=\"https:\/\/www.youtube.com\/playlist?list=PLmYPUe8PWHKpAyfjsrHYoJF7MtyT5W0-D\">YouTube<\/a>.\nPlease make sure you can use before the course starts. Please use the Slack channel for questions:\n<ul>\n<li style=\"list-style-type: none;\">\n<ul>\n<li>#edinburgh2020 for questions about the content; and<\/li>\n<li>#nominaldatatypes for technical support and further information.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n\u00a0\n<h4>Part 2: Week of 10 &#8211; 14 August: Language Implementation I:<\/h4>\n\u00a0 Michel Steuwer:\u00a0Compiler intermediate representations\n\u00a0 Video recordings are available on <a href=\"https:\/\/www.youtube.com\/playlist?list=PLmYPUe8PWHKrc3arcxUPp2XosprqIb617\">YouTube<\/a>.\n\u00a0\n<h4>Part 3: Week of 17 &#8211; 21 August: Language Implementation II:<\/h4>\n\u00a0 Edwin Brady: The Implementation of Idris 2\nCourse material is available on <a href=\"https:\/\/github.com\/edwinb\/SPLV20\">GitHub<\/a>\nVideo recordings on <a href=\"https:\/\/www.youtube.com\/playlist?list=PLmYPUe8PWHKqBRJfwBr4qga7WIs7r60Ql\">YouTube<\/a>.\nEach courses will comprise a mix of formal lectures (up to 5 hours), labs and discussions (up to 6 hours). The <a href=\"http:\/\/splv.slack.com\">on-line SPLV forum<\/a> will be used to ask questions and discuss lectures and exercises.\u00a0\n\u00a0\n<h4>Labs<\/h4>\nLabs will happen on-line, using the SPLV forum.\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:heading {\"level\":4} --><\/p>\n<h2>Prerequisites<\/h2>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>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&#8217;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.<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:heading --><\/p>\n<h2>Registration<\/h2>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>Registration is free, but all participants need to register by following this link:<\/p>\n<p><a href=\"http:\/\/tiny.cc\/SPLV20-registration\" target=\"_blank\" rel=\"noopener noreferrer\">http:\/\/tiny.cc\/SPLV20-registration<\/a><\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:table --><\/p>\n<p><!-- \/wp:table --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:heading --><\/p>\n<h2>Schedule<\/h2>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>A preliminary schedule can be found here.<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:heading --><\/p>\n<h2>Lightning talks<\/h2>\n<p><!-- \/wp:heading --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>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.<\/p>\n<h2>Sponsorship<\/h2>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>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.<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:paragraph --><\/p>\n<p>We also offer a range of <a href=\"http:\/\/www.macs.hw.ac.uk\/splv\/#sponsorship\">sponsorship opportunities for industry with attractive benefits<\/a> \u2014 please get in touch if you are interested.<\/p>\n<p><!-- \/wp:paragraph --><\/p>\n<p><!-- wp:tadv\/classic-paragraph --><\/p>\n<figure><a href=\"https:\/\/www.sicsa.ac.uk\/\"><img loading=\"lazy\" decoding=\"async\" src=\"http:\/\/www.macs.hw.ac.uk\/splv\/wp-content\/uploads\/2019\/05\/sicsa-300x82.jpeg\" alt=\"\" width=\"300\" height=\"82\" \/><\/a><\/figure>\n<figure><a href=\"https:\/\/erc.europa.eu\/\"><img loading=\"lazy\" decoding=\"async\" src=\"http:\/\/www.macs.hw.ac.uk\/splv\/wp-content\/uploads\/2019\/05\/erc_logo.png\" alt=\"\" width=\"100\" height=\"99\" \/><\/a><\/figure>\n<figure><a href=\"https:\/\/manycore.org.uk\/\"><img loading=\"lazy\" decoding=\"async\" src=\"http:\/\/www.macs.hw.ac.uk\/splv\/wp-content\/uploads\/2019\/05\/marionet-300x98.jpg\" alt=\"\" width=\"300\" height=\"98\" \/><\/a><\/figure>\n<p><!-- \/wp:tadv\/classic-paragraph --><\/p>\n<p><!-- wp:tadv\/classic-paragraph --><\/p>\n<h2 data-tadv-p=\"keep\">\u00a0<\/h2>\n<h2 data-tadv-p=\"keep\">\u00a0<\/h2>\n<h2 data-tadv-p=\"keep\">\u00a0<\/h2>\n<h2 data-tadv-p=\"keep\">Organisers<\/h2>\n<table style=\"width: 129.037%; height: 144px;\">\n<tbody>\n<tr style=\"height: 48px;\">\n<td style=\"height: 48px;\"><a href=\"http:\/\/www.macs.hw.ac.uk\/~ek19\/\" target=\"_blank\" rel=\"noopener noreferrer\">Ekaterina Komendantskaya<\/a><\/td>\n<td style=\"height: 48px;\">Heriot-Watt University<\/td>\n<\/tr>\n<tr style=\"height: 48px;\">\n<td style=\"height: 48px;\"><a href=\"http:\/\/homepages.inf.ed.ac.uk\/jcheney\/\" target=\"_blank\" rel=\"noopener noreferrer\">James Cheney<\/a><\/td>\n<td style=\"height: 48px;\">University of Edinburgh<\/td>\n<\/tr>\n<tr style=\"height: 48px;\">\n<td style=\"vertical-align: top; height: 48px;\"><a href=\"http:\/\/denotational.co.uk\/\">Ohad Kammar<\/a><\/td>\n<td style=\"height: 48px;\">University of Edinburgh<br \/>ohad.kammar@ed.ac.uk<\/td>\n<\/tr>\n<\/tbody>\n<\/table>","protected":false},"excerpt":{"rendered":"<p>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,\u00a0at the University of Edinburgh. Courses The school will feature an invited course, and three core courses. Invited course Maribel Fernandez (King&#8217;s College London): Nominal rewriting and unification Core courses Jamie&hellip;&nbsp;<a href=\"https:\/\/www.macs.hw.ac.uk\/splv\/splv20\/\" class=\"\" rel=\"bookmark\">Read More &raquo;<span class=\"screen-reader-text\">SPLV 2020, 03-21 August 2020, Edinburgh Informatics<\/span><\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"parent":18,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-426","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/pages\/426","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/comments?post=426"}],"version-history":[{"count":54,"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/pages\/426\/revisions"}],"predecessor-version":[{"id":519,"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/pages\/426\/revisions\/519"}],"up":[{"embeddable":true,"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/pages\/18"}],"wp:attachment":[{"href":"https:\/\/www.macs.hw.ac.uk\/splv\/wp-json\/wp\/v2\/media?parent=426"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}