References

[AB91] F. Alessi, F. Barbanera. Strong conjunction and intersection types. In A. Tarlecki, ed., Proc. 16th Int’l Symp. Mathematical Foundations Computer Science (MFCS ’91), vol. 520 of LNCS, pp. 64–73. Springer-Verlag, 1991.

[AT00a] T. Amtoft, F. Turbak. Faithful translations between polyvariant flows and polymorphic types. In Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS, pp. 26–40. Springer-Verlag, 2000.

[AT00b] T. Amtoft, F. Turbak. Faithful translations between polyvariant flows and polymorphic types. Technical Report BUCS-TR-2000-01, Comp. Sci. Dept., Boston Univ., 2000. Expanded full report of [AT00a]. To appear Fall 2000, but a DRAFT version is available.

[AW93] A. S. Aiken, E. L. Wimmers. Type inclusion constraints and type inference. In FPCA ’93, Conf. Funct. Program. Lang. Comput. Arch., pp. 31–41. ACM, 1993.

[AWL94] A. S. Aiken, E. L. Wimmers, T. K. Lakshman. Soft typing with conditional types. In Conf. Rec. 21st Ann. ACM Symp. Princ. of Prog. Langs., pp. 163–173, 1994.

[Ban97] A. Banerjee. A modular, polyvariant, and type-based closure analysis. In ICFP ’97 [ICFP97].

[Bar89] F. Barbanera. Combining term rewriting and type assignment systems. In ICTCS ’89 [ICTCS89], pp. 71–84. The ICTCS ’89 proceedings are to appear in Foundations of Computer Science.

[Bar92] H. P. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, eds., Handbook of Logic in Computer Science, vol. 2, chapter 2, pp. 117–309. Oxford University Press, 1992.

[BCDC83] H. Barendregt, M. Coppo, M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4):931–940, 1983.

[BDC91] F. Barbanera, M. Dezani-Ciancaglini. Intersection and union types. In TACS ’91 [TACS91], pp. 651–674.

[BDCd95] F. Barbanera, M. Dezani-Ciancaglini, U. de’Liguoro. Intersection and union types: Syntax and semantics. Inform. & Comput., 119:202–230, 1995.

[BRDR89] E. Bosio, S. Ronchi Della Rocca. Type synthesis for intersection type discipline. In ICTCS ’89 [ICTCS89], pp. 109–122. The ICTCS ’89 proceedings are to appear in Foundations of Computer Science.

[CC90] F. Cardone, M. Coppo. Two extensions of Curry’s type inference system. In P. Odifreddi, ed., Logic and Computer Science, number 31 in the APIC Series, chapter 1, pp. 19–75. Academic Press, 1990.

[CDC78] M. Coppo, M. Dezani-Ciancaglini. A new type-assignment for lambda terms. Archiv für Mathematische Logik, 19:139–156, 1978.

[CDC80] M. Coppo, M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685–693, 1980.

[CDCS79] M. Coppo, M. Dezani-Ciancaglini, P. Sallé. Functional characterization of some semantic equalities inside ???-calculus. In H. A. Maurer, ed., Automata, Languages and Programming, Sixth Colloquium, vol. 71 of LNCS, pp. 133–146, Graz, July 1979. Springer-Verlag.

[CDCV80] M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Principal type schemes and λ-calculus semantics. In Hindley and Seldin [HS80], pp. 535–560.

[CDCV81] M. Coppo, M. Dezani-Ciancaglini, B. Venneri. Functional characters of solvable terms. Z. Math. Logik Grundlag. Math., 27(1):45– 58, 1981.

[CDCZ87] M. Coppo, M. Dezani-Ciancaglini, M. Zacchi. Type-theories, normal forms, and D*-lambda models. Inform. & Comput., 72:85–116, 1987.

[CDG02] M. Coppo, F. Damiani, P. Giannini. Strictness, totality, and nonstandard type inference. Theoret. Comput. Sci., 272(1-2):69–111, feb 2002.

[CG92] M. Coppo, P. Giannini. A complete type inference algorithm for simple intersection types. In 17th Colloq. Trees in Algebra and Programming, vol. 581 of LNCS, pp. 102–123. Springer-Verlag, 1992.

[CG95] M. Coppo, P. Giannini. Principal types and unification for simple intersection type systems. Inform. & Comput., 122(1):70–96, 1995.

[CH00] R. L. Constable, J. Hickey. Nuprl’s class theory and its applications. Unpublished, 2000.

[CHDCL83] M. Coppo, F. Honsell, M. Dezani-Ciancaglini, G. Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, A. Marcja, eds., Logic Colloquium ’82, pp. 241–262. North-Holland, Florence, Italy, 1983.

[Cop80] M. Coppo. An extended polymorphic type system for applicative languages. In P. Dembinski, ed., Mathematical Foundations of Computer Science 1980, Proceedings of the 9th Symposium, vol. 88 of LNCS, pp. 194–204, Rydzyna, Poland, 1980. Springer-Verlag.

[CP96] A. B. Compagnoni, B. C. Pierce. Higher-order intersection types and multiple inheritance. Math. Structures Comput. Sci., 6(5):469– 501, Oct. 1996.

[Cra00] K. Crary. Simple, efficient object encoding using intersection types, 2000. CMU Internal Report.

[DCGV97] M. Dezani-Ciancaglini, S. Ghilezan, B. Venneri. The “relevance” of intersection and union types. Notre Dame J. Formal Logic, 38(2):246–269, Spring 1997.

[DCH92] M. Dezani-Ciancaglini, J. R. Hindley. Intersection types for combinatory logic. Theoret. Comput. Sci., 100(2):303–324, 29 June 1992. A preliminary version is pp. 181–192 in [K^{+}89].

[DCM84] M. Dezani-Ciancaglini, I. Margaria. F-semantics for intersection type discipline. In G. Kahn, D. B. MacQueen, G. Plotkin, eds., Proc. Semantics of Data Types, International Symposium, vol. 173 of LNCS, pp. 279–300, Sophia-Antipolis, France, June 1984. Springer-Verlag.

[DCM86] M. Dezani-Ciancaglini, I. Margaria. A characterization of Fcomplete type assignments. Theoret. Comput. Sci., 45:121–157, 1986.

[DG00] F. Damiani, P. Giannini. Automatic useless-code detection and elimination for HOT functional programs. J. Funct. Programming, pp. 509–559, 2000.

[DL01] D. Dougherty, P. Lescanne. Reductions, intersection types, and explicit substitution. In 5th Int’l Conf. Typed Lambda Calculi and Applications, vol. 2044 of LNCS, pp. 121–135, Kraków, Poland, 2–5 May 2001. Springer-Verlag.

[DMTW97] A. Dimock, R. Muller, F. Turbak, J. B. Wells. Strongly typed flowdirected representation transformations. In ICFP ’97 [ICFP97], pp. 11–24.

[EHRDR92] L. Egidi, F. Honsell, S. Ronchi Della Rocca. Operational, denotational, and logical descriptions: A case-study. Fund. Inform., 16(2):149–169, 1992. Mathematical foundations of computer science ’91 (Kazimierz Dolny, 1991).

[Gar94] P. Gardner. Discovering needed reductions using type theory. In Theoretical Aspects Comput. Softw. : Int’l Conf., vol. 789 of LNCS. Springer-Verlag, 1994.

[Ghi93] S. Ghilezan. Inhabitation in intersection and union type assignment systems. J. Logic Comput., 3(6):671–685, Dec. 1993.

[Ghi96] S. Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Logic, 37(1):44–52, Winter 1996.

[Hay91] S. Hayashi. Singleton, union and intersection types for program extraction. In TACS ’91 [TACS91], pp. 701–730.

[Hay94] S. Hayashi. Singleton, union and intersection types for program extraction. Inform. & Comput., 109(1/2):174–210, February/March 1994.

[Hin82] J. R. Hindley. The simple semantics for Coppo-Dezani-Sallé types. In M. Dezani-Ciancaglini, U. Montanari, eds., International Symposium on Programming, 5th Colloquium, vol. 137 of LNCS, pp. 212–226, Turin, Apr. 1982. Springer-Verlag.

[Hin84] J. R. Hindley. Coppo-Dezani types do not correspond to propositional logic. Theoret. Comput. Sci., 28(1–2):235–236, Jan. 1984.

[HL99] F. Honsell, M. Lenisa. Semantical analysis of perpetual strategies in λ-calculus. Theoret. Comput. Sci., 212(1–2):183–209, 6 Feb. 1999.

[HRDR91] F. Honsell, S. Ronchi Della Rocca. Reasoning about interpretation in qualitative lambda models. In IFIP TC2 Working Conference on Programming Concepts and Methods 1990, pp. 492–508. North-Holland, 1991.

[HRDR92] F. Honsell, S. Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. J. Comput. System Sci., 45(1):49–75, 1992.

[HS80] J. R. Hindley, J. P. Seldin, eds. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980.

[ICFP97] Proc. 1997 Int’l Conf. Functional Programming. ACM Press, 1997.

[ICTCS89] Proc. Third Italian Conference on Theoretical Computer Science, Mantova, 1989. World Scientific Press. The ICTCS ’89 proceedings are to appear in Foundations of Computer Science.

[Jen98] T. Jensen. Inference of polymorphic and conditional strictness properties. In POPL ’98 [POPL98].

[Jim95a] T. Jim. Rank 2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531, Massachusetts Institute of Technology, Nov. 1995.

[Jim95b] T. Jim. What are principal typings and what are they good for? Tech. memo. MIT/LCS/TM-532, MIT, 1995.

[Jim96] T. Jim. What are principal typings and what are they good for? In Conf. Rec. POPL ’96: 23rd ACM Symp. Princ. of Prog. Langs., 1996.

[JMZ92] B. Jacobs, I. Margaria, M. Zacchi. Filter models with polymorphic types. Theoret. Comput. Sci., 95:143–158, 1992.

[K^{+}89] J. W. Klop, et al., eds. J.W. de Bakker, 25 Jaar Semantiek. Centrum voor Wiskunde en Informatica, Amsterdam, 1989.

[Kfo96] A. J. Kfoury. Beta-reduction as unification. A refereed extensively edited version is [Kfo99]. This preliminary version was presented at the Helena Rasiowa Memorial Conference, July 1996.

[Kfo99] A. J. Kfoury. Beta-reduction as unification. In D. Niwinski, ed., Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference, December 1996), Banach Center Publication, Volume 46, pp. 137–158. Springer-Verlag, 1999. Supersedes [Kfo96] but omits a few proofs included in the latter.

[Kfo00] A. J. Kfoury. A linearization of the lambda-calculus. J. Logic Comput., 10(3), 2000. Special issue on Type Theory and Term Rewriting. Kamareddine and Klop (editors).

[KMTW99] A. J. Kfoury, H. G. Mairson, F. A. Turbak, J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int’l Conf. Functional Programming, pp. 90–101. ACM Press, 1999.

[Kop00] A. Kopylov. Dependent intersection: A new way of defining records in type theory. Technical Report TR2000-1809, Dept. of Computer Science, Cornell University, 2000.

[KW95a] A. J. Kfoury, J. B. Wells. Addendum to “New notions of reduction and non-semantic proofs of β-strong normalization in typed λ-calculi”. Tech. Rep. 95-007, Comp. Sci. Dept., Boston Univ., 1995.

[KW95b] A. J. Kfoury, J. B. Wells. New notions of reduction and nonsemantic proofs of β-strong normalization in typed λ-calculi. In Proc. 10th Ann. IEEE Symp. Logic in Comput. Sci., pp. 311–321, 1995.

[KW99] A. J. Kfoury, J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Conf. Rec. POPL ’99: 26th ACM Symp. Princ. of Prog. Langs., pp. 161–174, 1999. Superseded by [KW0X].

[KW0X] A. J. Kfoury, J. B. Wells. Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci., 200X. Supersedes [KW99]. Accepted subject to revisions.

[LDL02] S. Lengrand, D. Dougherty, P. Lescanne. An improved system of intersection types for explicit substitutions. In R. Baeza-Yates, U. Montanari, N. Santoro, eds., Foundations of Information Technology in the Era of Network and Mobile Computing, 2nd IFIP Int’l Conf. on Theoret. Comput. Sci., pp. 511–524. Kluwer Academic Publishers, 2002.

[LE85a] E. K. G. Lopez-Escobar. On intuitionistic sentential connectives. Rev. Colombiana de Math., 19:117–130, 1985.

[LE85b] E. K. G. Lopez-Escobar. Proof-functional connectives. In C. Di Prisco, ed., Methods of Mathematical Logic, Proceedings of the 6th Latin-American Symposium on Mathematical Logic, Caracas 1983, vol. 1130 of Lecture Notes in Mathematics, pp. 208–221. Springer-Verlag, 1985.

[Lei83] D. Leivant. Polymorphic type inference. In Conf. Rec. 10th Ann. ACM Symp. Princ. of Prog. Langs., pp. 88–98, 1983.

[Min89] G. E. Mints. The completeness of provable realizability. Notre Dame J. Formal Logic, 30(3):420–441, 1989.

[MZ] I. Margaria, M. Zacchi. Principal typing in a polymorphicintersection type discipline. Submitted circa 1991, probably published by now.

[Pie91a] B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, 1991. Also tech report CMU-CS-91-205.

[Pie91b] B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.

[Pie97] B. C. Pierce. Intersection types and bounded polymorphism. Math. Structures Comput. Sci., 7(2):129–193, Apr. 1997.

[Plo91] G. Plotkin. A semantics for type checking. In TACS ’91 [TACS91], pp. 1–17.

[POPL98] Conf. Rec. POPL ’98: 25th ACM Symp. Princ. of Prog. Langs., 1998.

[Pot80] G. Pottinger. A type assignment for the strongly normalizable λ-terms. In Hindley and Seldin [HS80], pp. 561–577.

[PP98] J. Palsberg, C. Pavlopoulou. From polyvariant flow information to intersection and union types. In POPL ’98 [POPL98], pp. 197–208. Superseded by [PP01].

[PP01] J. Palsberg, C. Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Programming, 11(3):263– 317, May 2001.

[RDR82] S. Ronchi Della Rocca. Characterization theorems for a filter lambda model. Information and Control, 54:201–216, 1982.

[RDR88] S. Ronchi Della Rocca. Principal type schemes and unification for intersection type discipline. Theoret. Comput. Sci., 59(1–2):181– 209, Mar. 1988.

[RDRV84] S. Ronchi Della Rocca, B. Venneri. Principal type schemes for an extended type theory. Theoret. Comput. Sci., 28(1–2):151–169, Jan. 1984.

[Rey87] J. C. Reynolds. Conjunctive types and Algol-like languages (abstract of invited lecture). In Proc. 2nd Ann. Symp. Logic in Comput. Sci., p. 119, 1987.

[Rey88] J. C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, 1988. Superseded by [Rey96].

[Rey89] J. C. Reynolds. Syntactic control of interference, part 2. In G. Ausiello, M. Dezani, S. R. D. Rocca, eds., Automata, Languages and Programming, 16th International Colloquium, Proceedings, vol. 372 of LNCS, pp. 704–722. Springer-Verlag, July 1989.

[Rey91] J. C. Reynolds. The coherence of languages with intersection types. In TACS ’91 [TACS91], pp. 675–700.

[Rey96] J. C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon Univ., Pittsburgh, PA 15213, USA, June 28 1996.

[Rey00] J. C. Reynolds. The meaning of types — from intrinsic to extrinsic semantics. Research Series RS–00–32, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Dec. 2000.

[Rey01] J. C. Reynolds. What do types mean? — from intrinsic to extrinsic semantics. To appear in Essays on Programming Methodology, edited by Annabelle McIver and Carroll Morgan, to be published by Springer-Verlag, New York, 2001.

[Sal78] P. Sallé. Une extension de la théorie des types en λ-calcul. In G. Ausiello, C. Böhm, eds., Fifth International Conference on Automata, Languages and Programming, vol. 62 of LNCS, pp. 398– 410. Springer-Verlag, July 1978.

[SM96] É. Sayag, M. Mauny. A new presentation of the intersection type discipline through principal typings of normal forms. Technical Report RR-2998, INRIA, Oct. 16, 1996.

[SM97] É. Sayag, M. Mauny. Structural properties of intersection types. In Proceedings of the 8th International Conference on Logic and Computer Science – Theoretical Foundations of Computing (LIRA), pp. 167–175, Novi Sad, Yugoslavia, Sept. 1997.

[TACS91] Theoretical Aspects Comput. Softw. : Int’l Conf., vol. 526 of LNCS. Springer-Verlag, 1991.

[TDMW97] F. Turbak, A. Dimock, R. Muller, J. B. Wells. Compiling with polymorphic and polyvariant flow types. In Proc. First Int’l Workshop on Types in Compilation, June 1997.

[TS96] V. Trifonov, S. Smith. Subtyping constrained types. In Proc. 3rd Int’l Static Analysis Symp., pp. 349–365, 1996.

[Urz94] P. Urzyczyn. The emptiness problem for intersection types. In Proc. 9th Ann. IEEE Symp. Logic in Comput. Sci., pp. 300–309, 1994.

[vB92] S. J. van Bakel. Complete restrictions of the intersection type discipline. Theoret. Comput. Sci., 102(1):135–163, 1992.

[vB93a] S. J. van Bakel. Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Catholic University of Nijmegen, 1993.

[vB93b] S. J. van Bakel. Principal type schemes for the strict type assignment system. J. Logic Comput., 3(6):643–670, Dec. 1993.

[vB95] S. J. van Bakel. Intersection type assignment systems. Theoret. Comput. Sci., 151(2):385–435, 27 Nov. 1995.

[vB96] S. J. van Bakel. Rank 2 intersection type assignment in term rewriting systems. Fundamenta Informatica, 2(26), 1996.

[Ven94] B. Venneri. Intersection types as logical formulae. J. Logic Comput., 4(2):109–124, Apr. 1994.

[WDMT97] J. B. Wells, A. Dimock, R. Muller, F. Turbak. A typed intermediate language for flow-directed compilation. In Proc. 7th Int’l Joint Conf. Theory & Practice of Software Development, pp. 757–771, 1997. Superseded by [WDMT02].

[WDMT02] J. B. Wells, A. Dimock, R. Muller, F. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 12(3):183–227, May 2002. Supersedes [WDMT97].

[Yok91] H. Yokouchi. Embedding second order type system into intersection type system and its application to type inference. Internal report, I.B.M. Research Lab., Tokyo, Japan, 1991. Probably published somewhere by now.