@inproceedings{477491037f02433381cd6d49cf6978c4,
title = "Curry-style types for nominal terms",
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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",
keywords = "Binding, Polymorphism, Rewriting, Type inference",
author = "Maribel Fern{\'a}ndez and Murdoch Gabbay",
year = "2007",
language = "English",
isbn = "9783540744634",
volume = "4502 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "125--139",
booktitle = "Types for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers",
note = "International Workshop on Types for Proofs and Programs, TYPES 2006 ; Conference date: 18-04-2006 Through 21-04-2006",
}