BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Extrinsic vs Intrinsic Specifications\, and Subset Types
DTSTART:20180608T133000
DTEND:20180608T141500
DTSTAMP:20260415T024321Z
UID:007aba7fa084fb44bddd4c20cf0e6814fb8c42cd14ee3443d16cec40
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr. K. Rustan M. Leino\nAbstract\nThere are many techniques of
  specifying programs and these techniques fall onto several axes. Along on
 e axis\, a function can be specified with a behavior (an intrinsic specifi
 cation) or its behavior can be formulated as a lemma about the function (a
 n extrinsic specification). There are advantages and disadvantages of both
  “-trinsicies”. For example\, because intrinsic specifications are aut
 omatically available in all contexts\, they are easier to use\, but may fo
 r the same reason degrade prover performance. Along another axis\, rather 
 than writing validity conditions on data structures and proving that funct
 ions preserve these\, some data-structure invariants can be baked into sub
 set types (aka refinement types). An advantage with subset types is that t
 hey simplify parametricity\, but they do so at the expense of a more compl
 icated type system.\nIn this talk\, I will lead a discussion of these tech
 niques through showing a progression of development steps that give some o
 f the advantages of each technique.\n\nBio\nDr. K. Rustan M. Leino is a Se
 nior Principal Engineer in the Automated Reasoning Group at Amazon Web Ser
 vices. He is known for his work on formal methods and programming language
 s. He has a long history of building program verifiers for both mainstream
  languages and languages designed to enhance reasoning. His easy-to-use la
 nguage and verifier Dafny are used in teaching at dozens of universities. 
 Previously\, Leino has held positions at Microsoft\, Imperial College Lond
 on\, and DEC/Compaq. He has been named an ACM Fellow for his contributions
  to making program verification accessible and practical.\n 
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR