BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Bringing Verification to Scala through Dependent Refinement Types
DTSTART:20170616T153000
DTEND:20170616T173000
DTSTAMP:20260407T105354Z
UID:9973a92cd7cb79ec7b574e994e8c366ad6d923f9900918a404c83467
CATEGORIES:Conferences - Seminars
DESCRIPTION:Georg Schmid\nEDIC candidacy exam\nExam president: Prof. Chris
 toph Koch\nThesis advisor: Prof. Viktor Kuncak\nCo-examiner: Prof. Martin 
 Odersky\n\nAbstract\nDespite numerous advances in type systems\, program a
 nalysis and model checking\, the verification of software artifacts is sti
 ll the exception rather than the rule.\nDependent refinement types have em
 erged as a verification technique that allows for expressive specification
 s\, but retains the familiar user interface of types.\nIn recent work the 
 checking of such types has been delegated to SMT solvers\, allowing progra
 mmers to largely automate the verification of simple program properties\, 
 while aiding them in proving more complex ones.\n\nIn this report we surve
 y dependent refinement types in the functional setting and consequently pr
 opose how Scala can evolve to support them.\nWe start out by introducing t
 wo concrete incarnations of dependent refinement types\, LiquidTypes and t
 he type system of F*.\nWe then discuss how their techniques may be applied
  to languages featuring rich\, user-defined subtyping relations and object
 -oriented programming\, such as in Scala.\nTo this end\, we also explore t
 he extent to which type inference remains feasible in the presence of subt
 yping.\nDrawing on these insights\, we finally present our research propos
 al for dependent refinement types in Scala.\n\nBackground papers\nLiquid T
 ypes\; Rondon et al.\nDependent Types and Multi-monadic Effects in F*\; Sw
 amy et al.\nType Inference with Simple Subtypes\; Mitchell.
LOCATION:BC 329 https://plan.epfl.ch/?room==BC%20329
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR