Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Dependently typed functional programming in Idris, 2 of 3</h1> <div class='date'><time class="dtstart dt-start" title="2015-01-20T15:30:00" datetime="2015-01-20T15:30:00">Tuesday, January 20, 2015 from 3:30</time>–<time class="dtend dt-end" title="2015-01-20T16:30:00" datetime="2015-01-20T16:30:00">4:30pm</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202394717'><span class='fn org p-name'>Galois Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 Sw 6th Ave Ste 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20Sw%206th%20Ave%20Ste%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>abstract: Idris is a pure functional language with full dependent types. In this series of tech talks, Idris contributor David Christiansen will provide an introduction to programming in Idris as well as using its development tools. Topics to be covered include the basics of dependent types, embedding DSLs in Idris, Idris’s notion of type providers, a general outline of the implementation strategy, the C FFI, and the effects library. Each talk has an associated set of exercises as well as suggested projects for further learning. Participants are expected to be familiar with functional programming in either Haskell or an ML.</p> <p>bio: David Raymond Christiansen is a Ph.D. student at the IT University of Copenhagen. For the last few months, he has been an intern at Galois, working on verifiable elections and better user interfaces for DSLs. His interests include functional programming languages, domain-specific languages, and environments that make them useful. David has contributed features such as type providers and error reflection to the Idris language as well as significant parts of the Emacs-based IDE. Additionally, he is a co-host of The Type Theory Podcast.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2015/01/tech-talk-dependently-typed-functional-programming-idris-2-3/">Website</a></li> </ul> </div>