### Abstract

We define a rank 1 polymorphic type system for nominal terms, where typing environments type atoms, variables and function symbols. The interaction between type assumptions for atoms and substitution for variables is subtle: substitution does not avoid capture and so can move an atom into multiple different typing contexts. We give typing rules such that principal types exist and are decidable for a fixed typing environment, a-equivalent nominal terms have the same types; a non-trivial result because nominal terms include explicit constructs for renaming atoms. We investigate rule formats to guarantee subject reduction. Our system is in a convenient Curry-style, so the user has no need to explicitly type abstracted atoms. © Springer-Verlag Berlin Heidelberg 2007.

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

Title of host publication | Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers |

Pages | 125-139 |

Number of pages | 15 |

Volume | 4502 LNCS |

Publication status | Published - 2007 |

Event | International Workshop on Types for Proofs and Programs, TYPES 2006 - Nottingham, United Kingdom Duration: 18 Apr 2006 → 21 Apr 2006 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 4502 LNCS |

ISSN (Print) | 0302-9743 |

### Conference

Conference | International Workshop on Types for Proofs and Programs, TYPES 2006 |
---|---|

Country | United Kingdom |

City | Nottingham |

Period | 18/04/06 → 21/04/06 |

### Keywords

- Binding
- Polymorphism
- Rewriting
- Type inference

## Fingerprint Dive into the research topics of 'Curry-style types for nominal terms'. Together they form a unique fingerprint.

## Cite this

*Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers*(Vol. 4502 LNCS, pp. 125-139). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4502 LNCS).