Tech Reports Home Contact
Technical Report Series
Actions
Submit Report
Browse Reports
Information
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0012


TitleType Inference with Expansion Variables and Intersection Types in System E and an Exact Correspondence with Beta-Reduction
AuthorsSebastien Carlier, J.B. Wells
Date2004-01-19
AbstractSystem E is a recently designed type system for the lambda-calculus with intersection types and expansion variables. During automatic type inference, expansion variables allow postponing decisions about which non-syntax-driven typing rules to use until the right information is available and allow the choices to be implemented via substitution. This paper shows how expansion variables enable a unification-based automatic type inference algorithm for System E that finds a typing for every beta-normalizable lambda-term. We have implemented and tested our algorithm and made our implementation publicly available. We show that each step of our unification algorithm corresponds to exactly one beta-reduction step, and vice versa. This formally verifies and makes precise a correspondence between type inference and beta-reduction that before was only known informally at an intuitive level and only among those who work with intersection types.
GroupULTRA
Notes
Download

 

Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 Copyright Heriot-Watt University, Disclaimer