BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Idris 2: Type Driven Development of Idris - Edwin Brady\, St Andre
 ws University 
DTSTART:20181127T110000Z
DTEND:20181127T120000Z
UID:TALK115510@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Idris is a general purpose pure functional programming languag
 e with dependent types. Dependent types allow types to be predicated on va
 lues\, meaning that some aspects of a program’s behaviour can be specifi
 ed precisely in the type. It is compiled\, with eager evaluation. Its feat
 ures are influenced by Haskell and ML\, and include:\n\n* Full dependent t
 ypes with dependent pattern matching\n* Simple foreign function interface 
 (to C)\n* Compiler-supported interactive editing: the compiler helps you w
 rite code using the types where clauses\, with rule\, simple case expressi
 ons\, pattern matching let and lambda bindings\n* Dependent records with p
 rojection and update\n* Interfaces (similar to type classes in Haskell)\n*
  Type-driven overloading resolution\ndo notation and idiom brackets\n* Ind
 entation significant syntax\n* Extensible syntax\n* Cumulative universes\n
 * Totality checking\n* Hugs style interactive environment\n\nIdris is a ge
 neral purpose functional programming language with full dependent types\, 
 building on state-of-the-art techniques in programming language research. 
 It encourages "Type Driven Development"\, in which we begin by stating a f
 unction's type\, and arrive at a working program by a series of refinement
 s.\n\nWe've been having lots of fun over the last couple of years investig
 ating the possibilities and limitations of type-driven development in Idri
 s. As we write larger programs\, though\, we're finding the implementation
  of Idris is showing the strain - and recently I decided the time was righ
 t to start again\, and implement Idris 2 in Idris. In this talk\, I'll giv
 e an introduction to type-driven development (in Idris 2) and report on pr
 ogress so far\, showing off the most interesting features which the new de
 sign enables. In particular\, I will show examples of how Idris 2 combines
  linear types and dependent types.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR