Join Newsletter

The Dependently Typed Revolution

YOW! Lambda Jam 2019 - 15 May

Dependently typed programming languages have a more powerful type system, allowing types to impose arbitrarily complex constraints on the relationships between function inputs and outputs.

In this workshop, we will explore some theory of dependently typed programming, and then learn to use Idris, a dependently typed language, on a toy problem (proving that certain moves in the game Minesweeper are safe). We will then briefly look at an HTTP server written in Idris to learn how dependent types can be used to improve type safety in real world systems.

Andrew Miller

Lead Developer

REA Group

Andrew leads a team of software developers at REA Group who use Scala (amongst other technologies) to build systems that allow real estate agents to promote properties listed on<...

Workshop Details

Target Audience
Functional programmers who don’t yet know much about dependent types, and are ready to take type safety to the next level.
1 hour 30min

Learning Outcomes

Attendees can expect to learn what dependent types are, what formal verification is, and to know some basic concepts around of how dependent types can be applied to formally verify properties of functional programs in the real world.

Workshop Outline

  • I will start with an introduction of the definition of 'dependently typed', with some motivating examples.
  • I will then introduce the audience to the Curry-Howard Correspodence, and explain what consequence that has for proving things at the type level. I will also explain the concept of formal verification.
  • I will introduce Proofsweeper (, a mine-sweeper game where you have to formally prove in Idris that a square is or isn’t a mine before marking it, and will take the audience through a basic proof, explaining how formal proofs are constructed in practice.
  • After that point, I will demonstrate how http4idris uses dependent types to provide type safety for real world systems.


Experience with statically typed functional programming is assumed. No prior knowledge of dependently typed programming will be assumed.