Type-driven Development of Communicating Systems in Idris by Edwin Brady

Idris is a functional programming language with dependent types, which supports ‘total’ functional programming. A function is total if, for all well-typed inputs, it gives either a complete result of a finite prefix of an infinite result, in finite time. Total functions give us strong guarantees about their behavior: for example functions can’t crash due to badly formed inputs, servers will always produce responses to requests. In this talk, I’ll show how Idris supports total programming, with a series of examples. As an extended example, I’ll show how to define a type for describing communicating concurrent systems which, by writing total functions, guarantees that concurrent programs will interact as intended.
About Edwin:
Edwin Brady is a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and domain-specific languages (DSLs). He is currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language. When he’s not doing that, you might find him playing Go (He’s about 1 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. He also perpetrated the whitespace programming language.
Follow @edwinbrady for more on his work and the book he alleges he’ll complete in 2038.
About Lambda World:
The 2016 Lambda World brought together Functional Programming enthusiasts from around the world for two days of presentations, hacking, networking, and a healthy dose of partying in Cadiz, Spain. Hosted by 47 Degrees, the event also featured a Typelevel Community Conference and a Scala Center Hackathon.
Join in on the conversation at / lambda_world and / 47deg using #LambdaWorld.
Stay tuned to www.lambda.world and www.47deg.com for more on the conference and announcements for the 2017 event.