Name
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. |
Year | Venue | Keywords |
|---|---|---|
2006 | TYPES | fixed typing environment,type abstracted atom,convenient curry-style,multiple different typing context,principal type,a-equivalent nominal term,typing environments type atom,curry-style type,polymorphic type system,type assumption,nominal term,type inference,rewriting,type system,polymorphism |
Field | DocType | Volume |
Subject reduction,Computer science,Nominal terms,Algorithm,Typing environment,Decidability,Type inference,Nominal type system,Theoretical computer science,Rewriting | Conference | 4502 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-74463-0 | 213 |
PageRank | References | Authors |
8.90 | 13 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maribel Fernández | 1 | 315 | 23.44 |
| Murdoch J. Gabbay | 2 | 944 | 50.91 |