addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwchatcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-crosscrosseditemptyheartfacebookfolderfullheartglobegmailgoogleimagesinstagramlinklocation-pinmagnifying-glassmailminusmoremuplabelShape 3 + Rectangle 1outlookpersonplusprice-ribbonImported LayersImported LayersImported Layersshieldstartrashtriangle-downtriangle-uptwitteruseryahoo

Idris: General Purpose Programming with Dependent Types

Speaker: Edwin Brady.

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 Edwin 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, finishing with (to the best of our knowledge!) the first ever dependently-typed arcade game...

Join or login to comment.

  • Derek W.

    Video uploaded at:

    February 3, 2014

  • James F.

    I'm only disappointed that I didn't see the arcade game (but perhaps that's because I turned up late :-)

    January 22, 2014

    • Ben C.

      It didn't get shown in the talk, but if you were one of the five people that turned up half an hour early, you would have seen it on screen for a few seconds...

      January 23, 2014

    • Alois C.

      I must say I largely preferred learning about the new effect system and the VI mode than leaning about that arcade game...

      January 23, 2014

  • @sleepyfox

    Sorry,not going to be able to make this tonight due to work. Have cancelled my RSVP so hopefully someone else can fill my place.

    January 22, 2014

  • Tim W.

    Sadly for me, I cannot attend this one

    January 22, 2014

  • Oliver C.

    "Will you attend?" C'mon, do I really have to answer that question?


    January 9, 2014

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy