![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > General Purpose Programming with Dependent Types
General Purpose Programming with Dependent TypesAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsType the title of a new list here Artificial Intelligence and Natural Computation seminars Condensed Matter Physics SeminarsOther talksTBC The tragic destiny of Mileva Marić Einstein TBA Life : it’s out there, but what and why ? Waveform modelling and the importance of multipole asymmetry in Gravitational Wave astronomy Quantum Sensing in Space |