Curry-style types for nominal terms

Maribel Fernández, Murdoch Gabbay

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)


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 languageEnglish
Title of host publicationTypes for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers
Number of pages15
Volume4502 LNCS
Publication statusPublished - 2007
EventInternational Workshop on Types for Proofs and Programs, TYPES 2006 - Nottingham, United Kingdom
Duration: 18 Apr 200621 Apr 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4502 LNCS
ISSN (Print)0302-9743


ConferenceInternational Workshop on Types for Proofs and Programs, TYPES 2006
Country/TerritoryUnited Kingdom


  • Binding
  • Polymorphism
  • Rewriting
  • Type inference


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

Cite this