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





The interactive transcript could not be loaded.


Rating is available when the video has been rented.
This feature is not available right now. Please try again later.
Published on Oct 19, 2016

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 http://www.twitter.com/lambda_world and http://www.twitter.com/47deg using #LambdaWorld.

Stay tuned to http://www.lambda.world and http://www.47deg.com for more on the conference and announcements for the 2017 event.

Comments are disabled for this video.
When autoplay is enabled, a suggested video will automatically play next.

Up next

to add this to Watch Later

Add to

Loading playlists...