General Purpose Programming with Dependent Types

Add to your list(s) Download to your calendar using vCal

• Edwin Brady, University of St Andrews
• Friday 10 January 2014, 16:00-17:00
• G42 Mechanical Engineering.

If you have a question about this talk, please contact Paul Levy.

Idris is an experimental functional programming language with full spectrum dependent types, meaning that types can be predicated on any value. Its syntax is influenced by Haskell. As well as full dependent types it supports records, type classes, tactic based theorem proving, totality checking, and an optimising compiler with a foreign function interface. One of the goals of the Idris project is to bring type-based program verification techniques to programming practitioners while still supporting efficient systems programming via an optimising compiler and interaction with external libraries.

In this talk I will introduce dependently typed programming using Idris, and demonstrate its features using several examples including verified compression by run-length encoding, management of state and side-effects and resource correctness proofs.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• G42 Mechanical Engineering
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.