Пирс Б. Типы в языках программирования
Подождите немного. Документ загружается.
431
λM <: ResetCounterM . λo : Objec t M .
let {X , b } = o in
{*X ,
{ state = b. methods . reset ( b. state ) ,
me thods = b . methods }} as Object M ;
32.7.2. Решение: Свойство минимальной типизации не работает в исчислении, как мы его определили.
Рассмотрим терм
{# x={ a =5 , b =7}}
Ему можно присвоить любой из типов {#x:{a:Nat}} и {#x:{a:Nat,b:Nat}}, но эти два типа несравни-
мы. Один из разумных способов с этим справиться — явно указывать при каждом инвариантном поле
в терме-записи его требуемый тип. По существу, это заставляет программиста сделать выбор между
двумя указанными выше типами.
32.9.1. Решение:
MyCo u n t e r M =
λR . { get : R -> Nat , set : R -> Nat ->R , inc :R ->R , accesse s :R -> Nat ,
ba ckup :R ->R , reset :R - >R };
MyCo u n t e r R = {# x :Nat ,# count : Nat ,# old : Nat };
myCounterClass =
λR <: MyCounte r R .
λself : Unit - > MyCo u n t e rM R .
λ_ : Unit .
let super = instrCounter C l a s s [ R] self unit in
{ get = super . get ,
set = super .set ,
inc = super .inc ,
acc esses = super . accesses ,
reset = λs : R. s x = s. old ,
ba ckup = λs:R. s old =s.x }
as M yCounterM R;
mc = {* MyCounterR ,
{ state = {# x =0 ,# co unt =0 ,# old =0} ,
me thods = fix ( myCounterClass [ MyCounterR ]) unit }};
se ndget [ MyCoun t e r M ]
( sendre s e t [ M yCounterM ] ( sendi nc [ MyCounterM ] mc ));
Дорогой Уотсон,
проанализируйте факты, —
сказал он с легким
раздражением, — Вы знаете мой
метод. Примените его, будет
интересно сравнить результаты.
А. Конан-Дойль, Знак четырех
(1890), пер. М. Литвиновой
rev. 104
432
Безупречное изложение этой
идеи можно оставить в качестве
упражнения для читателя. Я
прибегаю здесь к любимому
трюку математиков, который
позволяет им перескакивать
через болотистые участки своих
теорий.
У.в.О. Куайн (1987)
rev. 104
Приложение B
Принятые обозначения
B.1. Имена метапеременных
В тексте В коде на ML Значение
p q, r, s, t, u s, t термы
x, y, z x, y термовые переменные
v, w v, w значения
nv nv числовые значения
l, j, k l метки полей в записях / метки вариантов
µ store состояния памяти
M, N, P, Q, S, T, U, V tyS, tyT типы
A, B, T tyA, tyB базовые типы
Σ структуры типизации памяти
X, Y, Z tyX, tyY типовые переменные
K, L kK, kL виды
σ подстановки
Γ, ∆ ctx контексты
J произвольные утверждения
D деревья вывода типов
C деревья вывода наследования
fi информация о позиции в файле
i, j, k, l численные индексы
B.2. Имена правил
Префикс Значение
B- вычисление с большим шагом
CT- типизация с ограничениями
E- вычисление
K- присвоение видов
M- сопоставление с образцом
P- типизация образцов
Q- эквивалентность типов
QR- параллельная редукция типов
S- наследование
SA- алгоритмическое наследование
T- типизация
TA- алгоритмическая типизация
XA- выявление
433
434 B.3. Соглашения по именам и индексам
B.3. Соглашения по именам и индексам
При выборе имен метапеременных, численных индексов и штрихов в них на протяжении всей книги
мы руководствовались следующими принципами:
1. В определениях синтаксиса для всех термов используется простая метапеременная t, для типов
— T, для значений — v и т. д.
2. В правилах типизации главный терм (тип которого вычисляется) всегда называется t, его под-
термы называются t
1
, t
2
, и т. д. (Иногда — например, в правилах редукции, — требуются имена
для подтермов подтермов; для них мы используем t
11
, t
12
и т. д.)
3. В правилах вычисления весь редуцируемый терм называется t, а терм-результат редукции назы-
вается t .
4. Тип терма t назывется T. (Подобным образом, типом t
1
будет T
1
и т. п.)
5. Те же принципы используются также при формулировке и доказательстве теорем, только иногда
t заменяется на s (а T на S или R и т. п.), чтобы избежать смешения имен между определениями
и теоремами.
В некоторых случаях выполнить все эти правила одновременно оказывается невозможно. Тогда
правила, указанные раньше, имеют больший приоритет. (Например, в правиле T-Proj1 на Рис. 11.5
правило 4 ослабляется: типом подтерма t
1
служит T
1
T
2
.) Очень редко (например, в правиле проекции
для записей T-Proj на Рис. 11.7) правила игнорируются совсем, поскольку их выполнение привело бы
к слишком безобразным или нечитаемым результатам.
rev. 104
Список литературы
Abadi, Mart´ın. Secrecy by typing in security protocols. Journal of the ACM, 46(5): 749–786, September 1999.
Summary in Theoretical Aspects of Computer Software (TACS), Sendai, Japan, 1997; volume 1281 of Springer
LNCS.
Abadi, Mart´ın, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In ACM
Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 147–160, 1999.
Abadi, Mart´ın and Luca Cardelli. On subtyping and matching. In European Conference on Object-Oriented
Programming (ECOOP), pages 145–167, 1995.
Abadi, Mart´ın and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.
Abadi, Mart´ın, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. Theoretical
Computer Science, 121(1–2):9–58, 6 December 1993. Summary in ACM Symposium on Principles of
Programming Languages (POPL), Charleston, South Carolina, 1993.
Abadi, Mart´ın, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L´evy. Explicit substitutions. Journal of
Functional Programming, 1(4):375–416, 1991a. Summary in ACM Symposium on Principles of Programming
Languages (POPL), San Francisco, California, 1990.
Abadi, Mart´ın, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin. Dynamic typing in a statically typed
language. ACM Transactions on Programming Languages and Systems, 13(2):237–268, April 1991b. Summary
in ACM Symposium on Principles of Programming Languages (POPL), April 1989.
Abadi, Mart´ın, Luca Cardelli, Benjamin Pierce, and Didier R´emy. Dynamic typing in polymorphic languages.
Journal of Functional Programming, 5(1):111–130, January 1995. Summary in ACM SIGPLAN Workshop
on ML and its Applications, June 1992.
Abadi, Mart´ın, Luca Cardelli, and Ramesh Viswanathan. An interpretation of objects and object types. In
ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages
396–409, 1996.
Abadi, Mart´ın and Marcelo P. Fiore. Syntactic considerations on recursive types. In Proceedings of the 11th
Annual IEEE Symposium on Logic in Computer Science, LICS ’96, pages 242–252. IEEE Computer Society
Press, Los Alamitos, CA, July 1996.
Abelson, Harold and Gerald Sussman. Structure and Interpretation of Computer Programs. MIT Press, New
York, 1985. Second edition, 1996.
Abramsky, Samson, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for pcf. Information and
Computation, 163(2):409–470, December 2000.
Aczel, Peter. An introduction to inductive definitions. In Jon Barwise, editor, Hand-book of Mathematical
Logic, number 90 in Studies in Logic and the Foundations of Mathematics, pages 739–782. North Holland,
1977.
435
436 B.3. Соглашения по именам и индексам
Aczel, Peter. Non-Well-Founded Sets. Stanford Center for the Study of Language and Information,1988. CSLI
Lecture Notes number 14.
Agesen, Ole, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language.
In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA),
pages 49–65, Atlanta, GA, October 1997.
Aho, Alfred V., Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-
Wesley, Reading, MA, USA, 1986.
Aiken, Alexander and Edward L. Wimmers. Type inclusion constraints and type inference. In ACM Symposium
on Functional Programming Languages and Computer Architecture (FPCA), pages 31–41, 1993.
Amadio, Roberto M. and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming
Languages and Systems, 15(4):575–631, 1993. Summary in ACM Symposium on Principles of Programming
Languages (POPL), Orlando, Florida, pp. 104–118; also DEC/Compaq Systems Research Center Research
Report number 62, August 1990.
Appel, Andrew W. Modern Compiler Implementation in ML. Cambridge University Press, 1998.
Appel, Andrew W. and Marcelo J. R. Gon¸calves. Hash-consing garbage collection. Technical Report CS-TR-
412-93, Princeton University, Computer Science Department,1993.
Arbib, Michael and Ernest Manes. Arrows, Structures, and Functors: The Categorical Imperative. Academic
Press, 1975.
Ariola, Zena M., Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. A call-by-need lambda
calculus. In ACM Symposium on Principles of Programming Languages (POPL), San Francisco, California,
pages 233–246, January 1995.
Arnold, Ken and James Gosling. The Java Programming Language. Addison Wesley, 1996.
Arnold, Ken, Ann Wollrath, Bryan O’Sullivan, Robert Scheifler, and Jim Waldo. The Jini specification. Addison-
Wesley, Reading, MA, USA, 1999.
Asperti, Andrea and Giuseppe Longo. Categories, Types, and Structures: An Introduction to Category Theory
for the Working Computer Scientist. MIT Press, 1991.
Aspinall, David. Subtyping with singleton types. In Computer Science Logic (CSL), Kazimierz,Poland, pages
1–15. Springer-Verlag, 1994.
Aspinall, David and Adriana Compagnoni. Subtyping dependent types. Information and Computation,
266(1–2):273–309, September 2001. Preliminary version in IEEE Symposium on Logic in Computer Science
(LICS), 1996.
Astesiano, Egidio. Inductive and operational semantics. In E. J. Neuhold and M. Paul, editors, Formal
Description of Programming Concepts, IFIP State-of-the-Art Reports, pages 51–136. Springer-Verlag, 1991.
Augustsson, Lennart. A compiler for Lazy ML. In ACM Symposium on Lisp and Functional Programming
(LFP), Austin, Texas, pages 218–227, August 1984.
Augustsson, Lennart. Cayenne — a language with dependent types. In International Conference on Functional
Programming (ICFP), Baltimore, Maryland, USA, pages 239–250, 1998.
Baader, Franz and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
Baader, Franz and J¨org Siekmann. Unification theory. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson,
editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, Deduction
Methodologies, pages 41–125. Oxford University Press, Oxford, UK, 1994.
rev. 104
B.3. Соглашения по именам и индексам 437
Backus, John. Can programming be liberated from the von Neumann style? A functional style and its algebra
of programs. Communications of the ACM, 21(8):613– 641, August 1978. Reproduced in Selected Reprints
on Dataflow and Reduction Architectures, ed. S. S. Thakkar, IEEE, 1987, pp. 215–243, and in ACM Turing
Award Lectures: The First Twenty Years, ACM Press, 1987, pp. 63–130.
Backus, John. The history of Fortran I, II, and III. In Wexelblat, editor,History of Programming Languages,
pages 25–45. Academic Press, 1981.
Bainbridge, E. Stewart, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism.
Theoretical Computer Science, 70(1):35–64, 1990. Corrigendum in TCS 71(3), 431.
Baldan, Paolo, Giorgio Ghelli, and Alessandra Raffaet`a. Basic theory of F-bounded quantification. Information
and Computation, 153(1):173–237, 1999.
Barendregt, Henk P. The Lambda Calculus. North Holland, revised edition, 1984.
Barendregt, Henk P. Functional programming and lambda calculus. In Jan van Leeuwen, editor, Handbook of
Theoretical Computer Science, Volume B, chapter 7, pages 321–364. Elsevier / MIT Press, 1990.
Barendregt, Henk P. Introduction to generalized type systems. Journal of Functional Programming,
1(2):125–154, 1991.
Barendregt, Henk P. Lambda calculi with types. In Abramsky, Gabbay, and Maibaum, editors,Handbook of
Logic in Computer Science, volume II. Oxford University Press, 1992.
Barras, Bruno, Samuel Boutin, Cristina Cornes, Judicael Courant, Jean-Christophe Filliatre, Eduardo Gimenez,
Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring,
Amokrane Saibi, and Benjamin Werner. The Coq proof assistant reference manual : Version 6.1. Technical
Report RT-0203, Inria (Institut National de Recherche en Informatique et en Automatique), France, 1997.
Barwise, Jon and Lawrence Moss. Vicious Circles: On the Mathematics of Non-wellfounded Phenomena.
Cambridge University Press, 1996.
Berardi, Stefano. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other
systems in Barendregt’s cube. Technical report, Department of Computer Science, CMU, and Dipartimento
Matematica, Universita di Torino, 1988.
Berger, Ulrich. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors,
Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science,pages 91–106,
Utrecht, The Netherlands, March 1993. Springer-Verlag
Berger, Ulrich and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In
Gilles Kahn, editor, IEEE Symposium on Logic in Computer Science (LICS), pages 203–211, Amsterdam,
The Netherlands, July 1991. IEEE Computer Society Press.
Birtwistle, Graham M., Ole-Johan Dahl, Bjorn Myhrhaug, and Kristen Nygaard. Simula Begin.
Studentlitteratur (Lund, Sweden), Bratt Institut fuer neues Lernen (Goch, FRG), Chartwell-Bratt Ltd (kent,
England), 1979.
Bobrow, Daniel G., Linda G. DeMichiel, Richard P. Gabriel, Sonya E. Keene, Gregor Kiczales, and David A.
Moon. Common Lisp Object System specification X3J13 document 88-002R. SIGPLAN Notices, 23, 1988.
Boehm, Hans-J. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations
of Computer Science, pages 339–345. IEEE, October 1985.
Boehm, Hans-J. Type inference in the presence of type abstraction. In ACM SIGPLAN Conference on
Programming Language Design and Implementation (PLDI), Portland,Oregon, pages 192–206, June 1989.
B¨ohm, Corrado and Alessandro Berarducci. Automatic synthesis of typed Λ-programs on term algebras.
Theoretical Computer Science, 39(2–3):135–154, August 1985.
rev. 104
438 B.3. Соглашения по именам и индексам
Bono, Viviana and Kathleen Fisher. An imperative first-order calculus with object extension. In European
Conference on Object-Oriented Programming (ECOOP), 1998.
Bono, Viviana, Amit J. Patel, and Vitaly Shmatikov. A core calculus of classes and mixins. In European
Conference on Object-Oriented Programming (ECOOP), volume 1628 of Lecture Notes in Computer Science,
pages 43–66. Springer-Verlag, June 1999a.
Bono, Viviana, Amit J. Patel, Vitaly Shmatikov, and John C. Mitchell. A core calculus of classes and objects.
In Fifteenth Conference on the Mathematical Foundations of Programming Semantics, April 1999b.
Bracha, Gilad, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past:
Adding genericity to the Java programming language. In Craig Chambers, editor, ACM Symposium on Object
Oriented Programming: Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices volume
33 number 10, pages 183–200, Vancouver, BC, October 1998.
Braithwaite, Richard B. The Foundations of Mathematics: Collected Papers of Frank P. Ramsey. Routledge
and Kegan Paul, London, 1931.
Brandt, Michael and Fritz Henglein. Coinductive axiomatization of recursive type equality and subtyping. In
Roger Hindley, editor, Proc. 3d Int’l Conf. on Typed Lambda Calculi and Applications (TLCA), Nancy,
France, April 2–4, 1997, volume 1210 of Lecture Notes in Computer Science (LNCS), pages 63–81. Springer-
Verlag, April 1997. Full version in Fundamenta Informaticae, Vol. 33, pp. 309–338, 1998.
Breazu-Tannen, Val, Thierry Coquand, Carl Gunter, and Andre Scedrov. Inheritance as implicit coercion.
Information and Computation, 93:172–221, 1991. Also in Carl A. Gunter and John C. Mitchell, editors,
Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press,
1994).
Bruce, Kim B. The equivalence of two semantic definitions for inheritance in object-oriented languages. In
Proceedings of Mathematical Foundations of Programming Semantics, Pittsburgh, PA, March 1991.
Bruce, Kim B. A paradigmatic object-oriented programming language: Design, static typing and semantics.
Journal of Functional Programming, 4(2), April 1994. Summary in ACM Symposium on Principles of
Programming Languages (POPL), Charleston, South Carolina, under the title "Safe type checking in a
statically typed object-oriented programming language".
Bruce, Kim B. Foundations of Object-Oriented Languages: Types and Semantics. MIT Press, 2002.
Bruce, Kim B., Luca Cardelli, Giuseppe Castagna, the Hopkins Objects Group (Jonathan Eifrig, Scott Smith,
Valery Trifonov), Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object
Systems, 1(3):221–242, 1996.
Bruce, Kim B., Luca Cardelli, and Benjamin C. Pierce. Comparing object encodings. Information and
Computation, 155(1/2):108–133, November 1999. Special issue of papers from Theoretical Aspects of
Computer Software (TACS 1997). An earlier version appeared as an invited lecture in the Third International
Workshop on Foundations of Object Oriented Languages (FOOL 3), July 1996.
Bruce, Kim B. and Giuseppe Longo. A modest model of records, inheritance, and bounded quantification.
Information and Computation, 87:196–240, 1990. Also in Carl A. Gunter and John C. Mitchell, editors,
Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press,
1994). An earlier version appeared in the proceedings of the IEEE Symposium on Logic in Computer Science,
1988.
Bruce, Kim B. and John Mitchell. PER models of subtyping, recursive types and higher-order polymorphism.
In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, January
1992.
Bruce, Kim B., Leaf Petersen, and Adrian Fiech. Subtyping is not a good "match"for object-oriented languages.
In European Conference on Object-Oriented Programming (ECOOP), volume 1241 of Lecture Notes in
Computer Science, pages 104–127. Springer-Verlag, 1997.
rev. 104
B.3. Соглашения по именам и индексам 439
Buneman, Peter and Benjamin Pierce. Union types for semistructured data. In Internet Programming
Languages. Springer-Verlag, September 1998. Proceedings of the International Database Programming
Languages Workshop. LNCS 1686.
Burstall, Rod and Butler Lampson. A kernel language for abstract data types and modules. In G. Kahn, D.
MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer
Science, pages 1–50. Springer-Verlag, 1984.
Burstall, Rod M. Proving properties of programs by structural induction. The Computer Journal, 12(1):41–48,
1969.
Canning, Peter, William Cook, Walt Hill, and Walter Olthoff. Interfaces for strongly-typed object-oriented
programming. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications
(OOPSLA), pages 457–467, 1989a.
Canning, Peter, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-bounded quantification for
object-oriented programming. In ACM Symposium on Functional Programming Languages and Computer
Architecture (FPCA), pages 273–280, September 1989b.
Canning, Peter, Walt Hill, and Walter Olthoff. A kernel language for object-oriented programming. Technical
Report STL-88-21, Hewlett-Packard Labs, 1988.
Cardelli, Luca. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors,
Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51–67. Springer-Verlag,
1984. Full version in Information and Computation, 76(2/3):138–164, 1988.
Cardelli, Luca. Amber. In Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet, editors, Combinators
and Functional Programming Languages, pages 21–47. Springer-Verlag, 1986. Lecture Notes in Computer
Science No. 242.
Cardelli, Luca. Basic polymorphic typechecking. Science of Computer Programming, 8(2):147–172, April 1987.
An earlier version appeared in the Polymorphism Newsletter, January, 1985.
Cardelli, Luca. Structural subtyping and the notion of power type. In ACM Symposium on Principles of
Programming Languages (POPL), San Diego, California, pages 70–79, January 1988a.
Cardelli, Luca. Typechecking dependent types and subtypes. In M. Boscarol, L. Carlucci Aiello, and G. Levi,
editors, Foundations of Logic and Functional Programming, Workshop Proceedings, Trento, Italy, (Dec.
1986), volume 306 of Lecture Notes in Computer Science, pages 45–57. Springer-Verlag 1988b.
Cardelli, Luca. Notes about F
ω
. Unpublished manuscript, October 1990.Cardelli, Luca. Typeful programming.
In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991.
An earlier version appeared as DEC/Compaq Systems Research Center Research Report N45, February 1989.
Cardelli, Luca. Extensible records in a pure calculus of subtyping. Research report 81, DEC/Compaq Systems
Research Center, January 1992. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects
of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).
Cardelli, Luca. An implementation of F :. Research report 97, DEC/Compaq Systems Research Center,
February 1993.
Cardelli, Luca. Type systems. In Allen B. Tucker, editor, Handbook of Computer Science and Engineering.
CRC Press, 1996.
Cardelli, Luca, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. Modula-3 report
(revised). Research report 52, DEC/Compaq Systems Research Center, November 1989.
Cardelli, Luca and Xavier Leroy. Abstract types and the dot notation. In Proceedings of the IFIP TC2 Working
Conference on Programming Concepts and Methods. North Holland, 1990. Also appeared as DEC/Compaq
SRC technical report 56.
rev. 104
440 B.3. Соглашения по именам и индексам
Cardelli, Luca and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming,
1(4):417–458, October 1991. Summary in ACM Conference on Lisp and Functional Programming, June
1990. Also available as DEC/Compaq SRC Research Report 55, Feb. 1990.
Cardelli, Luca, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of System F with subtyping.
Information and Computation, 109(1–2):4–56, 1994. Summary in TACS ’91 (Sendai, Japan,pp. 750–770).
Cardelli, Luca and John Mitchell. Operations on records. Mathematical Structures in Computer Science,
1:3–48, 1991. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented
Programming: Types, Semantics, and Language Design (MIT Press, 1994); available as DEC/Compaq
Systems Research Center Research Report #48, August, 1989, and in the proceedings of MFPS ’89, Springer
LNCS volume 442.
Cardelli, Luca and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing
Surveys, 17(4):471–522, December 1985.
Cardone, Felice. Relational semantics for recursive types and bounded quantification. In Proceedings of the
Sixteenth International Colloquium on Automata, Languages, and Programming, volume 372 of Lecture
Notes in Computer Science, pages 164–178, Stresa, Italy, July 1989. Springer-Verlag.
Cardone, Felice and Mario Coppo. Type inference with recursive types: Syntax and semantics. Information and
Computation, 92(1):48–80, 1991.
Cartwright, Robert and Guy L. Steele, Jr. Compatible genericity with run-time types for the Java programming
language. In Craig Chambers, editor, ACM Symposium on Object Oriented Programming: Systems,
Languages, and Applications (OOPSLA), Vancouver, British Columbia, SIGPLAN Notices 33(10), pages
201–215. ACM, October 1998.
Castagna, Giuseppe. Object-Oriented Programming: A Unified Foundation. Springer-Verlag, 1997.
Castagna, Giuseppe, Giorgio Ghelli, and Giuseppe Longo. A calculus for over-loaded functions with subtyping.
Information and Computation, 117(1):115–135, 15 February 1995. preliminary version in LISP and Functional
Programming, July 1992 (pp. 182–192), and as Rapport de Recherche LIENS-92-4, Ecole Normale Sup´erieure,
Paris.
Chambers, Craig. Object-oriented multi-methods in Cecil. In European Conference on Object-Oriented
Programming (ECOOP), pages 33–56, 1992.
Chambers, Craig. The Cecil language: Specification and rationale. Technical report, University of Washington,
March 1993.
Chambers, Craig and Gary Leavens. Type-checking and modules for multi-methods. In ACM Symposium on
Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 1994. SIGPLAN
Notices 29(10).
Chen, Gang and Giuseppe Longo. Subtyping parametric and dependent types. In Kamareddine et al.,
editor,Type Theory and Term Rewriting, September 1996. Invited lecture.
Chirimar, Jawahar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation
of linear logic. Journal of Functional Programming, 6(2): 195–244, March 1996.
Church, Alonzo. An unsolvable problem of elementary number theory. American Journal of Mathematics,
58:354–363, 1936.
Church, Alonzo. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
Church, Alonzo. The Calculi of Lambda Conversion. Princeton University Press, 1941.
Clement, Dominique, Joelle Despeyroux, Thierry Despeyroux, and Gilles Kahn. A simple applicative language:
Mini-ML. In ACM Conference on LISP and Functional Programming, pages 13–27, 1986.
rev. 104