BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Making programming with dependent types practical through better t
 ools
DTSTART:20170831T140000
DTEND:20170831T160000
DTSTAMP:20260407T035006Z
UID:766d5ccf8f8d02ba92ad304e2a89b9b8090491b66e5bb88ee0f6c56b
CATEGORIES:Conferences - Seminars
DESCRIPTION:Guillaume Martres\nEDIC candidacy exam\nExam president: Prof. 
 Arjen Lenstra\nThesis advisor: Prof. Martin Odersky\nCo-examiner: Prof. Vi
 ktor Kuncak\n\nAbstract\nTraditionally\, programming languages with more p
 owerful type systems have been considered less user-friendly\, as using th
 em require developers to familiarize themselves with many non-intuitive co
 ncepts. In this report we survey\ndependently- typed languages\, a particu
 larly advanced category of languages.\nWe show the practical benefits that
  dependent types bring\, the trade-offs associated with them\, and the pow
 erful interactive programming experience they enable. Finally\, we discuss
  how these systems can serve as a source of inspiration for our work on Sc
 ala\, guiding us to improve both the static guarantees and user experience
  of the language\n\nBackground papers\nWhy Dependent Types Matter\, by Tho
 rsten Altenkirch\, Conor McBridge and James McKinna\nA Tool for Automated 
 Theorem Proving in Agda\, by Fredrik Lindblad and Marcin Benke\nElaborator
  Reflection: Extending Idris in Idris\, by David Christiansen and Edwin Br
 ady
LOCATION:INR331 https://plan.epfl.ch/theme/generalite_thm_plan_public?lang
 =en&room=inr331&dim_floor=3&dim_lang=en&baselayer_ref=grp_backgrounds&tree
 _groups=centres_nevralgiques%2Cacces%2Cmobilite_reduite%2Censeigneme
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR