UWA Logo
  Faculty Home | School Home | Internal Page | Awesome Animations   
           
Home
About the School
Contact and People
Future Undergraduate Students
Prospective Postgraduates
Current Students
Current Postgraduates
Research
Research Areas Research Areas Research Areas
Research Seminars Research Seminars Research Seminars
20082008 2008 2008
20072007 2007 2007
20062006 2006 2006
20052005 2005 2005
20042004 2004 2004
20032003 2003 2003
20022002 2002 2002
20012001 2001 2001
20002000 2000 2000
19991999 1999 1999
19981998 1998 1998
School Research Conferences School Research Conferences School Conferences
Tech Reports Tech Reports Tech Reports
Distinguished Visitors Distinguished Visitors Distinguished Visitors
Research Opportunities for Students Research Opportunities for Students Research Opportunities ...
Research Project Suggestions Research Project Suggestions Research Project Sugges...
IT News
Awards
Industry Links and Prizes
School and IT Information
Other
Internal Information

Research Seminar - August 10, 2001

Seminar Announcement


Title: Verifying Program Invariants with Refinement Types
Speaker: Mr Rowan Davies
  Department of Computer Science & Software Engineering
University of Western Australia
Date: Friday 10th August, 2001
Time: 2.00pm
Venue: Room 1.24

Abstract:

In current programming languages there is a large gap between the minimal consistency guaranteed by type-checking and total correctness of a program, which generally cannot be established in practice. We present a system of refinement types which stops far short of full verification, but which allows many relevant and interesting program invariants to be formally expressed and verified. We illustrate why such a system requires both subtyping and intersection types, and investigate how these constructs interact with other language features such as exceptions and effects. Our concrete realization will be as an extension of ML, but the underlying design is quite robust and has been applied to other languages such as logical frameworks. While full inference of refinement types is decidable and principal types exist, it is neither feasible nor desirable in practice. We discuss why and present our current design for partial type reconstruction and its interaction with a module system. This is work stemming from a collaboration with Frank Pfenning, CMU.
Top of Page