Dependent types are showing up in more and more mainstream languages, but they can still seem like magic. In this workshop, we'll walk through one of the primary techniques for implementing a type checker for dependent types, called normalization by evaluation. We'll be implementing a little dependently typed language called Pie developed by Dan Friedman and myself.

The implementation is written entirely in a very small subset of Scheme, and I'll assume no knowledge beyond that gained by reading The Little Schemer.

Workshop goals:

 * Introduce the ideas behind normalization by evaluation and
   bidirectional type checking

 * Write a type checker for a little dependently typed language


 * Basic familiarity with and interest in dependent types, equivalent
   to having worked through the Idris tutorial [1]

 * Know enough Racket or Scheme to write an interpreter for a small
   Lisp-like language

 * Have a recent version of Racket installed on your laptop


How do systems built in Erlang, Elixir or any other BEAM Language differ from other systems? To start with:+ They are designed from the bottom up to run 'forever.’

  • They are designed from the bottom up to expect, and recover from errors.
  • They are expected to evolve.
  • They scale seamlessly 


How is all of this achieved? - the answer is simple - by making systems from sets of isolated communication processes, and by treating errors and code as first class objects that can be sent in messages over a network.

 In this tutorial, Joe Armstrong will introduce what he calls the `Erlang way of thinking.`  He will cover:  


  • Basic data types
  • Sequential Programming
  • Concurrent Programming


In Basic Data Types & Sequential Erlang he’ll introduce the foundations and talk about Modules, Functions and Pattern Matching. Once you've understood the basic pattern matching mechanism the rest is easy.

In concurrent programming he'll talk about processes and their life span. You will look at sending and receiving messages, selective reception, and passing data in the messages. Joe will conclude this section by introducing the simple but powerful error handling mechanisms in processes which help detect and isolate failure.

Time permitting, he will cover distribution, showing you how, by doing it right form the start or with very few changes, you can write a program intended to run on a single VM and distribute it in a cluster.

Tutorial objectives: To learn the Erlang way of thinking when architecting and developing systems.

Target audience: Developers and Architects interested in the principles which make Erlang, Elixir or other BEAM based languages unique.

Note: We we recommend you take this tutorial in conjunction with the OTP one in the afternoon.

While Erlang is a powerful programming language used to build distributed, fault tolerant systems with requirements of high availability, these complex systems require middleware in the form of reusable libraries, release, debugging and maintenance tools together with design principles and patterns used to style your concurrency model and your architecture.

In this tutorial, Robert will introduce the building blocks that form OTP, the defacto middleware that ships with the Erlang and Elixir distributions. He will cover OTP’s design principles, describing how they provide software engineering guidelines that enable developers to structure systems in a scalable and fault tolerant way, without the need to reinvent the wheel.

Tutorial objectives: To learn the Erlang way of thinking when architecting and developing systems.

Target audience: Developers and Architects interested in the principles which make Erlang, Elixir or other Beam based languages unique.

Level: Beginners and Intermediate

Note: We recommend you take this tutorial in conjunction with the one on thinking concurrently.

Live Coding systems encourage us to think extremely differently about programming languages and take ideas such as those found in reactive programming to the next level. For example, in addition to considering standard requirements such as reliability, efficiency and correctness we are also forced to deal with issues such as:

  • liveness,
  • concurrency,
  • coordination
  • determinism
  • time

What is it like to think fluently with such concepts? How might these ideas apply and benefit your development practices? The object of this highly interactive workshop is not to just cover these questions but give you your own initial experiences to draw from. Together, we'll learn how to work with all these imprtant concepts using Sonic Pi - whilst having a lot of productive fun.

Together we'll learn the basics of live coding through time using music as our guiding metaphor. However, we'll continually explore which domains other than music where live interaction and manipulation of running processes is both relevant and important.

Once we have mastered the basics of live coding with time, we will end the workshop by building a live distributed reactive event system that will enable us to collaboratively jam together.

This workshop is friendly and open to everyone. No programming knowledge is required, although the rabbit hole is so deep that seasoned programmers will still find many new things to learn and experience.

Note: this is the only workshop that will explore the principles of reactive programming whilst making sick beats.

Please come along with a laptop with Sonic Pi pre-installed (

Workshop Schedule

09:00-12:30 Thinking Concurrently
Joe Armstrong
Implementing Dependent Types
David Christiansen
12:30-13:30   Lunch
13:30-17:00 OTP, Middleware for
Concurrent Distributed Scalable Architectures

Robert Virding
Distributed Live Coding with Sonic Pi
Sam Aaron
*Once you have purchased your ticket, we will contact you regarding the workshops
you would like to attend.