Bibliography for Intersection Types and Related Systems

191 references, last updated Fri Nov 9 4:50:02 2012

[1]

Alexander S. Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In FPCA '93, Conf. Funct. Program. Lang. Comput. Arch., pages 31-41. ACM, 1993.

[2]

Alexander S. Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Conf. Rec. 21st Ann. ACM Symp. Princ. of Prog. Langs., pages 163-173, 1994.

[3]

F. Alessi and F. Barbanera. Strong conjunction and intersection types. In A. Tarlecki, editor, Proc. 16th Int'l Symp. Mathematical Foundations Computer Science (MFCS '91), volume 520 of Lecture Notes in Computer Science, pages 64-73. Springer, 1991.

[4]

Fabio Alessi and Mariangiola Dezani-Ciancaglini. Type preorders and recursive terms. In ITRS '04 [111], pages 3-21. The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci. (PDF)

[5]

Fabio Alessi and Stefania Lusin. Simple easy terms. In ITRS '02 [110]. The ITRS '02 proceedings appears as vol. 70, issue 1 of Elec. Notes in Theoret. Comp. Sci., 2003-02. (PDF)

[6]

F. Alessi, F. Barbanera, and M. Dezani-Ciancaglini. Intersection types and computational rules. In WoLLIC '03, volume 82 of ENTCS. Elsevier, August 2003. (PDF)

[7]

Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Tailoring filter models. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types '03, volume 3085 of LNCS, pages 17-33. Springer-Verlag, 2004. (PDF)

[8]

Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. Inverse limit models as filter models. In Delia Kesner, Femke van Raamsdonk, and J. B. Wells, editors, HOR '04, pages 3-25, Aachen, 2004. RWTH Aachen. (PDF)

[9]

Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Stefania Lusin. Intersection types and domain operators. Theoret. Comput. Sci., 316(1-3):25-47, 2004. (PDF)

[10]

Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoret. Comput. Sci., 355(2):108-126, 2006. (PDF)

[11]

Sandra Alves and Mário Florido. On the relation between rank-2 intersection types and simple types. In 2002 Joint Conference on Declarative Programming, APPIA-GULP-PRODE (AGP) 2002, 2002.

[12]

Torben Amtoft and Franklyn Turbak. Faithful translations between polyvariant flows and polymorphic types. In Programming Languages & Systems, 9th European Symp. Programming, volume 1782 of Lecture Notes in Computer Science, pages 26-40. Springer, 2000. (PostScript) (PDF)

[13]

Torben Amtoft and Franklyn 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 [12]. To appear Fall 2000, but a DRAFT version is available. (PostScript) (PDF)

[14]

Anindya Banerjee. A modular, polyvariant, and type-based closure analysis. In ICFP '97 [108], pages 1-10. (PostScript) (PDF)

[15]

F. Barbanera and U. de' Liguoro. Type assignment for mobile objects. In COMETA'03, ENTCS 104C. Elsevier, 2004. (PDF)

[16]

Franco Barbanera and Mariangiola Dezani-Ciancaglini. Intersection and union types. In TACS '91 [167], pages 651-674.

[17]

Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: Syntax and semantics. Inform. & Comput., 119:202-230, 1995.

[18]

F. Barbanera. Combining term rewriting and type assignment systems. In ICTCS '89 [109], pages 71-84. The ICTCS '89 proceedings are to appear in Foundations of Computer Science.

[19]

Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symbolic Logic, 48(4):931-940, 1983.

[20]

H[enrik] P[ieter] Barendregt. Lambda calculi with types. In S[amson] Abramsky, Dov M. Gabbay, and T[homas] S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 2, pages 117-309. Oxford University Press, 1992.

[21]

Alessandro Berarducci and Mariangiola Dezani-Ciancaglini. Infinite lambda -calculus and types. Theoret. Comput. Sci., 212(1-2):29-75, 1999. Gentzen (Rome, 1996).

[22]

E. Bosio and Simona Ronchi Della Rocca. Type synthesis for intersection type discipline. In ICTCS '89 [109], pages 109-122. The ICTCS '89 proceedings are to appear in Foundations of Computer Science.

[23]

Gérard Boudol and Pascal Zimmer. On type inference in the intersection type discipline. Draft available from 1st author's web page. Obsoleted by [24], February 2004.

[24]

Gérard Boudol and Pascal Zimmer. On type inference in the intersection type discipline. In ITRS '04 [111]. The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci.

[25]

Beatrice Capitani, Michele Loreti, and Betti Venneri. Hyperformulae, parallel deductions and intersection types. Electronic Notes in Theoretical Computer Science, 50, 2001. Proceedings of ICALP 2001 workshop: Bohm's Theorem: Applications to Computer Science Theory (BOTH 2001), Crete, Greece, 2001-07-13.

[26]

Felice Cardone and Mario Coppo. Two extensions of Curry's type inference system. In P. Odifreddi, editor, Logic and Computer Science, number 31 in the APIC Series, chapter 1, pages 19-75. Academic Press, 1990.

[27]

F. Cardone and M. Coppo. Type inference with recursive types: Syntax and semantics. Inform. & Comput., 92(1):48-80, May 1991.

[28]

Felice Cardone, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Combining type disciplines. Ann. Pure Appl. Logic, 66(3):197-230, 1994.

[29]

Sébastien Carlier and J. B. Wells. Type inference with expansion variables and intersection types in System E and an exact correspondence with beta -reduction. In Proc. 6th Int'l Conf. Principles & Practice Declarative Programming, 2004. Completely supersedes [Car+Wel:TIEV-2004]. (PDF)

[30]

Sébastien Carlier and J. B. Wells. Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. In ITRS '04 [111], pages 173-202. The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci. (PDF)

[31]

Sébastien Carlier and J. B. Wells. The algebra of expansion. Draft corresponding roughly to an ITRS 2008 workshop talk, March 2008. (PDF)

[32]

Sébastien Carlier, Jeff Polakow, J. B. Wells, and A. J. Kfoury. System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In Programming Languages & Systems, 13th European Symp. Programming, volume 2986 of Lecture Notes in Computer Science, pages 294-309. Springer, 2004. (PDF)

[33]

Sébastien Carlier. Polar type inference with intersection types and omega . In ITRS '02 [110]. (PostScript)

[34]

Adriana B. Compagnoni and Benjamin C. Pierce. Higher-order intersection types and multiple inheritance. Math. Structures Comput. Sci., 6(5):469-501, October 1996.

[35]

Robert L. Constable and Jason Hickey. Nuprl's class theory and its applications. Unpublished, 2000.

[36]

Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type-assignment for lambda terms. Archiv für Mathematische Logik, 19:139-156, 1978.

[37]

Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the lambda -calculus. Notre Dame J. Formal Logic, 21(4):685-693, 1980.

[38]

M. Coppo and M. Dezani-Ciancaglini. A fully abstract model for higher-order mobile ambients. In VMCAI 2002, volume 2294 of LNCS, pages 255-271, 2002. (PDF)

[39]

M. Coppo and P. Giannini. A complete type inference algorithm for simple intersection types. In 17th Colloq. Trees in Algebra and Programming, volume 581 of Lecture Notes in Computer Science, pages 102-123. Springer, 1992.

[40]

Mario Coppo and Paola Giannini. Principal types and unification for simple intersection type systems. Inform. & Comput., 122(1):70-96, 1995.

[41]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. Functional characterization of some semantic equalities inside ???-calculus. In H. A. Maurer, editor, Automata, Languages and Programming, Sixth Colloquium, volume 71 of Lecture Notes in Computer Science, pages 133-146, Graz, July 1979. Springer.

[42]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Principal type schemes and lambda -calculus semantics. In Hindley and Seldin [102], pages 535-560.

[43]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. Functional characters of solvable terms. Z. Math. Log. Grund. Math., 27(1):45-58, 1981.

[44]

Mario Coppo, Furio Honsell, Mariangiola Dezani-Ciancaglini, and Giuseppe Longo. Extended type structures and filter lambda models. In G. Lolli, G. Longo, and A. Marcja, editors, Logic Colloquium '82, pages 241-262. North-Holland, Florence, Italy, 1983.

[45]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms, and d_ infty -lambda-models. Inform. & Comput., 72(2):85-116, 1987.

[46]

M. Coppo, F. Damiani, and P. Giannini. Strictness, totality, and non-standard type inference. Theoret. Comput. Sci., 272(1-2):69-111, February 2002. (PostScript)

[47]

M. Coppo. An extended polymorphic type system for applicative languages. In P. Dembinski, editor, Mathematical Foundations of Computer Science 1980, Proceedings of the 9th Symposium, volume 88 of Lecture Notes in Computer Science, pages 194-204, Rydzyna, Poland, 1980. Springer.

[48]

Karl Crary. Simple, efficient object encoding using intersection types, 2000. CMU Internal Report.

[49]

Ferruccio Damiani and Paola Giannini. A decidable intersection type system based on relevance. In TACS '94 [168], pages 707-725.

[50]

F. Damiani and P. Giannini. Automatic useless-code detection and elimination for HOT functional programs. J. Funct. Programming, pages 509-559, 2000.

[51]

Ferruccio Damiani and Frédéric Prost. Detecting and removing dead-code using rank 2 intersection. In TYPES, pages 66-87, 1996.

[52]

Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. A filter model for mobile processes. Math. Structures Comput. Sci., 9(1):63-102, 1999.

[53]

F. Damiani. Typing local definitions and conditional expressions with rank 2 intersection. In Foundations Softw. Sci. & Comput. Structures, FOSSACS 2000, volume 1784 of Lecture Notes in Computer Science, pages 82-97. Springer, 2000. Superseded by  [55].

[54]

F. Damiani. Principal typings and true rank 2 intersection typable recursive definitions. Internal report. Superseded by  [59], October 2003. (PDF)

[55]

F. Damiani. Rank 2 intersection types for local definitions and conditional expressions. ACM Trans. on Prog. Langs. & Systs., 25(4):401-451, 2003. (PDF)

[56]

F. Damiani. Rank 2 intersection types for modules. In Proc. 5th Int'l Conf. Principles & Practice Declarative Programming, pages 67-78, 2003. (PDF)

[57]

Ferruccio Damiani. A conjunctive type system for useless-code elimination. Math. Structures Comput. Sci., 13:157-197, 2003.

[58]

F. Damiani. Rank-2 intersection and polymorphic recursion. In TLCA'05, volume 3461 of LNCS, pages 146-161. Springer, 2005. (PDF)

[59]

F. Damiani. Rank-2 intersection and polymorphic recursion (extended version with proofs). Internal report. Extended version with proofs of  [58], January 2005. (PDF)

[60]

U. de' Liguoro. Restricted intersection type assignment systems and object properties. December 2002. (PDF)

[61]

U. de' Liguoro. Subtyping in logical form. In Proceedings of ITRS'02, volume 70.1 of ENTCS, page 16, 2002. (PDF)

[62]

Ugo de'Liguoro. Characterizing convergent terms in object calculi via intersection types. In TLCA '01 [170].

[63]

M. Dezani-Ciancaglini and S. Ghilezan. Lambda models characterizing computational behaviours of terms. Schedae Informaticae, 12:35-49, June 2003. (PDF)

[64]

M. Dezani-Ciancaglini and S. Ghilezan. Two behavioural lambda models. In Types'02, volume 2246 of LNCS, pages 127-147. Springer-Verlag, 2003. (PDF)

[65]

Mariangiola Dezani-Ciancaglini and J. Roger Hindley. Intersection types for combinatory logic. Theoret. Comput. Sci., 100(2):303-324, 29 June 1992. A preliminary version is pp. 181-192 in  [129].

[66]

M. Dezani-Ciancaglini and S. Lusin. Intersection types and lambda theories. In WIT 2002, 2002. (PDF)

[67]

Mariangiola Dezani-Ciancaglini and I. Margaria. F-semantics for intersection type discipline. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Proc. Semantics of Data Types, International Symposium, volume 173 of LNCS, pages 279-300, Sophia-Antipolis, France, June 1984. Springer-Verlag.

[68]

Mariangiola Dezani-Ciancaglini and I. Margaria. A characterization of F-complete type assignments. Theoret. Comput. Sci., 45:121-157, 1986.

[69]

Mariangiola Dezani-Ciancaglini and Simona Ronchi Della Rocca. Intersection and reference types. In Erik Barendsen, Venanzio Capretta, Hermann Geuvers, and Milad Niqui, editors, Reflections on Type Theory, Lambda Calculus, and the Mind, pages 77-86. Radboud University Nijmegen, 2007.

[70]

Mariangiola Dezani-Ciancaglini and Makoto Tatsuta. A behavioural model for Klop's calculus. In Flavio Corradini and Carlo Toffalori, editors, Proceedings of the Workshop on Logic, Models and Computer Science (LMCS 2006), volume 169 of ENTCS, pages 19-32, Camerino, Italy, 2007. Elsevier. (PDF)

[71]

Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Adolfo Piperno. Filter models for conjunctive-disjunctive lambda -calculi. Theoret. Comput. Sci., 170(1-2):83-128, 1996.

[72]

Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Betti Venneri. The ``relevance'' of intersection and union types. Notre Dame J. Formal Logic, 38(2):246-269, Spring 1997.

[73]

Mariangiola Dezani-Ciancaglini, Jerzy Tiuryn, and Pawel Urzyczyn. Discrimination by parallel observers. In Proc. 12th Logic in Computer Science, 1997.

[74]

Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, and Adolfo Piperno. A filter model for concurrent lambda -calculus. SIAM J. Comput., 27(5):1376-1419 (electronic), 1998.

[75]

Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterization of lambda-terms using intersection types. In M. Nielsen and B. Rovan, editors, Mathematical Foundations of Computer Science 2000, volume 1893 of Lecture Notes in Computer Science, pages 304-313. Springer, 2000.

[76]

M. Dezani-Ciancaglini, A. Frisch, E. Giovannetti, and Y. Motohama. The relevance of semantic subtyping. In ITRS 2002, volume 70.1 of ENTCS. Elsevier, 2002. (PDF)

[77]

M. Dezani-Ciancaglini, F. Honsell, and F. Alessi. A complete characterization of complete intersection-type preorders. ACM Transactions on Logic and Computation, 4(1):120-147, January 2003. (PDF)

[78]

Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, and Silvia Likavec. Behavioural inverse limit lambda -models. Theoret. Comput. Sci., 316(1-3):49-74, 2004. (PDF)

[79]

Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, and Makoto Tatsuta. On isomorphisms of intersection types. In Michael Kaminski and Simone Martini, editors, Proc. 17th EACSL Ann. Conf. Computer Science Logic, volume 5213 of Lecture Notes in Computer Science, pages 461-492, Bertinoro, Italy, 2008. Springer. (PDF)

[80]

Mariangiola Dezani, Robert Meyer, and Yoko Motohama. The semantics of entailment omega. Notre Dame J. Formal Logic, 43(3):129-145, 2002. (PDF)

[81]

M. Dezani. Finitary logical semantics (abstract). The Bulletin of Symbolic Logic, 9(2):257-258, 2003. (PDF)

[82]

M. Dezani. Intersection types and observational equivalence. In HOR 2004, 2004.

[83]

Allyn Dimock, Robert Muller, Franklyn Turbak, and J. B. Wells. Strongly typed flow-directed representation transformations. In ICFP '97 [108], pages 11-24. (PostScript)

[84]

Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and Jeffrey Considine. Space issues in compiling with intersection and union types. In Preliminary Proceedings of the Third Workshop on Types in Compilation (TIC 2000), 2000. Superseded by  [86].

[85]

Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, and J. B. Wells. Functioning without closure: Type-safe customized function representations for Standard ML. In Proc. 6th Int'l Conf. Functional Programming, pages 14-25. ACM Press, 2001. (PDF)

[86]

Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and Jeffrey Considine. Program representation size in an intermediate language with intersection and union types. In Types in Compilation, Third Int'l Workshop, TIC 2000, volume 2071 of Lecture Notes in Computer Science, pages 27-52. Springer, 2001.

[87]

Allyn Dimock, Ian Westmacott, Robert Muller, Franklyn Turbak, J. B. Wells, and Jeffrey Considine. Program representation size in an intermediate language with intersection and union types. Technical Report BUCS-TR-2001-02, Comp. Sci. Dept., Boston Univ., March 2001. This is a version of [86] extended with an appendix describing the CIL typed intermediate language. (PostScript) (PDF)

[88]

D. Dougherty and P. Lescanne. Reductions, intersection types, and explicit substitution. In TLCA '01 [170], pages 121-135.

[89]

Eric Duquesne. Elimination des coupures et types principaux dans le système D omega . Presentation at ``Séminaire de lambda-calcul typé'' at Université Paris 7, November 1990. Quoted from Regnier  [Regnier:LCR-1992].

[90]

Lavinia Egidi, Furio Honsell, and Simona 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).

[91]

Jonathan Eifrig, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and its application to OOP. In Proc. 1995 Mathematical Foundations of Programming Semantics Conf., volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.

[92]

Mário Florido and Luís Damas. Linearization of the lambda-calculus and its relation with intersection type systems. J. Funct. Programming, 200X. To appear.

[93]

Jean Gallier. Typing untyped lambda-terms, or reducibility strikes again! Ann. Pure Appl. Logic, 91:231-270, 1998.

[94]

Philippa Gardner. Discovering needed reductions using type theory. In TACS '94 [168], pages 555-597.

[95]

Silvia Ghilezan. Inhabitation in intersection and union type assignment systems. J. Logic Comput., 3(6):671-685, December 1993.

[96]

Silvia Ghilezan. Strong normalization and typability with intersection types. Notre Dame J. Formal Logic, 37(1):44-52, Winter 1996.

[97]

Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. In Programming Languages & Systems, 12th European Symp. Programming, volume 2618 of Lecture Notes in Computer Science, pages 284-301. Springer, 2003. Superseded by [98]. (PDF)

[98]

Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Programming, 50:189-224, 2004. Supersedes [97]. (PDF)

[99]

Joseph J. Hallett and Assaf J. Kfoury. Programming examples needing polymorphic recursion. Technical Report BUCS-TR-2004-004, Department of Computer Science, Boston University, January 2004. (PostScript) (PDF)

[100]

Susumu Hayashi. Singleton, union and intersection types for program extraction. In TACS '91 [167], pages 701-730.

[101]

Susumu Hayashi. Singleton, union and intersection types for program extraction. Inform. & Comput., 109(1/2):174-210, February/March 1994.

[102]

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

[103]

J. R. Hindley. The simple semantics for Coppo-Dezani-Sallé types. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, volume 137 of LNCS, pages 212-226, Turin, April 1982. Springer-Verlag.

[104]

J. Roger Hindley. Coppo-Dezani types do not correspond to propositional logic. Theoret. Comput. Sci., 28(1-2):235-236, January 1984.

[105]

Furio Honsell and Marina Lenisa. Semantical analysis of perpetual strategies in lambda -calculus. Theoret. Comput. Sci., 212(1-2):183-209, 6 February 1999.

[106]

F. Honsell and Simona Ronchi Della Rocca. Reasoning about interpretation in qualitative lambda models. In IFIP TC2 Working Conference on Programming Concepts and Methods 1990, pages 492-508. North-Holland, 1991.

[107]

Furio Honsell and Simona 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.

[108]

Proc. 1997 Int'l Conf. Functional Programming. ACM Press, 1997.

[109]

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.

[110]

Proceedings of the 2nd Workshop on Intersection Types and Related Systems, 2002. The ITRS '02 proceedings appears as vol. 70, issue 1 of Elec. Notes in Theoret. Comp. Sci., 2003-02.

[111]

Proc. 3rd Int'l Workshop Intersection Types & Related Systems (ITRS 2004), 2005. The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci.

[112]

B. Jacobs, I. Margaria, and M. Zacchi. Filter models with polymorphic types. Theoret. Comput. Sci., 95:143-158, 1992.

[113]

T. P. Jensen. Conjunctive type systems and abstract interpretation of higher order functional programming languages. J. Logic Comput., 5(4):397-421, 1995.

[114]

Thomas Jensen. Inference of polymorphic and conditional strictness properties. In POPL '98 [148].

[115]

Trevor Jim. Rank 2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531, Massachusetts Institute of Technology, November 1995. (PostScript) (PDF)

[116]

Trevor Jim. What are principal typings and what are they good for? Tech. memo. MIT/LCS/TM-532, MIT, 1995. (PostScript) (PDF)

[117]

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

[118]

Assaf J. Kfoury and J. B. Wells. New notions of reduction and non-semantic proofs of beta -strong normalization in typed lambda -calculi. Tech. Rep. 94-014, Boston Univ. Comp. Sci. Dept., 1994. (PostScript)

[119]

A. J. Kfoury and J. B. Wells. New notions of reduction and non-semantic proofs of beta -strong normalization in typed lambda -calculi. In Proc. 10th Ann. IEEE Symp. Logic in Comput. Sci., pages 311-321, 1995. (PostScript) (PDF)

[120]

Assaf J. Kfoury and J. B. Wells. Addendum to ``New notions of reduction and non-semantic proofs of beta -strong normalization in typed lambda -calculi''. Tech. Rep. 95-007, Comp. Sci. Dept., Boston Univ., 1995. (PostScript)

[121]

Assaf J. Kfoury and 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., pages 161-174, 1999. Superseded by [122]. (PostScript)

[122]

Assaf J. Kfoury and J. B. Wells. Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci., 311(1-3):1-70, 2004. Supersedes [121]. For omitted proofs, see the longer report [Kfo+Wel:PTI-2003]. (PDF)

[123]

Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, and J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int'l Conf. Functional Programming, pages 90-101. ACM Press, 1999. (PostScript)

[124]

Assaf J. Kfoury, Geoff Washburn, and J. B. Wells. Implementing compositional analysis using intersection types with expansion variables. In ITRS '02 [110]. (PDF)

[125]

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

[126]

Assaf J. Kfoury. Beta-reduction as unification. In D. Niwinski, editor, Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference, December 1996), Banach Center Publication, Volume 46, pages 137-158. Springer-Verlag, 1999. Supersedes  [125] but omits a few proofs included in the latter. (PostScript) (PDF)

[127]

Assaf J. Kfoury. Beta-reduction as unification. In D. Niwinski, editor, Logic, Algebra, and Computer Science (H. Rasiowa Memorial Conference, December 1996), Banach Center Publication, Volume 46, pages 137-158. Springer-Verlag, 1999. (PostScript) (PDF)

[128]

Assaf J. Kfoury. A linearization of the lambda-calculus. J. Logic Comput., 10(3):411-436, 2000. Special issue on Type Theory and Term Rewriting. Kamareddine and Klop (editors). (PostScript) (PDF)

[129]

J. W. Klop et al., editors. J.W. de Bakker, 25 Jaar Semantiek. Centrum voor Wiskunde en Informatica, Amsterdam, 1989.

[130]

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

[131]

Daniel Leivant. Polymorphic type inference. In Conf. Rec. 10th Ann. ACM Symp. Princ. of Prog. Langs., pages 88-98, 1983.

[132]

Daniel Leivant. Typing and computational properties of lambda expressions. Theoret. Comput. Sci., 44(1):51-68, 1986.

[133]

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

[134]

Stéphane Lengrand, Pierre Lescanne, Daniel J. Dougherty, Mariangiola Dezani-Ciancaglini, and Steffen van Bakel. Intersection types for explicit substitutions. Inform. & Comput., 189(1):17-42, 2004. (PDF)

[135]

Luigi Liquori and Simona Ronchi Della Rocca. Towards an intersection typed system textit á la Church. In ITRS '04 [111]. The ITRS '04 proceedings appears as vol. 136 (2005-07-19) of Elec. Notes in Theoret. Comp. Sci. (PDF)

[136]

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

[137]

E. K. G. Lopez-Escobar. Proof-functional connectives. In C. Di Prisco, editor, Methods of Mathematical Logic, Proceedings of the 6th Latin-American Symposium on Mathematical Logic, Caracas 1983, volume 1130 of Lecture Notes in Mathematics, pages 208-221. Springer-Verlag, 1985.

[138]

I. Margaria and M. Zacchi. Principal typing in a forall cap -discipline. J. Logic Comput., 5(3):367-381, 1995.

[139]

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

[140]

Peter Møller Neergaard and Harry G. Mairson. Rank bounded intersection: Types, potency, and idempotency. This paper is obsolete and has been replaced with [Nee-Mai-icfp-2004], 2003. (PostScript) (PDF)

[141]

Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. In POPL '98 [148], pages 197-208. Superseded by [142].

[142]

Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Programming, 11(3):263-317, May 2001.

[143]

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

[144]

Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, February 1991.

[145]

Benjamin C. Pierce. Intersection types and bounded polymorphism. In Proc. Int'l Conf. Typed Lambda Calculi and Applications. Springer, 1993.

[146]

Benjamin C. Pierce. Intersection types and bounded polymorphism. Math. Structures Comput. Sci., 7(2):129-193, April 1997.

[147]

G. Plotkin. A semantics for type checking. In TACS '91 [167], pages 1-17.

[148]

Conf. Rec. POPL '98: 25th ACM Symp. Princ. of Prog. Langs., 1998.

[149]

Garrel Pottinger. A type assignment for the strongly normalizable lambda -terms. In Hindley and Seldin [102], pages 561-577.

[150]

Christian Retoré. A note on intersection types. Technical Report RR-2431, INRIA, January 31 1995.

[151]

John C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345-372. North-Holland, 1981.

[152]

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

[153]

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

[154]

J. C. Reynolds. Syntactic control of interference, part 2. In G. Ausiello, M. Dezani, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, Proceedings, volume 372 of Lecture Notes in Computer Science, pages 704-722. Springer, July 1989.

[155]

J. C. Reynolds. The coherence of languages with intersection types. In TACS '91 [167], pages 675-700.

[156]

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

[157]

John 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, December 2000. (PostScript) (PDF) (DVI)

[158]

John 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. (PostScript) (DVI)

[159]

Simona Ronchi Della Rocca and Luca Roversi. Intersection logic. In Computer Science Logic, CSL '01, pages 414-428. Springer, 2001.

[160]

Simona Ronchi Della Rocca and Betti Venneri. Principal type schemes for an extended type theory. Theoret. Comput. Sci., 28(1-2):151-169, January 1984.

[161]

Simona Ronchi Della Rocca. Characterization theorems for a filter lambda model. Information and Control, 54:201-216, 1982.

[162]

Simona Ronchi Della Rocca. Principal type schemes and unification for intersection type discipline. Theoret. Comput. Sci., 59(1-2):181-209, March 1988.

[163]

Simona Ronchi Della Rocca. Intersection typed lambda-calculus. In ITRS 2002, volume 70.1 of ENTCS. Elsevier, 2002. (PDF)

[164]

Patrick Sallé. Une extension de la théorie des types en lambda -calcul. In G. Ausiello and Corrado Böhm, editors, Fifth International Conference on Automata, Languages and Programming, volume 62 of Lecture Notes in Computer Science, pages 398-410. Springer, July 1978.

[165]

Émilie Sayag and Michel Mauny. A new presentation of the intersection type discipline through principal typings of normal forms. Technical Report RR-2998, INRIA, October 16, 1996.

[166]

Émilie Sayag and Michel Mauny. Structural properties of intersection types. In Proceedings of the 8th International Conference on Logic and Computer Science -- Theoretical Foundations of Computing (LIRA), pages 167-175, Novi Sad, Yugoslavia, September 1997.

[167]

Theoretical Aspects Comput. Softw. : Int'l Conf., volume 526 of Lecture Notes in Computer Science. Springer, 1991.

[168]

Theoretical Aspects Comput. Softw. : Int'l Conf., volume 789 of Lecture Notes in Computer Science. Springer, 1994.

[169]

Makoto Tatsuta and Mariangiola Dezani-Ciancaglini. Normalisation is insensible to lambda-term identity or difference. In Rajeev Alur, editor, Proc. 21st Ann. IEEE Symp. Logic in Comput. Sci., pages 327-336. IEEE Comput. Soc. Press, 2006. (PDF)

[170]

5th Int'l Conf. Typed Lambda Calculi and Applications, volume 2044 of Lecture Notes in Computer Science, Kraków, Poland, 2-5 May 2001. Springer.

[171]

Valery Trifonov and Scott Smith. Subtyping constrained types. In Proc. 3rd Int'l Static Analysis Symp., pages 349-365, 1996.

[172]

Franklyn Turbak, Allyn Dimock, Robert Muller, and J. B. Wells. Compiling with polymorphic and polyvariant flow types. In Proc. First Int'l Workshop on Types in Compilation, June 1997. (PostScript)

[173]

Pawel Urzyczyn. The emptiness problem for intersection types. In Proc. 9th Ann. IEEE Symp. Logic in Comput. Sci., pages 300-309, 1994.

[174]

Silvio Valentini and Matteo Viale. A binary modal logic for the intersection types of lambda-calculus. Inform. & Comput., 185, 2003.

[175]

Silvio Valentini. An elementary proof of strong normalization for intersection types. Arch. Math. Logic, 40(7):475-488, October 2001.

[176]

S. van Bakel and U. de' Liguoro. Logical semantics for the first order sigma-calculus. In ICTCS'03, volume 2841 of LNCS, pages 202-215. Springer-Verlag, October 2003. (PDF)

[177]

S. van Bakel and M. Dezani-Ciancaglini. Characterizing strong normalization for explicit substitutions. In LATIN'02, volume 2286 of LNCS, pages 356-370. Springer-Verlag, 2002. (PDF)

[178]

Steffen J. van Bakel. Complete restrictions of the intersection type discipline. Theoret. Comput. Sci., 102(1):135-163, 1992.

[179]

Steffen J. van Bakel. Essential intersection type assignment. In Proc. FST&TCS '93, 13th Conf. Foundations of Software Technology and Theoret. Comput. Sci., volume 761 of Lecture Notes in Computer Science, pages 13-23. Springer, 1993. Superseded by [182].

[180]

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

[181]

Steffen J. van Bakel. Principal type schemes for the strict type assignment system. J. Logic Comput., 3(6):643-670, December 1993.

[182]

Steffen J. van Bakel. Intersection type assignment systems. Theoret. Comput. Sci., 151(2):385-435, 27 November 1995.

[183]

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

[184]

Betti Venneri. Intersection types as logical formulae. J. Logic Comput., 4(2):109-124, April 1994.

[185]

J. B. Wells and Christian Haack. Branching types. In Programming Languages & Systems, 11th European Symp. Programming, volume 2305 of Lecture Notes in Computer Science, pages 115-132. Springer, 2002. Completely superseded by [186]. (PDF)

[186]

J. B. Wells and Christian Haack. Branching types. Inform. & Comput., 200X. Completely supersedes [185]. Accepted subject to revisions. (PDF)

[187]

J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A typed intermediate language for flow-directed compilation. In Proc. 7th Int'l Joint Conf. Theory & Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 757-771, 1997. Superseded by [188]. (PostScript) (PDF)

[188]

J. B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 12(3):183-227, May 2002. Supersedes [187]. (PDF)

[189]

J. B. Wells. The essence of principal typings. A longer version of [190] with a 3-page appendix with extra proofs, a page of extra discussion of non-related work, and other minor changes, 2002. (PDF)

[190]

J. B. Wells. The essence of principal typings. In Proc. 29th Int'l Coll. Automata, Languages, and Programming, volume 2380 of Lecture Notes in Computer Science, pages 913-925. Springer, 2002. (PDF)

[191]

Hirofumi Yokouchi. Embedding a second order type system into an intersection type system. Inform. & Comput., 117(2):206-220, 1995.