The next Talk @ DI will be presented by Edwin Brady, Lecturer at the University of St Andrews (UK) and Idris’ creator, in the follow up of the invitation addressed by Vasco Vasconcelos.
The lecture, with the same title of Brady’s book “Type-Driven Development with Idris”, will present how to improve the performance and accuracy of programs by taking advantage of a state-of-the-art type system, and will take place at January, 24th, 16:00h, at 6.2.44 room of FCUL’s C6 building.

Abstract:
Idris is a general purpose functional programming language with first-class dependent types, building on state-of-the-art techniques in programming language research. It aims to make type-based program verification techniques accessible to programming practitioners while supporting efficient systems programming via an optimising compiler and interaction with external libraries.
In this talk, I’ll demonstrate “Type-driven Development” in Idris, using a series of examples to show how types can be used for verifying realistic and important properties of software, from simple properties such as array bounds checking, to more complex properties of networked and concurrent systems.

Short Bio:

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.