cs0011039/acm1.bbl
1: \begin{thebibliography}{}
2: 
3: \bibitem[\protect\citeauthoryear{Abramsky}{Abramsky}{1991}]{abra91}
4: {\sc Abramsky, S.} 1991.
5: \newblock Domain theory in logical form.
6: \newblock {\em Ann. Pure Appl. Logic\/}~{\em 51,\/}~1-2, 1--77.
7: 
8: \bibitem[\protect\citeauthoryear{Abramsky and Ong}{Abramsky and
9:   Ong}{1993}]{abraong93}
10: {\sc Abramsky, S.} {\sc and} {\sc Ong, C.-H.~L.} 1993.
11: \newblock Full abstraction in the lazy lambda calculus.
12: \newblock {\em Inform. and Comput.\/}~{\em 105,\/}~2, 159--267.
13: 
14: \bibitem[\protect\citeauthoryear{Barendregt, Coppo, and
15:   Dezani-Ciancaglini}{Barendregt et~al\mbox{.}}{1983}]{barecoppdeza83}
16: {\sc Barendregt, H.}, {\sc Coppo, M.}, {\sc and} {\sc Dezani-Ciancaglini, M.}
17:   1983.
18: \newblock A filter lambda model and the completeness of type assignment.
19: \newblock {\em J. Symbolic Logic\/}~{\em 48,\/}~4, 931--940.
20: 
21: \bibitem[\protect\citeauthoryear{Barendregt and et. al.}{Barendregt and et.
22:   al.}{2000}]{bare00}
23: {\sc Barendregt, H.} {\sc and} {\sc et. al.} 2000.
24: \newblock {\em Typed $\lambda$-calculus and applications}.
25: \newblock North-Holland, Amsterdam.
26: \newblock (to appear).
27: 
28: \bibitem[\protect\citeauthoryear{Coppo and Dezani-Ciancaglini}{Coppo and
29:   Dezani-Ciancaglini}{1980}]{coppdeza80}
30: {\sc Coppo, M.} {\sc and} {\sc Dezani-Ciancaglini, M.} 1980.
31: \newblock An extension of the basic functionality theory for the $\lambda
32:   $-calculus.
33: \newblock {\em Notre Dame J. Formal Logic\/}~{\em 21,\/}~4, 685--693.
34: 
35: \bibitem[\protect\citeauthoryear{Coppo, Dezani-Ciancaglini, and Venneri}{Coppo
36:   et~al\mbox{.}}{1981}]{coppdezavenn81}
37: {\sc Coppo, M.}, {\sc Dezani-Ciancaglini, M.}, {\sc and} {\sc Venneri, B.}
38:   1981.
39: \newblock Functional characters of solvable terms.
40: \newblock {\em Z. Math. Logik Grundlag. Math.\/}~{\em 27,\/}~1, 45--58.
41: 
42: \bibitem[\protect\citeauthoryear{Coppo, Dezani-Ciancaglini, and Zacchi}{Coppo
43:   et~al\mbox{.}}{1987}]{coppdezazacc87}
44: {\sc Coppo, M.}, {\sc Dezani-Ciancaglini, M.}, {\sc and} {\sc Zacchi, M.} 1987.
45: \newblock Type theories, normal forms, and ${D}\sb \infty$-lambda-models.
46: \newblock {\em Inform. and Comput.\/}~{\em 72,\/}~2, 85--116.
47: 
48: \bibitem[\protect\citeauthoryear{Coppo, Honsell, Dezani-Ciancaglini, and
49:   Longo}{Coppo et~al\mbox{.}}{1984}]{coppdezahonslong84}
50: {\sc Coppo, M.}, {\sc Honsell, F.}, {\sc Dezani-Ciancaglini, M.}, {\sc and}
51:   {\sc Longo, G.} 1984.
52: \newblock Extended type structures and filter lambda models.
53: \newblock In {\em Logic colloquium '82}. North-Holland, Amsterdam, 241--262.
54: 
55: \bibitem[\protect\citeauthoryear{Dezani-Ciancaglini, Honsell, and
56:   Alessi}{Dezani-Ciancaglini et~al\mbox{.}}{2000}]{alesdezahons00}
57: {\sc Dezani-Ciancaglini, M.}, {\sc Honsell, F.}, {\sc and} {\sc Alessi, F.}
58:   2000.
59: \newblock A complete characterization of the complete intersection-type
60:   theories.
61: \newblock In {\em Proceedings in Informatics}, {J.~et~al.}, Ed. Vol.~8. ITRS'00
62:   Workshop, Carleton-Scientific, Canada, 287--301.
63: 
64: \bibitem[\protect\citeauthoryear{Dezani-Ciancaglini and
65:   Margaria}{Dezani-Ciancaglini and Margaria}{1986}]{dezamarg86}
66: {\sc Dezani-Ciancaglini, M.} {\sc and} {\sc Margaria, I.} 1986.
67: \newblock A characterization of ${F}$-complete type assignments.
68: \newblock {\em Theoret. Comput. Sci.\/}~{\em 45,\/}~2, 121--157.
69: 
70: \bibitem[\protect\citeauthoryear{Egidi, Honsell, and Ronchi~della Rocca}{Egidi
71:   et~al\mbox{.}}{1992}]{egidhonsronc92}
72: {\sc Egidi, L.}, {\sc Honsell, F.}, {\sc and} {\sc Ronchi~della Rocca, S.}
73:   1992.
74: \newblock Operational, denotational and logical descriptions: a case study.
75: \newblock {\em Fund. Inform.\/}~{\em 16,\/}~2, 149--169.
76: 
77: \bibitem[\protect\citeauthoryear{Hindley}{Hindley}{1983a}]{hind83}
78: {\sc Hindley, J.} 1983a.
79: \newblock The completeness theorem for typing $\lambda$-terms.
80: \newblock {\em Theoret. Comput. Sci.\/}~{\em 22}, 1--17.
81: 
82: \bibitem[\protect\citeauthoryear{Hindley}{Hindley}{1983b}]{hind83a}
83: {\sc Hindley, J.} 1983b.
84: \newblock The completeness theorem for typing $\lambda$-terms.
85: \newblock {\em Theoret. Comput. Sci.\/}~{\em 22}, 127--133.
86: 
87: \bibitem[\protect\citeauthoryear{Hindley}{Hindley}{1982}]{hind82}
88: {\sc Hindley, J.~R.} 1982.
89: \newblock The simple semantics for {C}oppo--{D}ezani--{S}all\'e types.
90: \newblock In {\em International symposium on programming (Turin, 1982)}.
91:   Springer, Berlin, 212--226.
92: 
93: \bibitem[\protect\citeauthoryear{Hindley and Longo}{Hindley and
94:   Longo}{1980}]{hindlong80}
95: {\sc Hindley, R.} {\sc and} {\sc Longo, G.} 1980.
96: \newblock Lambda-calculus models and extensionality.
97: \newblock {\em Z. Math. Logik Grundlag. Math.\/}~{\em 26,\/}~4, 289--310.
98: 
99: \bibitem[\protect\citeauthoryear{Honsell and Lenisa}{Honsell and
100:   Lenisa}{1999}]{honsleni99}
101: {\sc Honsell, F.} {\sc and} {\sc Lenisa, M.} 1999.
102: \newblock Semantical analysis of perpetual strategies in $\lambda$-calculus.
103: \newblock {\em Theoret. Comput. Sci.\/}~{\em 212,\/}~1-2, 183--209.
104: 
105: \bibitem[\protect\citeauthoryear{Honsell and Ronchi~della Rocca}{Honsell and
106:   Ronchi~della Rocca}{1992}]{honsronc92}
107: {\sc Honsell, F.} {\sc and} {\sc Ronchi~della Rocca, S.} 1992.
108: \newblock An approximation theorem for topological lambda models and the
109:   topological incompleteness of lambda calculus.
110: \newblock {\em J. Comput. System Sci.\/}~{\em 45,\/}~1, 49--75.
111: 
112: \bibitem[\protect\citeauthoryear{Mitchell}{Mitchell}{1988}]{mitc88}
113: {\sc Mitchell, J.} 1988.
114: \newblock Polymorphic type inference and containment.
115: \newblock {\em Information and Computation\/}~{\em 76}, 211--249.
116: 
117: \bibitem[\protect\citeauthoryear{Park}{Park}{1976}]{park76}
118: {\sc Park, D.} 1976.
119: \newblock The ${\Y}$-combinator in {S}cott's $\l$-calculus models (revised
120:   version).
121: \newblock Theory of Computation Report 13, Department of Computer Science,
122:   University of Warick.
123: 
124: \bibitem[\protect\citeauthoryear{Plotkin}{Plotkin}{1975}]{plot75}
125: {\sc Plotkin, G.~D.} 1975.
126: \newblock Call-by-name, call-by-value and the $\lambda $-calculus.
127: \newblock {\em Theoret. Comput. Sci.\/}~{\em 1,\/}~2, 125--159.
128: 
129: \bibitem[\protect\citeauthoryear{Plotkin}{Plotkin}{1993}]{plot93}
130: {\sc Plotkin, G.~D.} 1993.
131: \newblock Set-theoretical and other elementary models of the
132:   $\lambda$-calculus.
133: \newblock {\em Theoret. Comput. Sci.\/}~{\em 121,\/}~1-2, 351--409.
134: 
135: \bibitem[\protect\citeauthoryear{Scott}{Scott}{1972}]{scot72}
136: {\sc Scott, D.} 1972.
137: \newblock Continuous lattices.
138: \newblock In {\em Toposes, Algebraic Geometry and Logic}, {F.~Lawvere}, Ed.
139:   Lecture Notes in Mathematics, vol. 274. Springer, Berlin, 97--136.
140: 
141: \bibitem[\protect\citeauthoryear{Scott}{Scott}{1975}]{scot75}
142: {\sc Scott, D.} 1975.
143: \newblock Open problem.
144: \newblock In {\em Lambda Calculus and Computer Science Theory}, {C.~B\"ohm},
145:   Ed. Lecture Notes in Computer Science, vol.~37. Springer, Berlin, 369.
146: 
147: \bibitem[\protect\citeauthoryear{Scott}{Scott}{1976}]{scot76}
148: {\sc Scott, D.} 1976.
149: \newblock Data types as lattices.
150: \newblock {\em SIAM J. Comput.\/}~{\em 5,\/}~3, 522--587.
151: \newblock Semantics and correctness of programs.
152: 
153: \bibitem[\protect\citeauthoryear{Scott}{Scott}{1980a}]{scot80}
154: {\sc Scott, D.} 1980a.
155: \newblock Lambda calculus: Some models, some philosophy.
156: \newblock In {\em The Kleene Symposium}, {J.~Barwise}, {H.~J. Keisler}, {and}
157:   {K.~Kunen}, Eds. North-Holland, Amsterdam, 223--265.
158: 
159: \bibitem[\protect\citeauthoryear{Scott}{Scott}{1980b}]{scot80l}
160: {\sc Scott, D.~S.} 1980b.
161: \newblock Letter to {A}lbert {M}eyer.
162: \newblock CMU.
163: 
164: \bibitem[\protect\citeauthoryear{van Bakel}{van Bakel}{1992}]{bake92}
165: {\sc van Bakel, S.} 1992.
166: \newblock Complete restrictions of the intersection type discipline.
167: \newblock {\em Theoret. Comput. Sci.\/}~{\em 102,\/}~1, 135--163.
168: 
169: \bibitem[\protect\citeauthoryear{Vickers}{Vickers}{1989}]{vick89}
170: {\sc Vickers, S.} 1989.
171: \newblock {\em Topology via logic}.
172: \newblock Cambridge University Press, Cambridge.
173: 
174: \bibitem[\protect\citeauthoryear{Yokouchi}{Yokouchi}{1994}]{yoko94}
175: {\sc Yokouchi, H.} 1994.
176: \newblock F-semantics for type assignment systems.
177: \newblock {\em Theoret. Comput. Sci.\/}~{\em 129}, 39--77.
178: 
179: \end{thebibliography}
180: