Extrinsic vs Intrinsic Specifications, and Subset Types
Event details
| Date | 08.06.2018 |
| Hour | 13:30 › 14:15 |
| Speaker | Dr. K. Rustan M. Leino |
| Location | |
| Category | Conferences - Seminars |
Abstract
There are many techniques of specifying programs and these techniques fall onto several axes. Along one axis, a function can be specified with a behavior (an intrinsic specification) or its behavior can be formulated as a lemma about the function (an extrinsic specification). There are advantages and disadvantages of both “-trinsicies”. For example, because intrinsic specifications are automatically available in all contexts, they are easier to use, but may for the same reason degrade prover performance. Along another axis, rather than writing validity conditions on data structures and proving that functions preserve these, some data-structure invariants can be baked into subset types (aka refinement types). An advantage with subset types is that they simplify parametricity, but they do so at the expense of a more complicated type system.
In this talk, I will lead a discussion of these techniques through showing a progression of development steps that give some of the advantages of each technique.
Bio
Dr. K. Rustan M. Leino is a Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work on formal methods and programming languages. He has a long history of building program verifiers for both mainstream languages and languages designed to enhance reasoning. His easy-to-use language and verifier Dafny are used in teaching at dozens of universities. Previously, Leino has held positions at Microsoft, Imperial College London, and DEC/Compaq. He has been named an ACM Fellow for his contributions to making program verification accessible and practical.
There are many techniques of specifying programs and these techniques fall onto several axes. Along one axis, a function can be specified with a behavior (an intrinsic specification) or its behavior can be formulated as a lemma about the function (an extrinsic specification). There are advantages and disadvantages of both “-trinsicies”. For example, because intrinsic specifications are automatically available in all contexts, they are easier to use, but may for the same reason degrade prover performance. Along another axis, rather than writing validity conditions on data structures and proving that functions preserve these, some data-structure invariants can be baked into subset types (aka refinement types). An advantage with subset types is that they simplify parametricity, but they do so at the expense of a more complicated type system.
In this talk, I will lead a discussion of these techniques through showing a progression of development steps that give some of the advantages of each technique.
Bio
Dr. K. Rustan M. Leino is a Senior Principal Engineer in the Automated Reasoning Group at Amazon Web Services. He is known for his work on formal methods and programming languages. He has a long history of building program verifiers for both mainstream languages and languages designed to enhance reasoning. His easy-to-use language and verifier Dafny are used in teaching at dozens of universities. Previously, Leino has held positions at Microsoft, Imperial College London, and DEC/Compaq. He has been named an ACM Fellow for his contributions to making program verification accessible and practical.
Practical information
- General public
- Free