Por Edwin Brady (University of St Andrews).
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.
Sponsor
Palestra financiada pelo LASIGE, através do financiamento do projeto estratégico da Unidade, com a referência FCT UID/CEC/00408/2013.
