University of Birmingham > Talks@bham > Theoretical computer science seminar > General Purpose Programming with Dependent Types

General Purpose Programming with Dependent Types

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.