@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",

}