Nominal essential intersection types. (English) Zbl 1395.68081
Summary: Nominal systems are an alternative approach for the treatment of variables in computational systems, where first-order syntax is generalised to provide support for the specification of binding operators. In this work, an intersection type system is presented for nominal terms. The subject reduction property is shown to hold for a specialised notion of typed nominal rewriting, thus ensuring preservation of types under computational execution.
MSC:
| 68N15 | Theory of programming languages |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q42 | Grammars and rewriting systems |
Keywords:
nominal syntax; nominal rewriting; binding; essential intersection types; subject reductionReferences:
| [1] | Ayala-Rincón, M.; Kamareddine, F., Unification via the \(\lambda s_e\)-style of explicit substitution, Log. J. IGPL, 9, 4, 489-523, (2001) · Zbl 0987.03012 |
| [2] | van Bakel, S., Essential intersection type assignment, (Foundations of Software Technology and Theoretical Computer Science, 13th Conference, Bombay, India, December 15-17, 1993, Proceedings, (1993)), 13-23 · Zbl 0924.03027 |
| [3] | van Bakel, S., Intersection type assignment systems, Theoret. Comput. Sci., 151, 2, 385-435, (1995) · Zbl 0871.68031 |
| [4] | van Bakel, S., Strict intersection types for the lambda calculus, ACM Comput. Surv., 43, 3, 20, (2011) · Zbl 1293.68073 |
| [5] | van Bakel, S.; Barbanera, F.; Fernández, M., Rewrite systems with abstraction and beta-rule: types, approximants and normalization, (Programming Languages and Systems - ESOP’96, 6th European Symposium on Programming, Proceedings, Lecture Notes in Comput. Sci., vol. 1058, (1996), Springer Verlag), 387-403 |
| [6] | van Bakel, S.; Fernández, F., Normalization results for typeable rewrite systems, Inform. and Comput., 133, 2, 73-116, (1997) · Zbl 0877.68072 |
| [7] | Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A filter lambda model and the completeness of type assignment, J. Symbolic Logic, 48, 4, 931-940, (1983) · Zbl 0545.03004 |
| [8] | Barendregt, H. P.; Dekkers, W.; Statman, R., Lambda calculus with types. perspectives in logic, (2013), Cambridge University Press · Zbl 1347.03001 |
| [9] | Bernadet, A.; Lengrand, S., Non-idempotent intersection types and strong normalisation, Log. Methods Comput. Sci., 9, 4, (2013) · Zbl 1297.03010 |
| [10] | Castagna, G.; Dezani-Ciancaglini, M.; Giachino, E.; Padovani, L., Foundations of session types, (Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, (2009)), 219-230 |
| [11] | Cheney, J., A simple nominal type theory, Electron. Notes Theor. Comput. Sci., 228, 37-52, (2009) · Zbl 1337.03039 |
| [12] | Cheney, J., A dependent nominal type theory, Log. Methods Comput. Sci., 8, 1, (2012) · Zbl 1241.68046 |
| [13] | Coppo, M.; Dezani-Ciancaglini, M., A new type assignment for λ-terms, Arch. Math. Logic, 19, 1, 139-156, (1978) · Zbl 0418.03010 |
| [14] | Coppo, M.; Dezani-Ciancaglini, M.; Venneri, B., Functional characters of solvable terms, Math. Log. Q., 27, 26, 45-58, (1981) · Zbl 0479.03006 |
| [15] | Dowek, G.; Hardin, T.; Kirchner, C., Higher-order unification via explicit substitutions, Inform. and Comput., 157, 1/2, 183-235, (2000) · Zbl 1005.03016 |
| [16] | Dunfield, J., Elaborating intersection and union types, J. Funct. Programming, 24, 2-3, 133-165, (2014) · Zbl 1297.68049 |
| [17] | Espírito Santo, J.; Ivetic, J.; Likavec, S., Characterising strongly normalising intuitionistic terms, Fund. Inform., 121, 1-4, 83-120, (2012) · Zbl 1277.03003 |
| [18] | Fairweather, E., Type systems for nominal terms, (2014), King’s College London, Ph.D. thesis |
| [19] | Fairweather, E.; Fernández, M., Typed nominal rewriting, ACM Trans. Comput. Log., 19, 1, 6:1-6:46, (2018) · Zbl 1407.68240 |
| [20] | Fairweather, E.; Fernández, M.; Gabbay, M. J., Principal types for nominal theories, (International Symposium on Fundamentals of Computation Theory FCT, Lecture Notes in Comput. Sci., vol. 6914, (2011), Springer Verlag), 160-172 · Zbl 1241.68048 |
| [21] | Fairweather, E.; Fernández, M.; Szasz, N.; Tasistro, A., Dependent types for nominal terms with atom substitutions, (13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland., (2015)), 180-195 · Zbl 1433.03070 |
| [22] | Fernández, M.; Gabbay, M. J., Curry-style types for nominal terms, (Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, (2006)), 125-139, Revised Selected Papers · Zbl 1178.68150 |
| [23] | Fernández, M.; Gabbay, M. J., Nominal rewriting, Inform. and Comput., 205, 6, 917-965, (2007) · Zbl 1118.68075 |
| [24] | Gabbay, M. J.; Pitts, A. M., A new approach to abstract syntax involving binders, (14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, (1999)), 214-224 |
| [25] | Ghilezan, S.; Ivetic, J.; Lescanne, P.; Likavec, S., Intersection types for the resource control lambda calculi, (Antonio Cerone, P. P., The 8th International Colloquium on Theoretical Aspects of Computing (ICTAC), Lecture Notes in Comput. Sci., vol. 6916, (2011), Springer-Verlag), 116-134 · Zbl 1351.03008 |
| [26] | Girard, J.-Y.; Lafont, Y.; Taylor, P., Proofs and types, Cambridge Tracts Theoret. Comput. Sci., vol. 7, (1989), Cambridge University Press · Zbl 0671.68002 |
| [27] | Hindley, J. R., Basic simple type theory, Cambridge Tracts Theoret. Comput. Sci., (2002), Cambridge University Press |
| [28] | Huet, G. P., A unification algorithm for typed \(\overset{\rightarrow}{\lambda}\)-calculus, Theoret. Comput. Sci., 1, 27-57, (1975) · Zbl 0337.68027 |
| [29] | Kamareddine, F.; Nour, K., A completeness result for a realisability semantics for an intersection type system, Ann. Pure Appl. Logic, 146, 2-3, 180-198, (2007) · Zbl 1127.03011 |
| [30] | Kesner, D.; Ventura, D., Quantitative types for the linear substitution calculus, (Díaz, J.; Lanese, I.; Sangiorgi, D., The 8th International Conference on Theoretical Computer Science (TCS), Lecture Notes in Comput. Sci., vol. 8705, (2014), Springer-Verlag), 296-310 · Zbl 1418.03180 |
| [31] | Kesner, D.; Ventura, D., A resource aware semantics for a focused intuitionistic calculus, Math. Structures Comput. Sci., 1-34, (2017) |
| [32] | Kfoury, A.; Wells, J. B., Principality and type inference for intersection types using expansion variables, Theoret. Comput. Sci., 311, 1-3, 1-70, (2004) · Zbl 1070.68021 |
| [33] | Kumar, R.; Norrish, M., (nominal) unification by recursive descent with triangular substitutions, (Interactive Theorem Proving, First International Conference, ITP 2010, Lecture Notes in Comput. Sci., vol. 6172, (2010), Springer Verlag), 51-66 · Zbl 1291.68356 |
| [34] | Lengrand, S.; Lescanne, P.; Dougherty, D. J.; Dezani-Ciancaglini, M.; van Bakel, S., Intersection types for explicit substitutions, Inform. and Comput., 189, 1, 17-42, (2004) · Zbl 1082.68014 |
| [35] | Padovani, L., On projecting processes into session types, Math. Structures Comput. Sci., 22, 2, 237-289, (2012) · Zbl 1277.68199 |
| [36] | Piccolo, M., Strong normalization in the π-calculus with intersection and union types, Fund. Inform., 121, 1-4, 227-252, (2012) · Zbl 1276.03028 |
| [37] | Pitts, A. M., Nominal logic, a first order theory of names and binding, Inform. and Comput., 186, 2, 165-193, (2003) · Zbl 1056.03014 |
| [38] | Pitts, A. M.; Matthiesen, J.; Derikx, J., A dependent type theory with abstractable names, Electron. Notes Theor. Comput. Sci., vol. 312, 19-50, (2015) · Zbl 1342.68054 |
| [39] | Stehr, M.-O., CINNI - a generic calculus of explicit substitutions and its application to λ- ς- and π-calculi, (The 3rd Int. Workshop on Rewriting Logic and its Applications, Electron. Notes Theor. Comput. Sci., vol. 36, (2000)), 70-92 |
| [40] | Urban, C.; Pitts, A. M.; Gabbay, M. J., Nominal unification, Theoret. Comput. Sci., 323, 1-3, 473-497, (2004) · Zbl 1078.68140 |
| [41] | Ventura, D. L.; Kamareddine, F.; Ayala-Rincón, M., Explicit substitution calculi with de Bruijn indices and intersection type systems, Log. J. IGPL, 23, 2, 295-340, (2015) · Zbl 1405.03037 |
| [42] | Wells, J. B., The essence of principal typings, (Widmayer, P.; Ruiz, F. T.; Bueno, R. M.; Hennessy, M.; Eidenbenz, S.; Conejo, R., The 29th International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Comput. Sci., vol. 2380, (2002), Springer Verlag), 913-925 · Zbl 1057.03023 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
