Talk: (English)
Programming as a Conversation: Type-driven Development in Action
During development, programs spend most of their time in an incomplete state, and the act of programming is as much about the steps required to achieve a complete program as it is about the end result. Accordingly, it is helpful for language implementations and tools to support the editing process as well as check and compile the end result. Precise type systems can support this process by allowing a programmer to state up front certain important properties of a program. In this talk, I’ll demonstrate this idea by showing progress on a new implementation of Idris, a functional language with dependent types which builds in support for interactive type-driven development. I will give examples which demonstrate how dependent types support type directed program synthesis, and type safe concurrent programming.
Edwin Brady
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.
