When: Saturday, October 1st - 11:30 - 12:30
Type-driven Development of Communicating Systems in Idris
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 compete result of a finite prefix of an infinite result, in finite time. Total functions give us strong guarantees about their behaviour: 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.
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:
Lambda World takes place September 30th - October 1st, in Cadiz, Spain and is hosted by 47 Degrees in conjunction with the Scala and Java communities of Spain. The event is located at the Palacio de Congresos, an old tobacco factory near the beach. You can find more details at Lambda.world.