## Abstract

System E is a recently designed type system for the ?-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 implementing the choices via substitution. This paper uses expansion variables in a unification-based automatic type inference algorithm for System E that succeeds for every ß-normalizable ?-term. We have implemented and tested our algorithm and released our implementation publicly. Each step of our unification algorithm corresponds to exactly one ß-reduction step, and vice versa. This formally verifies and makes precise a step-for-step correspondence between type inference and ß-reduction. This also shows that type inference with intersection types and expansion variables can, in effect, carry out an arbitrary amount of partial evaluation of the program being analyzed.

Original language | English |
---|---|

Title of host publication | Proceedings of the Sixth ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, PPDP'04 |

Pages | 132-143 |

Number of pages | 12 |

Publication status | Published - 2004 |

Event | 14th International Symposium on Logic Based Program Synthesis and Transformation - Verona, Italy Duration: 26 Aug 2004 → 28 Aug 2004 |

### Conference

Conference | 14th International Symposium on Logic Based Program Synthesis and Transformation |
---|---|

Abbreviated title | LOPSTR 2004 |

Country/Territory | Italy |

City | Verona |

Period | 26/08/04 → 28/08/04 |

## Keywords

- Expansion variables
- Intersection types
- Lambda-calculus
- Type inference