Tech Talk: Fun with Dependent Types
March 17th, 2009 by Levent Erkok
The March 24th Galois Tech Talk was delivered by Aaron Tomb, titled “Fun with Dependent Types.”
- Date: Tuesday, March 24, 2009
- Time: 10:30am – 11:30am
- Location: Galois, Inc.
421 SW 6th Ave. Suite 300
(3rd floor of the Commonwealth Building)
Portland, OR 97204
Here are Aaron’s slides. Further material on this topic can be found on Kenn Knowles’s site.
Abstract: A number of dependently-typed programming languages exist, but many either restrict expressiveness or require extensive user input to deal with the undecidability of type checking. Languages such as Cayenne, lambda-H, and Sage have instead used a “best-effort” attempt to deal with this undecidability by attempting to type check programs, but potentially failing to prove valid programs type-correct.
One powerful (and undecidable) form of dependent typing is based on what are variously known as contract types, refinement types, or predicate subtypes. The lambda-H language uses refinement types alone, and Sage includes them as part of a “pure” type system that uses the same syntax to describe both terms and types.
An interesting recent result (by one of my friends from Santa Cruz) shows that while type checking for refinement types is undecidable, a form of type inference is decidable. It has the interesting property that if the input program is well-typed, then it has the inferred type. However, the algorithm does not determine whether the input program is, in fact, well-typed. Because it only decides one part of the type inference problem, the authors refer to it as “type reconstruction” instead.
I will talk about refinement types, existing techniques for checking them, and the basics of decidable refinement type reconstruction.
Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.
Leave a Reply
©2000–2010 Galois, Inc. All rights reserved. Terms of use. Contact Us