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. α-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.
Research partially supported by the EPSRC (EP/D501016/1 “CANS”).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Baader, F., Snyder, W.: Unification Theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 8, vol. I, pp. 445–532. Elsevier Science, Amsterdam (2001)
van Bakel, S., Fernández, M.: Normalization results for typable rewrite systems. Information and Computation 133(2), 73–116 (1997)
Barbanera, F., Fernández, M.: Intersection type assignment systems with higher-order algebraic rewriting. Theoretical Computer Science 170, 173–207 (1996)
Barendregt, H.P.: Pairing without conventional constraints. Zeitschrift für mathematischen Logik und Grundlagen der Mathematik 20, 289–306 (1974)
Barendregt, H.P.: Lambda Calculi With Types. In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, Oxford University Press, Oxford (1992)
Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4), 931–940 (1983)
Berghofer, S., Urban, C.: A Head-to-Head Comparison of de Bruijn Indices and Names. In: LFMTP 2006, pp. 46–59 (2006)
Curry, H.B., Feys, R.: Combinatory Logic, vol. 1. North-Holland, Amsterdam (1958)
Damas, L.M.M., Milner, R.: Principal Type Schemes for Functional programs. In: Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, ACM Press, New York (1982)
Fernández, M., Gabbay, M.J., Mackie, I.: Nominal Rewriting Systems. In: PPDP 2004. ACM Symposium on Principles and Practice of Declarative Programming, ACM Press, New York (2004)
Fernández, M., Gabbay, M.J.: Nominal Rewriting with Name Generation: Abstraction vs. Locality. In: PPDP 2005. ACM Symposium on Principles and Practice of Declarative Programming, ACM Press, New York (2005)
Fernández, M., Gabbay, M.J.: Nominal Rewriting. Information and Computation (to appear), available from http://dx.doi.org/10.1016/j.ic.2006.12.002
Gabbay, M.J., Pitts, A.M.: A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13, 341–363 (2002)
Gabbay, M.J.: A Theory of Inductive Definitions with Alpha-Equivalence. PhD Thesis, Cambridge University (2000)
Girard, J.-Y.: The System F of Variable Types, Fifteen Years Later, Theoretical Computer Science 45 (1986)
Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)
Khasidashvili, Z.: Expression reduction systems. In: Tbisili. Proceedings of I.Vekua Institute of Applied Mathematics, vol. 36, pp. 200–220 (1990)
Klop, J.-W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems, introduction and survey. Theoretical Computer Science 121, 279–308 (1993)
Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192, 3–29 (1998)
Shinwell, M.R., Pitts, A.M., Gabbay, M.: FreshML: Programming with binders made simple. In: ICFP 2003, pp. 263–274 (2003)
Urban, C., Pitts, A.M., Gabbay, M.J.: Nominal unification. Theoretical Computer Science 323, 473–497 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fernández, M., Gabbay, M.J. (2007). Curry-Style Types for Nominal Terms. In: Altenkirch, T., McBride, C. (eds) Types for Proofs and Programs. TYPES 2006. Lecture Notes in Computer Science, vol 4502. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74464-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-74464-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74463-4
Online ISBN: 978-3-540-74464-1
eBook Packages: Computer ScienceComputer Science (R0)