Curry-style types for nominal terms

Maribel Fernández, Murdoch Gabbay

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

10 Citations (Scopus)

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 languageEnglish
Title of host publicationTypes for Proofs and Programs - International Workshop, TYPES 2006, Revised Selected Papers
Pages125-139
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

Conference

ConferenceInternational Workshop on Types for Proofs and Programs, TYPES 2006
CountryUnited Kingdom
CityNottingham
Period18/04/0621/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

    Fernández, M., & Gabbay, M. (2007). Curry-style types for nominal terms. In 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).