Programme

Keynote speaker

Picture of Philip Wadler Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is a Fellow of the Royal Society, a Fellow of the Royal Society of Edinburgh, and an ACM Fellow. He is head of the steering committee for Proceedings of the ACM, past editor-in-chief of PACMPL and JFP, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award.

Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of over 70 with more than 25,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.


Schedule

12:00 Lunch with coffee
12:45 Session 1
12:45 - 13:45 Substitution without Copy and Paste • Phil Wadler
13:45 - 14:15 Applying Formal Methods to Cardano • James Chapman
14:15 Short coffee break
14:30 Session 2
14:30 - 15:00 Freely Extending Interpreters • Greg Brown
15:00 - 15:30 Hardware Architectures for Lazy Functional Programming, Revisited • Craig Ramsay
15:30 - 16:00 Forwarders Should Be Lazy • Wen Kokke
16:00 Long coffee break
16:30 Session 3
16:30 - 17:00 Strong Rule Induction for Syntax with Bindings • Jan van Brügge
17:00 - 17:30 A Tale of Two Compilers • Wim Vanderbauwhede
17:30 - late Pub and dinner

Post-seminar social gathering

We have dinner booked at Mosob Ethiopian & Eritrean Restaurant, 56 Dundas Street, Glasgow G1 2AQ. The reservation is at 18:30, which gives attendees ample time to reach the dinner venue. We can take the subway from Hillhead station to Buchanan Street station. Mosob is in the City Centre, next to Queen Street station and close to Glasgow Central train station.

We may visit the pub afterwards.

Abstracts

You can find the abstracts and a downloadable version of the slides provided by speakers. Slides will be uploaded after the event.


  1. Substitution without Copy and PastePhil Wadler • University of Edinburgh    Slides

    The definition of substitution in the presence of lambda binding is notoriously difficult to get correct. The best technique, which I first learned from Conor McBride, is straightforward but does everything twice, defining renaming first and substitution second. That is not so bad, but the key result describing composition explodes into four proofs, with either renaming or substitution on both the left and right. This talk describes a new approach that collapses the two definitions to one definition and the four proofs to one proof. The result includes a set of rewrites (taken from Autosubst) that can simplify any equation involving substitution. Our work is available as an Agda script.

    This is joint work with Thorsten Altenkirch and Nathaniel Burke.

  2. Applying Formal Methods to CardanoJames Chapman • IOHK Research   

    Cardano is a Proof-of-Stake cryptocurrency with a market cap in the tens of billions of USD and a daily volume of hundreds of millions of USD. In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano. We describe our strategy, our projects, reflect on lessons learned, the challenges we face and how we propose to meet them.

  3. Freely Extending InterpretersGreg Brown • University of Edinburgh    Slides

    A partial evaluator extends an interpreter to work on terms with free variables. In this talk, I will formalise this intuition for pure simply-typed languages. I will focus on the simply-typed lambda calculus, but my definitions are in terms of any second-order algebra as defined by Fiore. After giving a definition for a denotational interpreter, I will define what it means for a model of a language (formulated as a SOAS algebra) to extend an interpreter, as well as morphisms between extensions. From this, I will define the free extension of an interpreter, which is the least opinionated partial evaluator.

    This is work in progress towards my PhD.

  4. Hardware Architectures for Lazy Functional Programming, RevisitedCraig Ramsay • Heriot-Watt University    Slides

    Custom hardware architectures for functional languages enjoyed a boom in the 80s and 90s following Backus' Turing Award lecture "Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs". Research interest later waned due to difficulties in matching the rapid pace of RISC processor development and compiler techniques.

    This talk from the HAFLANG project re-explores these ideas in a modern landscape --- where single-thread performance of stock CPUs have begun to stagnate, but the performance of hardware prototyping platforms such as FPGAs have not. We present the Heron processor for evaluating non-strict functional programs, as well as its concurrent hardware garbage collector. While still slightly slower than conventional platforms, it offers interesting advantages in energy efficiency and opportunity for formal verification from source language down to hardware implementation. We also propose a path towards a single-chip many-core architecture.

  5. Forwarders Should Be LazyWen Kokke • Strathclyde University and the University of Edinburgh    Slides

    Classical Processes is a process calculus interpretation of Classical Linear Logic. Nominally, CP interprets CLL's axiom as a forwarder process, which sends any message it receives over its input channel over its output channel. Operationally, CP's forwarders do not forward messages at all. Instead, they put their input and output channels together and terminate. This causes lots of trouble with CP's metatheory and its use as a model of concurrent computation.

    I propose an alternative operational semantics for forwarders which avoids this trouble and has an pleasant interpretation in CLL.

  6. Strong Rule Induction for Syntax with BindingsJan van Brügge • Heriot-Watt University    Slides

    When reasoning about inductively defined predicates over syntax with bindings, keeping bound variables fresh helps to reduce the complexity of the proofs. We have identified a general criteria when it is possible to strengthen the induction theorem derived from the knaster-tarski fixpoint underlying the inductive predicate to avoid bound variables. This criteria is not dependent on the syntactic format of the rules, and thus supports e.g. higher order relators and quantifiers in the predicate without requiring extra side conditions.

  7. A Tale of Two CompilersWim Vanderbauwhede • University of Glasgow    Slides

    This talk is about a side project I did on compiling Fortran to Uxn, a tiny stack-based VM with 64 kB memory and 8-bit instructions. The talk focuses on two languages: Fortran (naturally) and Funktal, a strict, statically typed functional language for Uxn; and on their compilers: a general purpose, "serious" source-to-source compiler for Fortran, and a custom, "frivolous" compiler from Funktal. The link between the two will become clear in the talk.