\expandafter\ifx\csname href\endcsname\relax\newcommand{\href}[2]{#2}\fi
\newcommand{\etalchar}[1]{$^{#1}$}
 \newcommand{\bibnoop}[1]{} \newcommand{\bibvonmagic}[2]{#2}
  \newcommand{\bibsingleletter}[1]{#1}
\begin{thebibliography}{EHRDR92}
\expandafter\ifx\csname href\endcsname\relax
  \def\href#1#2{#2}\fi

\bibitem[AB91]{Ale+Bar:MFCS-1991}
\href{http://www.dimi.uniud.it/~alessi/}{F.~Alessi}, \href{http://www.dipmat.unict.it/~barba/}{F.~Barbanera}.
\newblock Strong conjunction and intersection types.
\newblock In A.~Tarlecki, ed., {\em Proc.\ 16th Int'l Symp.\ Mathematical
  Foundations Computer Science (MFCS '91)}, vol. 520 of {\em LNCS}, pp. 64--73.
  Springer-Verlag, 1991.

\bibitem[AT00a]{Amt+Tur:Faithful-ESOP-2000}
\href{http://www.cis.ksu.edu/~tamtoft/}{T.~Amtoft}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}.
\newblock
  \href{http://www.church-project.org/reports/Amt+Tur:Faithful-ESOP-2000.html}{Faithful translations between polyvariant flows and polymorphic types}.
\newblock In {\em Programming Languages \& Systems, 9th European Symp.\
  Programming}, vol. 1782 of {\em LNCS}, pp. 26--40. Springer-Verlag, 2000.

\bibitem[AT00b]{Amt+Tur:Faithful-TR-2000}
\href{http://www.cis.ksu.edu/~tamtoft/}{T.~Amtoft}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}.
\newblock
  \href{http://www.church-project.org/reports/electronic/Amt+Tur:Faithful-TR-2000.pdf}{Faithful translations between polyvariant flows and polymorphic
  types}.
\newblock Technical Report BUCS-TR-2000-01, Comp.\ Sci.\ Dept., Boston Univ.,
  2000.
\newblock Expanded full report of \cite{Amt+Tur:Faithful-ESOP-2000}. To appear
  Fall 2000, but a \emph{DRAFT} version is available.

\bibitem[AW93]{Aik+Wim:FPCA-1993}
\href{http://www.cs.berkeley.edu/~aiken/}{A.~S. Aiken}, E.~L. Wimmers.
\newblock \href{http://http.cs.berkeley.edu/~aiken/pubs.html}{Type inclusion
  constraints and type inference}.
\newblock In {\em FPCA '93, Conf.\ Funct.\ Program.\ Lang.\ Comput.\ Arch.},
  pp. 31--41. ACM, 1993.

\bibitem[AWL94]{Aik+Wim+Lak:POPL-1994}
\href{http://www.cs.berkeley.edu/~aiken/}{A.~S. Aiken}, E.~L. Wimmers, T.~K. Lakshman.
\newblock Soft typing with conditional types.
\newblock In {\em Conf.\ Rec.\ 21st Ann.\ {ACM} Symp.\ Princ.\ of\ \ Prog.\
  Langs.}, pp. 163--173, 1994.

\bibitem[Ban97]{Banerjee:ICFP-1997}
\href{http://www.cis.ksu.edu/~ab/}{A.~Banerjee}.
\newblock
  \href{http://www.church-project.org/reports/Banerjee:ICFP-1997.html}{A
  modular, polyvariant, and type-based closure analysis}.
\newblock In IC{\relax FP} '97 \cite{ICFP1997}.

\bibitem[Bar89]{Barbanera:ICTCS-1989}
\href{http://www.dipmat.unict.it/~barba/}{F.~Barbanera}.
\newblock Combining term rewriting and type assignment systems.
\newblock In IC{\relax TCS} '89 \cite{ICTCS1989}, pp. 71--84.
\newblock The ICTCS '89 proceedings are to appear in \emph{Foundations of
  Computer Science}.

\bibitem[Bar92]{Barendregt:HLCS-1992}
\href{http://www.cs.kun.nl/~henk/}{H.~P. Barendregt}.
\newblock Lambda calculi with types.
\newblock In \href{http://www.informatics.ed.ac.uk/people/staff/Samson_Abramsky.html}{S.~Abramsky}, D.~M. Gabbay, T.~S.~E. Maibaum, eds., {\em Handbook
  of Logic in Computer Science}, vol.~2, chapter~2, pp. 117--309. Oxford
  University Press, 1992.

\bibitem[BCDC83]{Bar+Cop+Dez:JSL-1983-v48}
\href{http://www.cs.kun.nl/~henk/}{H.~Barendregt}, \href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini.
\newblock A filter lambda model and the completeness of type assignment.
\newblock {\em J.~Symbolic Logic}, 48(4):931--940, 1983.

\bibitem[BDC91]{Bar+Dez:TACS-1991}
\href{http://www.dipmat.unict.it/~barba/}{F.~Barbanera}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini.
\newblock Intersection and union types.
\newblock In TA{\relax CS} '91 \cite{TACS1991}, pp. 651--674.

\bibitem[BDCd95]{Bar+Dez+dLig:IAC-1995-v119}
\href{http://www.dipmat.unict.it/~barba/}{F.~Barbanera}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.unito.it/~deligu/}{U.~de'Liguoro}.
\newblock Intersection and union types: Syntax and semantics.
\newblock {\em Inform.\ {\&} Comput.}, 119:202--230, 1995.

\bibitem[BRDR89]{Bos+Ron:ICTCS-1989}
E.~Bosio, \href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock Type synthesis for intersection type discipline.
\newblock In IC{\relax TCS} '89 \cite{ICTCS1989}, pp. 109--122.
\newblock The ICTCS '89 proceedings are to appear in \emph{Foundations of
  Computer Science}.

\bibitem[CC90]{CC1990}
F.~Cardone, \href{http://www.di.unito.it/~coppo/}{M.~Coppo}.
\newblock Two extensions of {Curry's} type inference system.
\newblock In P.~Odifreddi, ed., {\em Logic and Computer Science}, number~31 in
  the APIC Series, chapter~1, pp. 19--75. Academic Press, 1990.

\bibitem[CDC78]{Cop+Dez:AML-1978-v19}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini.
\newblock A new type-assignment for lambda terms.
\newblock {\em Archiv f{\"{u}}r Mathematische Logik}, 19:139--156, 1978.

\bibitem[CDC80]{Cop+Dez-Cia:NDJFL-1980-v21n4}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini.
\newblock An extension of the basic functionality theory for the
  $\lambda$-calculus.
\newblock {\em Notre Dame J.~Formal Logic}, 21(4):685--693, 1980.

\bibitem[CDCS79]{Cop+Dez+Sal:ICALP-1979}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.enseeiht.fr/fr/recherche/Info/Logiciel/Logiciel.html}{P.~Sall\'{e}}.
\newblock Functional characterization of some semantic equalities inside
  ???-calculus.
\newblock In H.~A. Maurer, ed., {\em Automata, Languages and Programming, Sixth
  Colloquium}, vol.~71 of {\em LNCS}, pp. 133--146, Graz, July 1979.
  Springer-Verlag.

\bibitem[CDCV80]{Cop+Dez-Cia+Ven:HBC-1980}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www-dsi.ing.unifi.it/general/people.html}{B.~Venneri}.
\newblock Principal type schemes and $\lambda$-calculus semantics.
\newblock In \href{http://www-maths.swan.ac.uk/staff/jrh/}{Hindley} and \href{http://home.uleth.ca/~jonathan.seldin/}{Seldin} \cite{Sel+Hin:HBC-1980}, pp. 535--560.

\bibitem[CDCV81]{Cop+Dez-Cia+Ven:ZMLGM-1981}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www-dsi.ing.unifi.it/general/people.html}{B.~Venneri}.
\newblock Functional characters of solvable terms.
\newblock {\em Z. Math. Logik Grundlag. Math.}, 27(1):45--58, 1981.

\bibitem[CDCZ87]{Cop+Dez+Zac:IAC-1987-v72}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.unito.it/~zacchi/}{M.~Zacchi}.
\newblock Type-theories, normal forms, and {D}*-lambda models.
\newblock {\em Inform.\ {\&} Comput.}, 72:85--116, 1987.

\bibitem[CDG02]{Cop+Dam+Gia:TCS-2002}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~damiani/}{F.~Damiani}, \href{http://www.di.unito.it/~giannini/}{P.~Giannini}.
\newblock \href{http://www.di.unito.it/~damiani/papers/tcs1.ps}{Strictness,
  totality, and non-standard type inference}.
\newblock {\em Theoret.\ Comput.\ Sci.}, 272(1-2):69--111, feb 2002.

\bibitem[CG92]{Cop+Gia:CAAP-1992}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~giannini/}{P.~Giannini}.
\newblock A complete type inference algorithm for simple intersection types.
\newblock In {\em 17th Colloq.\ Trees in Algebra and Programming}, vol. 581 of
  {\em LNCS}, pp. 102--123. Springer-Verlag, 1992.

\bibitem[CG95]{Cop+Gia:IAC-1995-v122n1}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.di.unito.it/~giannini/}{P.~Giannini}.
\newblock Principal types and unification for simple intersection type systems.
\newblock {\em Inform.\ {\&} Comput.}, 122(1):70--96, 1995.

\bibitem[CH00]{Con+Hic:NCT-2000}
R.~L. Constable, J.~Hickey.
\newblock Nuprl's class theory and its applications.
\newblock Unpublished, 2000.

\bibitem[CHDCL83]{Cop+Dez+Hon+Lon:LC-1982}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}, \href{http://www.dimi.uniud.it/~honsell/}{F.~Honsell}, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.ens.fr/~longo/}{G.~Longo}.
\newblock Extended type structures and filter lambda models.
\newblock In G.~Lolli, \href{http://www.di.ens.fr/~longo/}{G.~Longo}, A.~Marcja, eds., {\em Logic Colloquium '82},
  pp. 241--262. North-Holland, Florence, Italy, 1983.

\bibitem[Cop80]{Coppo:MFCS-1980}
\href{http://www.di.unito.it/~coppo/}{M.~Coppo}.
\newblock An extended polymorphic type system for applicative languages.
\newblock In P.~Dembinski, ed., {\em Mathematical Foundations of Computer
  Science 1980, Proceedings of the 9th Symposium}, vol.~88 of {\em LNCS}, pp.
  194--204, Rydzyna, Poland, 1980. Springer-Verlag.

\bibitem[CP96]{Com+Pie:MSCS-1996-v6n5}
\href{http://guinness.cs.stevens-tech.edu/~abc/}{A.~B. Compagnoni}, \href{http://www.cis.upenn.edu/~bcpierce/}{B.~C. Pierce}.
\newblock Higher-order intersection types and multiple inheritance.
\newblock {\em Math.\ Structures Comput.\ Sci.}, 6(5):469--501, Oct. 1996.

\bibitem[Cra00]{Crary:SEOE-2000}
\href{http://www.cs.cmu.edu/~crary/}{K.~Crary}.
\newblock Simple, efficient object encoding using intersection types, 2000.
\newblock CMU Internal Report.

\bibitem[DCGV97]{Dez+Ghi+Ven:NDJFL-1997-v38n2}
\href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.cs.kun.nl/~silviagh/}{S.~Ghilezan}, \href{http://www-dsi.ing.unifi.it/general/people.html}{B.~Venneri}.
\newblock The ``relevance'' of intersection and union types.
\newblock {\em Notre Dame J.~Formal Logic}, 38(2):246--269, Spring 1997.

\bibitem[DCH92]{Dez+Hin:TCS-1992-v100}
\href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www-maths.swan.ac.uk/staff/jrh/}{J.~R. Hindley}.
\newblock Intersection types for combinatory logic.
\newblock {\em Theoret.\ Comput.\ Sci.}, 100(2):303--324, 29~June 1992.
\newblock A preliminary version is pp. 181--192 in~\cite{Klo+:JWB-1989}.

\bibitem[DCM84]{Dez+Mar:SDT-1984}
\href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.unito.it/~ines/}{I.~Margaria}.
\newblock F-semantics for intersection type discipline.
\newblock In G.~Kahn, \href{http://www.cs.bell-labs.com/~dbm/}{D.~B. MacQueen}, \href{http://www.dcs.ed.ac.uk/home/gdp/}{G.~Plotkin}, eds., {\em Proc.\ Semantics
  of Data Types, International Symposium}, vol. 173 of {\em LNCS}, pp.
  279--300, Sophia-Antipolis, France, June 1984. Springer-Verlag.

\bibitem[DCM86]{Dez+Mar:TCS-1986-v45}
\href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.unito.it/~ines/}{I.~Margaria}.
\newblock A characterization of {F}-complete type assignments.
\newblock {\em Theoret.\ Comput.\ Sci.}, 45:121--157, 1986.

\bibitem[DG00]{Dam+Gia:JFP-2000}
\href{http://www.di.unito.it/~damiani/}{F.~Damiani}, \href{http://www.di.unito.it/~giannini/}{P.~Giannini}.
\newblock Automatic useless-code detection and elimination for {HOT} functional
  programs.
\newblock {\em J.~Funct.\ Programming}, pp. 509--559, 2000.

\bibitem[DL01]{Dou+Les:TLCA-2001}
\href{http://www.cs.wpi.edu/~dd/}{D.~Dougherty}, P.~Lescanne.
\newblock Reductions, intersection types, and explicit substitution.
\newblock In {\em 5th Int'l Conf.\ Typed Lambda Calculi and Applications}, vol.
  2044 of {\em LNCS}, pp. 121--135, Krak{{\'o}}w, Poland, 2--5~May 2001.
  Springer-Verlag.

\bibitem[DMTW97]{Dim+Mul+Tur+Wel:ICFP-1997}
\href{http://www.cs.uml.edu/~dimock/}{A.~Dimock}, \href{http://oak.bc.edu/~muller/}{R.~Muller}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Dim+Mul+Tur+Wel:ICFP-1997.html}{Strongly typed flow-directed representation transformations}.
\newblock In IC{\relax FP} '97 \cite{ICFP1997}, pp. 11--24.

\bibitem[EHRDR92]{Egi+Hon+Ron:FI-1992-v16n2}
L.~Egidi, \href{http://www.dimi.uniud.it/~honsell/}{F.~Honsell}, \href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock Operational, denotational, and logical descriptions: A case-study.
\newblock {\em Fund.\ Inform.}, 16(2):149--169, 1992.
\newblock Mathematical foundations of computer science '91 (Kazimierz Dolny,
  1991).

\bibitem[Gar94]{Gardner:TACS-1994}
\href{http://www.cl.cam.ac.uk/users/pag20/}{P.~Gardner}.
\newblock Discovering needed reductions using type theory.
\newblock In {\em Theoretical Aspects Comput.\ Softw.\ : Int'l Conf.}, vol. 789
  of {\em LNCS}. Springer-Verlag, 1994.

\bibitem[Ghi93]{Ghilezan:JLC-1993-v3n6}
\href{http://www.cs.kun.nl/~silviagh/}{S.~Ghilezan}.
\newblock Inhabitation in intersection and union type assignment systems.
\newblock {\em J.~Logic Comput.}, 3(6):671--685, Dec. 1993.

\bibitem[Ghi96]{Ghilezan:NDJFL-1996-v37n1}
\href{http://www.cs.kun.nl/~silviagh/}{S.~Ghilezan}.
\newblock Strong normalization and typability with intersection types.
\newblock {\em Notre Dame J.~Formal Logic}, 37(1):44--52, Winter 1996.

\bibitem[Hay91]{Hayashi:TACS-1991}
\href{http://pascal.seg.kobe-u.ac.jp/~hayashi/}{S.~Hayashi}.
\newblock Singleton, union and intersection types for program extraction.
\newblock In TA{\relax CS} '91 \cite{TACS1991}, pp. 701--730.

\bibitem[Hay94]{Hayashi:IAC-1994-v109n1/2}
\href{http://pascal.seg.kobe-u.ac.jp/~hayashi/}{S.~Hayashi}.
\newblock Singleton, union and intersection types for program extraction.
\newblock {\em Inform.\ {\&} Comput.}, 109(1/2):174--210, February/March 1994.

\bibitem[Hin82]{Hindley:ISOP-1982}
\href{http://www-maths.swan.ac.uk/staff/jrh/}{J.~R. Hindley}.
\newblock The simple semantics for {C}oppo-{D}ezani-{S}all{\'e} types.
\newblock In \href{http://www.di.unito.it/~dezani/}{M.~Dezani}-Ciancaglini, \href{http://www.di.unipi.it/~ugo/ugo.html}{U.~Montanari}, eds., {\em International
  Symposium on Programming, 5th Colloquium}, vol. 137 of {\em LNCS}, pp.
  212--226, Turin, Apr. 1982. Springer-Verlag.

\bibitem[Hin84]{Hindley:TCS-1984-v28n1/2}
\href{http://www-maths.swan.ac.uk/staff/jrh/}{J.~R. Hindley}.
\newblock {C}oppo-{D}ezani types do not correspond to propositional logic.
\newblock {\em Theoret.\ Comput.\ Sci.}, 28(1--2):235--236, Jan. 1984.

\bibitem[HL99]{Hon+Len:TCS-1999-v212n1/2}
\href{http://www.dimi.uniud.it/~honsell/}{F.~Honsell}, M.~Lenisa.
\newblock Semantical analysis of perpetual strategies in $\lambda$-calculus.
\newblock {\em Theoret.\ Comput.\ Sci.}, 212(1--2):183--209, 6~Feb. 1999.

\bibitem[HRDR91]{Hon+Ron:PCM-1990}
\href{http://www.dimi.uniud.it/~honsell/}{F.~Honsell}, \href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock Reasoning about interpretation in qualitative lambda models.
\newblock In {\em IFIP TC2 Working Conference on Programming Concepts and
  Methods 1990}, pp. 492--508. North-Holland, 1991.

\bibitem[HRDR92]{Hon+Ron:JCSS-1992-v45n1}
\href{http://www.dimi.uniud.it/~honsell/}{F.~Honsell}, \href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock An approximation theorem for topological lambda models and the
  topological incompleteness of lambda calculus.
\newblock {\em J. Comput. System Sci.}, 45(1):49--75, 1992.

\bibitem[HS80]{Sel+Hin:HBC-1980}
\href{http://www-maths.swan.ac.uk/staff/jrh/}{J.~R. Hindley}, \href{http://home.uleth.ca/~jonathan.seldin/}{J.~P. Seldin}, eds.
\newblock {\em To {H}.~{B}.\ {C}urry: Essays on Combinatory Logic, Lambda
  Calculus, and Formalism}.
\newblock Academic Press, 1980.

\bibitem[IC{\relax FP}97]{ICFP1997}
{\em Proc.\ 1997 Int'l Conf.\ Functional Programming}. ACM Press, 1997.

\bibitem[IC{\relax TCS}89]{ICTCS1989}
{\em Proc. Third Italian Conference on Theoretical Computer Science}, Mantova,
  1989. World Scientific Press.
\newblock The ICTCS '89 proceedings are to appear in \emph{Foundations of
  Computer Science}.

\bibitem[Jen98]{Jensen:POPL-1998}
\href{http://www.irisa.fr/lande/jensen/}{T.~Jensen}.
\newblock Inference of polymorphic and conditional strictness properties.
\newblock In PO{\relax PL} '98 \cite{POPL1998}.

\bibitem[Jim95a]{Jim:RTTS-1995}
\href{http://www.research.att.com/~trevor/}{T.~Jim}.
\newblock
  \href{http://www.church-project.org/reports/electronic/Jim:RTTS-1995.pdf}{Rank 2 type systems and recursive definitions}.
\newblock Technical Report MIT/LCS/TM-531, Massachusetts Institute of
  Technology, Nov. 1995.

\bibitem[Jim95b]{Jim:MIT-LCS-1995-532}
\href{http://www.research.att.com/~trevor/}{T.~Jim}.
\newblock
  \href{http://www.church-project.org/reports/electronic/Jim:MIT-LCS-1995-532.pdf}{What are principal typings and what are they good for?}
\newblock Tech.\ memo. MIT/LCS/TM-532, MIT, 1995.

\bibitem[Jim96]{Jim:POPL-1996}
\href{http://www.research.att.com/~trevor/}{T.~Jim}.
\newblock What are principal typings and what are they good for?
\newblock In {\em Conf.\ Rec.\ POPL '96: 23rd {ACM} Symp.\ Princ.\ of\ Prog.\
  Langs.}, 1996.

\bibitem[JMZ92]{Jac+Mar+Zac:TCS-1992-v95}
\href{http://www.cs.kun.nl/~bart/}{B.~Jacobs}, \href{http://www.di.unito.it/~ines/}{I.~Margaria}, \href{http://www.di.unito.it/~zacchi/}{M.~Zacchi}.
\newblock Filter models with polymorphic types.
\newblock {\em Theoret.\ Comput.\ Sci.}, 95:143--158, 1992.

\bibitem[K{\etalchar{+}}89]{Klo+:JWB-1989}
\href{http://www.cs.vu.nl/fb/generated/personal/Klop.html}{J.~W. Klop}, et~al., eds.
\newblock {\em J.W. de Bakker, 25 Jaar Semantiek}.
\newblock Centrum voor Wiskunde en Informatica, Amsterdam, 1989.

\bibitem[Kfo96]{Kfoury:TTTR-1996a}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}.
\newblock
  \href{http://www.church-project.org/reports/electronic/Kfoury:TTTR-1996a.pdf}{Beta-reduction as unification}.
\newblock A refereed extensively edited version
  is~\cite{Kfoury:Rasiowa-memorial}. This preliminary version was presented at
  the Helena Rasiowa Memorial Conference, July 1996.

\bibitem[Kfo99]{Kfoury:Rasiowa-memorial}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}.
\newblock
  \href{http://www.church-project.org/reports/Kfoury:Rasiowa-memorial.html}{Beta-reduction as unification}.
\newblock In D.~Niwinski, ed., {\em Logic, Algebra, and Computer Science (H.
  Rasiowa Memorial Conference, December 1996), Banach Center Publication,
  Volume 46}, pp. 137--158. Springer-Verlag, 1999.
\newblock Supersedes~\cite{Kfoury:TTTR-1996a} but omits a few proofs included
  in the latter.

\bibitem[Kfo00]{Kfoury:JLC-2000-v10n3}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}.
\newblock
  \href{http://www.church-project.org/reports/Kfoury:JLC-2000-v10n3.html}{A
  linearization of the lambda-calculus}.
\newblock {\em J.~Logic Comput.}, 10(3), 2000.
\newblock Special issue on Type Theory and Term Rewriting. \href{http://www.macs.hw.ac.uk/~fairouz/}{Kamareddine} and \href{http://www.cs.vu.nl/fb/generated/personal/Klop.html}{Klop}
  (editors).

\bibitem[KMTW99]{Kfo+Mai+Tur+Wel:ICFP-1999}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}, \href{http://www.cs.brandeis.edu/~mairson/}{H.~G. Mairson}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~A. Turbak}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Kfo+Mai+Tur+Wel:ICFP-1999.html}{Relating typability and expressibility in finite-rank intersection type
  systems}.
\newblock In {\em Proc.\ 1999 Int'l Conf.\ Functional Programming}, pp.
  90--101. ACM Press, 1999.

\bibitem[Kop00]{Kopylov:Cornell-CS-TR2000-1809}
\href{http://www.cs.cornell.edu/People/kopylov/}{A.~Kopylov}.
\newblock Dependent intersection: A new way of defining records in type theory.
\newblock Technical Report TR2000-1809, Dept.\ of Computer Science, Cornell
  University, 2000.

\bibitem[KW95a]{Kfo+Wel:ANN-1995}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.cs.bu.edu/techreports/1995-007-strong-normalization-addendum.ps.gz}{Addendum to ``{New} notions of reduction and non-semantic proofs of
  $\beta$-strong normalization in typed $\lambda$-calculi''}.
\newblock Tech.\ Rep. 95-007, Comp.\ Sci.\ Dept., Boston Univ., 1995.

\bibitem[KW95b]{Kfo+Wel:LICS-1995}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Kfo+Wel:LICS-1995.html}{New
  notions of reduction and non-semantic proofs of $\beta$-strong normalization
  in typed $\lambda$-calculi}.
\newblock In {\em Proc.\ 10th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.}, pp.
  311--321, 1995.

\bibitem[KW99]{Kfo+Wel:POPL-1999}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Kfo+Wel:POPL-1999.html}{Principality and decidable type inference for finite-rank intersection types}.
\newblock In {\em Conf.\ Rec.\ POPL '99: 26th {ACM} Symp.\ Princ.\ of\ Prog.\
  Langs.}, pp. 161--174, 1999.
\newblock Superseded by~\cite{Kfo+Wel:TCSB-ta}.

\bibitem[KW0X]{Kfo+Wel:TCSB-ta}
\href{http://www.cs.bu.edu/~kfoury/}{A.~J. Kfoury}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Kfo+Wel:TCSB-ta.html}{Principality and type inference for intersection types using expansion variables}.
\newblock {\em Theoret.\ Comput.\ Sci.}, 200X.
\newblock Supersedes~\cite{Kfo+Wel:POPL-1999}. Accepted subject to revisions.

\bibitem[LDL02]{Len+Dou+Les:TCS-2002}
\href{http://www.ens-lyon.fr/~slengran/}{S.~Lengrand}, \href{http://www.cs.wpi.edu/~dd/}{D.~Dougherty}, P.~Lescanne.
\newblock An improved system of intersection types for explicit substitutions.
\newblock In R.~Baeza-Yates, \href{http://www.di.unipi.it/~ugo/ugo.html}{U.~Montanari}, N.~Santoro, eds., {\em 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.

\bibitem[LE85a]{Lopez-Escobar:RCM-1985-v19}
E.~K.~G. Lopez-Escobar.
\newblock On intuitionistic sentential connectives.
\newblock {\em Rev. Colombiana de Math.}, 19:117--130, 1985.

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

\bibitem[Lei83]{Leivant:POPL-1983}
\href{http://www.cs.indiana.edu/~leivant/}{D.~Leivant}.
\newblock Polymorphic type inference.
\newblock In {\em Conf.\ Rec.\ 10th Ann.\ {ACM} Symp.\ Princ.\ of\ \ Prog.\
  Langs.}, pp. 88--98, 1983.

\bibitem[Min89]{Mints:NDJFL-1989-v30}
G.~E. Mints.
\newblock The completeness of provable realizability.
\newblock {\em Notre Dame J.~Formal Logic}, 30(3):420--441, 1989.

\bibitem[MZ]{Mar+Zac:PTP}
\href{http://www.di.unito.it/~ines/}{I.~Margaria}, \href{http://www.di.unito.it/~zacchi/}{M.~Zacchi}.
\newblock Principal typing in a polymorphic-intersection type discipline.
\newblock Submitted circa 1991, probably published by now.

\bibitem[Pie91a]{Pierce:PITBP-1991}
\href{http://www.cis.upenn.edu/~bcpierce/}{B.~C. Pierce}.
\newblock {\em Programming with Intersection Types and Bounded Polymorphism}.
\newblock PhD thesis, Carnegie Mellon University, 1991.
\newblock Also tech report CMU-CS-91-205.

\bibitem[Pie91b]{Pierce:PIT-1991}
\href{http://www.cis.upenn.edu/~bcpierce/}{B.~C. Pierce}.
\newblock Programming with intersection types, union types, and polymorphism.
\newblock Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb.
  1991.

\bibitem[Pie97]{Pierce:MSCS-1997-v7n2}
\href{http://www.cis.upenn.edu/~bcpierce/}{B.~C. Pierce}.
\newblock Intersection types and bounded polymorphism.
\newblock {\em Math.\ Structures Comput.\ Sci.}, 7(2):129--193, Apr. 1997.

\bibitem[Plo91]{Plotkin:TACS-1991}
\href{http://www.dcs.ed.ac.uk/home/gdp/}{G.~Plotkin}.
\newblock A semantics for type checking.
\newblock In TA{\relax CS} '91 \cite{TACS1991}, pp. 1--17.

\bibitem[PO{\relax PL}98]{POPL1998}
{\em Conf.\ Rec.\ POPL '98: 25th {ACM} Symp.\ Princ.\ of\ Prog.\ Langs.}, 1998.

\bibitem[Pot80]{Pottinger:HBC-1980}
\href{http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/p/Pottinger:Garrel.html}{G.~Pottinger}.
\newblock A type assignment for the strongly normalizable $\lambda$-terms.
\newblock In \href{http://www-maths.swan.ac.uk/staff/jrh/}{Hindley} and \href{http://home.uleth.ca/~jonathan.seldin/}{Seldin} \cite{Sel+Hin:HBC-1980}, pp. 561--577.

\bibitem[PP98]{Pal+Pav:POPL-1998}
\href{http://www.cs.purdue.edu/people/palsberg}{J.~Palsberg}, C.~Pavlopoulou.
\newblock From polyvariant flow information to intersection and union types.
\newblock In PO{\relax PL} '98 \cite{POPL1998}, pp. 197--208.
\newblock Superseded by \cite{Pal+Pav:JFP-2001}.

\bibitem[PP01]{Pal+Pav:JFP-2001}
\href{http://www.cs.purdue.edu/people/palsberg}{J.~Palsberg}, C.~Pavlopoulou.
\newblock From polyvariant flow information to intersection and union types.
\newblock {\em J.~Funct.\ Programming}, 11(3):263--317, May 2001.

\bibitem[RDR82]{Ronchi:IAC-1982-v54}
\href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock Characterization theorems for a filter lambda model.
\newblock {\em Information and Control}, 54:201--216, 1982.

\bibitem[RDR88]{Ronchi:TCS-1988-v59}
\href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}.
\newblock Principal type schemes and unification for intersection type
  discipline.
\newblock {\em Theoret.\ Comput.\ Sci.}, 59(1--2):181--209, Mar. 1988.

\bibitem[RDRV84]{Ron+Ven:TCS-1984-v28}
\href{http://www.di.unito.it/~ronchi/}{S.~Ronchi Della~Rocca}, \href{http://www-dsi.ing.unifi.it/general/people.html}{B.~Venneri}.
\newblock Principal type schemes for an extended type theory.
\newblock {\em Theoret.\ Comput.\ Sci.}, 28(1--2):151--169, Jan. 1984.

\bibitem[Rey87]{Reynolds:LICS-1987}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock Conjunctive types and {A}lgol-like languages (abstract of invited
  lecture).
\newblock In {\em Proc.\ 2nd Ann.\ Symp.\ Logic in Comput. Sci.}, p. 119, 1987.

\bibitem[Rey88]{Reynolds88}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock Preliminary design of the programming language {F}orsythe.
\newblock Technical Report CMU-CS-88-159, Carnegie Mellon University, 1988.
\newblock Superseded by \cite{Reynolds:DPLF-1996}.

\bibitem[Rey89]{Reynolds:ICALP-1989}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock Syntactic control of interference, part 2.
\newblock In G.~Ausiello, \href{http://www.di.unito.it/~dezani/}{M.~Dezani}, S.~R.~D. Rocca, eds., {\em Automata,
  Languages and Programming, 16th International Colloquium, Proceedings}, vol.
  372 of {\em LNCS}, pp. 704--722. Springer-Verlag, July 1989.

\bibitem[Rey91]{Reynolds:TACS-1991}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock The coherence of languages with intersection types.
\newblock In TA{\relax CS} '91 \cite{TACS1991}, pp. 675--700.

\bibitem[Rey96]{Reynolds:DPLF-1996}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock Design of the programming language {F}orsythe.
\newblock Technical Report CMU-CS-96-146, Carnegie Mellon Univ., Pittsburgh, PA
  15213, USA, June~28 1996.

\bibitem[Rey00]{Reynolds:BRICS-RS-00-32}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock \href{http://www.brics.dk/RS/00/32/}{The meaning of types --- from
  intrinsic to extrinsic semantics}.
\newblock Research Series RS--00--32, BRICS, DAIMI, Department of Computer
  Science, University of Aarhus, Dec. 2000.

\bibitem[Rey01]{Reynolds:WDTM-2001}
\href{http://www.cs.cmu.edu/~jcr/}{J.~C. Reynolds}.
\newblock \href{ftp://ftp.cs.cmu.edu/user/jcr/shorttypemeaning.ps.gz}{What do
  types mean? --- from intrinsic to extrinsic semantics}.
\newblock To appear in Essays on Programming Methodology, edited by Annabelle
  McIver and Carroll Morgan, to be published by Springer-Verlag, New York,
  2001.

\bibitem[Sal78]{Salle:ICALP-1978}
\href{http://www.enseeiht.fr/fr/recherche/Info/Logiciel/Logiciel.html}{P.~Sall\'{e}}.
\newblock Une extension de la th\'{e}orie des types en $\lambda$-calcul.
\newblock In G.~Ausiello, C.~B{\"o}hm, eds., {\em Fifth International
  Conference on Automata, Languages and Programming}, vol.~62 of {\em LNCS},
  pp. 398--410. Springer-Verlag, July 1978.

\bibitem[SM96]{Say+Mau:NPI-1996}
{\'E}.~Sayag, \href{http://pauillac.inria.fr/~mauny/}{M.~Mauny}.
\newblock A new presentation of the intersection type discipline through
  principal typings of normal forms.
\newblock Technical Report RR-2998, INRIA, Oct.~16, 1996.

\bibitem[SM97]{Say+Mau:SPIT-1997}
{\'E}.~Sayag, \href{http://pauillac.inria.fr/~mauny/}{M.~Mauny}.
\newblock Structural properties of intersection types.
\newblock In {\em Proceedings of the 8th International Conference on Logic and
  Computer Science -- Theoretical Foundations of Computing (LIRA)}, pp.
  167--175, Novi Sad, Yugoslavia, Sept. 1997.

\bibitem[TA{\relax CS}91]{TACS1991}
{\em Theoretical Aspects Comput.\ Softw.~: Int'l Conf.}, vol. 526 of {\em
  LNCS}. Springer-Verlag, 1991.

\bibitem[TDMW97]{Tur+Dim+Mul+Wel:CPPFT-1997}
\href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}, \href{http://www.cs.uml.edu/~dimock/}{A.~Dimock}, \href{http://oak.bc.edu/~muller/}{R.~Muller}, \href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}.
\newblock
  \href{http://www.church-project.org/reports/Tur+Dim+Mul+Wel:CPPFT-1997.html}{Compiling with polymorphic and polyvariant flow types}.
\newblock In {\em Proc.\ First Int'l Workshop on Types in Compilation}, June
  1997.

\bibitem[TS96]{Tri+Smi:SAS-1996}
\href{http://rum.cs.yale.edu/trifonov/}{V.~Trifonov}, \href{http://www.cs.jhu.edu/~scott/}{S.~Smith}.
\newblock Subtyping constrained types.
\newblock In {\em Proc.\ 3rd Int'l Static Analysis Symp.}, pp. 349--365, 1996.

\bibitem[Urz94]{Urzyczyn:LICS-1994}
\href{http://www.mimuw.edu.pl/~urzy/}{P.~Urzyczyn}.
\newblock The emptiness problem for intersection types.
\newblock In {\em Proc.\ 9th Ann.\ {IEEE} Symp.\ Logic in Comput. Sci.}, pp.
  300--309, 1994.

\bibitem[vB92]{vanBakel:TCS-1992-v102}
\href{http://theory.doc.ic.ac.uk/~svb/}{S.~J. van Bakel}.
\newblock Complete restrictions of the intersection type discipline.
\newblock {\em Theoret.\ Comput.\ Sci.}, 102(1):135--163, 1992.

\bibitem[vB93a]{vanBakel:ITD-1993}
\href{http://theory.doc.ic.ac.uk/~svb/}{S.~J. van Bakel}.
\newblock {\em Intersection Type Disciplines in Lambda Calculus and Applicative
  Term Rewriting Systems}.
\newblock PhD thesis, Catholic University of Nijmegen, 1993.

\bibitem[vB93b]{vanBakel:JLC-1993-v3n6}
\href{http://theory.doc.ic.ac.uk/~svb/}{S.~J. van Bakel}.
\newblock Principal type schemes for the strict type assignment system.
\newblock {\em J.~Logic Comput.}, 3(6):643--670, Dec. 1993.

\bibitem[vB95]{Bakel:TCS-1995-v151n5}
\href{http://theory.doc.ic.ac.uk/~svb/}{S.~J. van Bakel}.
\newblock Intersection type assignment systems.
\newblock {\em Theoret.\ Comput.\ Sci.}, 151(2):385--435, 27~Nov. 1995.

\bibitem[vB96]{vanBakel:FI-1996}
\href{http://theory.doc.ic.ac.uk/~svb/}{S.~J. van Bakel}.
\newblock Rank~2 intersection type assignment in term rewriting systems.
\newblock {\em Fundamenta Informatica}, 2(26), 1996.

\bibitem[Ven94]{Venneri:JLC-1994-v4n2}
\href{http://www-dsi.ing.unifi.it/general/people.html}{B.~Venneri}.
\newblock Intersection types as logical formulae.
\newblock {\em J.~Logic Comput.}, 4(2):109--124, Apr. 1994.

\bibitem[WDMT97]{Wel+Dim+Mul+Tur:TAPSOFT-1997}
\href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}, \href{http://www.cs.uml.edu/~dimock/}{A.~Dimock}, \href{http://oak.bc.edu/~muller/}{R.~Muller}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}.
\newblock
  \href{http://www.church-project.org/reports/Wel+Dim+Mul+Tur:TAPSOFT-1997.html}{A typed intermediate language for flow-directed compilation}.
\newblock In {\em Proc.\ 7th Int'l Joint Conf.\ Theory \& Practice of Software
  Development}, pp. 757--771, 1997.
\newblock Superseded by \cite{Wel+Dim+Mul+Tur:JFP-2002-v12n3}.

\bibitem[WDMT02]{Wel+Dim+Mul+Tur:JFP-2002-v12n3}
\href{http://www.macs.hw.ac.uk/~jbw/}{J.~B. Wells}, \href{http://www.cs.uml.edu/~dimock/}{A.~Dimock}, \href{http://oak.bc.edu/~muller/}{R.~Muller}, \href{http://cs.wellesley.edu/~fturbak/lyn.html}{F.~Turbak}.
\newblock
  \href{http://www.church-project.org/reports/Wel+Dim+Mul+Tur:JFP-2002-v12n3.html}{A calculus with polymorphic and polyvariant flow types}.
\newblock {\em J.~Funct.\ Programming}, 12(3):183--227, May 2002.
\newblock Supersedes \cite{Wel+Dim+Mul+Tur:TAPSOFT-1997}.

\bibitem[Yok91]{Yokouchi:ESO-1991}
H.~Yokouchi.
\newblock Embedding second order type system into intersection type system and
  its application to type inference.
\newblock Internal report, I.B.M. Research Lab., Tokyo, Japan, 1991.
\newblock Probably published somewhere by now.

\end{thebibliography}
