Пирс Б. Типы в языках программирования
Подождите немного. Документ загружается.
B.3. Соглашения по именам и индексам 441
Clinger, William, Daniel P. Friedman, and Mitchell Wand. A scheme for a higher-level semantic algebra. In John
Reynolds and Maurice Nivat, editors, Algebraic Methods in Semantics, pages 237–250. Cambridge University
Press, 1985.
Colazzo, Dario and Giorgio Ghelli. Subtyping recursive types in Kernel Fun. In 14th Symposium on Logic in
Computer Science (LICS’99), pages 137–146. IEEE, July 1999.
Compagnoni, Adriana and Healfdene Goguen. Decidability of higher-order subtyping via logical
relations,December 1997a. Manuscript, available at ftp://www.dcs.ed.ac.uk/pub/hhg/hosdec.ps.gz.
Compagnoni, Adriana and Healfdene Goguen. Typed operational semantics for higher order subtyping.
Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997b.
Compagnoni, Adriana B. Decidability of higher-order subtyping with intersection types. In Computer Science
Logic, September 1994. Kazimierz, Poland. Springer Lecture Notes in Computer Science 933, June 1995.
Also available as University of Edinburgh, LFCS technical report ECS-LFCS-94-281, titled "Subtyping in is
decidable". Compagnoni, Adriana B. and Benjamin C. Pierce. Intersection types and multiple inheritance.
Mathematical Structures in Computer Science, 6(5):469–501, October 1996. Preliminary version available
as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer
science technical report 93-18, Aug. 1993, under the title "Multiple Inheritance via Intersection Types".
Constable, Robert L. Types in computer science, philosophy, and logic. In Samuel R. Buss, editor, Handbook
of Proof Theory, volume 137 of Studies in logic and the foundations of mathematics, pages 683–786. Elsevier,
1998.
Constable et al., Robert L. Implementing Mathematics with the NuPRL Proof Development System. Prentice-
Hall, Englewood Cliffs, NJ, 1986.
Cook, William. Object-oriented programming versus abstract data types. In J. W. de Bakker et al., editors,
Foundations of Object-Oriented Languages, volume 489 of Lecture Notes in Computer Science, pages 151–178.
Springer-Verlag, 1991.
Cook, William and Jens Palsberg. A denotational semantics of inheritance and its correctness. In ACM
Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), pages
433–444, 1989.
Cook, William R. A Denotational Semantics of Inheritance. PhD thesis,.Brown University, 1989.
Cook, William R., Walter L. Hill, and Peter S. Canning. Inheritance is not subtyping. In ACM Symposium
on Principles of Programming Languages (POPL), San Francisco, California, pages 125–135, January 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).
Coppo, Mario and Mariangiola Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv Math. Logik,
19:139–156, 1978.
Coppo, Mario, Mariangiola Dezani-Ciancaglini, and Patrick Sall´e. Functional characterization of some semantic
equalities inside λ-calculus. In Hermann A. Maurer, editor, Proceedings of the 6th Colloquium on Automata,
Languages and Programming, volume 71 of LNCS, pages 133–146, Graz, Austria, July 1979. Springer.
Coquand, Thierry. Une Th´eorie des Constructions. PhD thesis, University Paris VII, January 1985.
Coquand, Thierry and G´erard Huet. The Calculus of Constructions. Information and Computation,
76(2/3):95–120, February/March 1988.
Courcelle, Bruno. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.
Cousineau, Guy and Michel Mauny. The Functional Approach to Programming. Cambridge University Press,
1998.
rev. 104
442 B.3. Соглашения по именам и индексам
Crary, Karl. Sound and complete elimination of singleton kinds. Technical Report CMU-CS-00-104, Carnegie
Mellon University, School of Computer Science,January 2000.
Crary, Karl, Robert Harper, and Derek Dreyer. A type system for higher-order modules. In ACM Symposium
on Principles of Programming Languages (POPL), Portland, Oregon, 2002.
Crary, Karl, Robert Harper, and Sidd Puri. What is a recursive module? In ACM SIGPLAN Conference on
Programming Language Design and Implementation (PLDI), pages 50–63, May 1999.
Crary, Karl, Stephanie Weirich, and J. Gregory Morrisett. Intensional polymorphism in type-erasure semantics.
In International Conference on Functional Programming (ICFP), Baltimore, Maryland, USA, pages 301–312,
1998.
Crole, Roy. Categories for Types. Cambridge University Press, 1994.
Curien, Pierre-Louis and Giorgio Ghelli. Subtyping + extensionality: Confluence of βη-reductions in F . In
T. Ito and A. R. Meyer, editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in
Lecture Notes in Computer Science, pages 731–749. Springer-Verlag, September 1991.
Curien, Pierre-Louis and Giorgio Ghelli. Coherence of subsumption: Minimum typing and type-checking in F .
Mathematical Structures in Computer Science, 2:55–91, 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).
Curry, Haskell B. and Robert Feys. Combinatory Logic, volume 1. North Holland, 1958. Second edition,1968.
Damas, Luis and Robin Milner. Principal type schemes for functional programs. In ACM Symposium on
Principles of Programming Languages (POPL), Albuquerque,New Mexico, pages 207–212, 1982.
Danvy, Olivier. Type-directed partial evaluation. In John Hatcliff, Torben Æ. Mogensen, and Peter Thiemann,
editors, Partial Evaluation - Practice and Theory; Proceedings of the 1998 DIKU Summer School, number
1706 in Lecture Notes in Computer Science, pages 367–411, Copenhagen, Denmark, July 1998. Springer-
Verlag.
Davey, Brian A. and Hilary A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.
Davies, Rowan. A refinement-type checker for Standard ML. In International Conference on Algebraic
Methodology and Software Technology, volume 1349 of Lecture Notes in Computer Science. Springer-Verlag,
1997.
Davies, Rowan and Frank Pfenning. A modal analysis of staged computation. In ACM Symposium on Principles
of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 258–270, 1996.
de Bruijn, Nicolas G. Lambda-calculus notation with nameless dummies: a tool for automatic formula
manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381–392, 1972.
de Bruijn, Nicolas G. A survey of the project AUTOMATH.In J. P. Seldin and J. R. Hindley, editors, To H.
B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589–606. Academic Press,
1980.
De Millo, Richard A., Richard J. Lipton, and Alan J. Perlis. Social processes and proofs of theorems and
programs. Communications of the ACM, 22(5):271–280, May 1979. An earlier version appeared in ACM
Symposium on Principles of Programming Languages (POPL), Los Angeles, California, 1977pp. 206–214.
Detlefs, David L., K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Technical
Report 159, Compaq Systems Research Center (SRC), 1998. Also see http://research.compaq.com/SRC/
esc/overview.html.
Donahue, James and Alan Demers. Data types are values. ACM Transactions on Programming Languages and
Systems, 7(3):426–445, July 1985.
rev. 104
B.3. Соглашения по именам и индексам 443
Dowek, Gilles, Th´er`ese Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions:
The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference
and Symposium on Logic Programming, pages 259–273, Bonn, Germany, September 1996. MIT Press.
Drossopoulou, Sophia, Susan Eisenbach, and Sarfraz Khurshid. Is the Java Type System Sound?Theory
and Practice of Object Systems, 7(1):3–24, 1999. Summary in European Conference on Object-Oriented
Programming (ECOOP), 1997.
Duggan, Dominic and Adriana Compagnoni. Subtyping for object type constructors. In Workshop on
Foundations of Object-Oriented Languages (FOOL), informal proceedings, January 1999.
Dybvig, R. Kent. The Scheme Programming Language. Prentice-Hall, Inc., Englewood Cliffs, New Jersey,
second edition,1996. Available electronically at http://www.scheme.com/tsp12d/
Eidorff, Peter, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine B. Sørensen, and Mads Tofte.
AnnoDomini in practice: A type-theoretic approach to the Year 2000 problem. In Jean-Yves Girard, editor,
Proc. Symposium on Typed Lambda Calculus and Applications (TLCA), volume 1581 of Lecture Notes in
Computer Science, pages 6–13, L’Aquila, Italy, April 1999. Springer-Verlag.
Eifrig, Jonathan, Scott Smith, and Valery Trifonov. Type inference for recursively constrained types and
its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics
Conference, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.
Feinberg, Neal, Sonya E. Keene, Robert O. Mathews, and P. Tucker Withington. The Dylan Programming
Book. Addison-Wesley Longman, Reading, Mass., 1997.
Felleisen, Matthias and Daniel P. Friedman. A Little Java, A Few Patterns. MIT Press, Cambridge,
Massachusetts, 1998.
Felty, Amy, Elsa Gunter, John Hannan, Dale Miller, Gopalan Nadathur, and Andre Scedrov. Lambda prolog: An
extended logic programming language. In E. Lusk; R. Overbeek, editor, Proceedings on the 9th International
Conference on Automated Deduction, volume 310 of LNCS, pages 754–755, Berlin, May 1988. Springer.
Filinski, Andrzej. A semantic account of type-directed partial evaluation. In Gopalan Nadathur, editor,
Proceedings of the International Conference on Principles and Practice of Declarative Programming, number
1702 in Lecture Notes in Computer Science, pages 378–395, Paris, France, September 1999. Springer-Verlag.
Extended version available as technical report BRICS RS-99-17.
Filinski, Andrzej. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky,
editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in
Lecture Notes in Computer Science, pages 151–165, Krak´ow, Poland, May 2001. Springer-Verlag.
Fisher, Kathleen. Classes = objects + data abstraction. In Kim Bruce and Giuseppe Longo, editors, Workshop
on Foundations of Object-Oriented Languages (FOOL), informal proceedings, July 1996a. Invited talk. Also
available as Stanford University Technical Note STAN-CS-TN-96-31.
Fisher, Kathleen. Type Systems for object-oriented programming languages. PhD thesis, Stanford
University,1996b. STAN-CS-TR-98-1602.
Fisher, Kathleen, Furio Honsell, and John C. Mitchell. A lambda calculus of objects and method specialization.
Nordic J. Computing (formerly BIT), 1:3–37, 1994. Summary in Proc. IEEE Symp. on Logic in Computer
Science, 1993, 26–38.
Fisher, Kathleen and John Mitchell. The development of type systems for object-oriented languages. Theory
and Practice of Object Systems, 1(3):189–220, 1996.
Fisher, Kathleen and John C. Mitchell. On the relationship between classes, objects, and data abstraction.
Theory and Practice of Object Systems, 4(1):3–25, 1998.
rev. 104
444 B.3. Соглашения по именам и индексам
Fisher, Kathleen and John H. Reppy. The design of a class mechanism for Moby. In SIGPLAN Conference on
Programming Language Design and Implementation (PDLI), pages 37–49, 1999.
Flanagan, Cormac and Matthias Felleisen. Componential set-based analysis. ACM SIGPLAN Notices,
32(5):235–248, May 1997.
Flatt, Matthew and Matthias Felleisen. Units: Cool modules for HOT languages. In ACM SIGPLAN Conference
on Programming Language Design and Implementation (PLDI), Montreal, Canada, pages 236–248, 1998.
Flatt, Matthew, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In ACM Symposium on
Principles of Programming Languages (POPL), San Diego, California, January 1998a.
Flatt, Matthew, Shriram Krishnamurthi, and Matthias Felleisen. A programmer’s reduction semantics for
classes and mixins. Technical Report TR97-293, Computer Science Department, Rice University,February
1998b. Corrected June, 1999.
Freeman, Tim and Frank Pfenning. Refinement types for ML. In ACM SIGPLAN Conference on Programming
Language Design and Implementation (PLDI), Toronto, Ontario, June 1991.
Frege, Gottlob. Beagriffschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle:
L. Nebert, 1879. Available in several translations.
Friedman, Daniel P. and Matthias Felleisen. The Little Schemer. MIT Press, 1996.
Friedman, Daniel P., Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages.
McGraw-Hill Book Co., New York, N.Y.,second edition, 2001.
Friedman, Harvey. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium, volume 453 of
Lecture Notes in Mathematics, pages 22–37, Berlin, 1975. Springer-Verlag.
Gallier, Jean. On Girard’s "Candidats de reductibilit´e". In Piergiorgio Odifreddi, editor, Logic and Computer
Science, number 31 in APIC Studies in Data Processing, pages 123–203. Academic Press, 1990.
Gallier, Jean. Constructive logics. Part I: A tutorial on proof systems and typed λ-calculi. Theoretical Computer
Science, 110(2):249–339, March 1993.
Gandy, Robin O. The simple theory of types. In Logic Colloquium 76, volume 87 of Studies in Logic and the
Foundations of Mathematics, pages 173–181. North Holland, 1976.
Gapeyev, Vladimir, Michael Levin, and Benjamin Pierce. Recursive subtyping revealed. In International
Conference on Functional Programming (ICFP), Montreal, Canada, 2000. To appear in Journal of Functional
Programming.
Garrigue, Jaques and Hassan A¨ıt-Kaci. The typed polymorphic label-selective lambda-calculus. In ACM
Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 35–47, 1994.
Garrigue, Jaques and Didier R´emy. Extending ML with semi-explicit polymorphism. In Mart´ın Abadi and
Takayasu Ito, editors, International Symposium on Theoretical Aspects of Computer Software (TACS),
Sendai, Japan, pages 20–46. Springer-Verlag, September 1997.
Ghelli, Giorgio. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric
Polymorphism. PhD thesis, Universit`a di Pisa, March 1990. Technical report TD-6/90, Dipartimento di
Informatica, Universit`a di Pisa.
Ghelli, Giorgio. Recursive types are not conservative over F . In M. Bezen and J.F. Groote, editors, Typed
Lambda Calculi and Applications (TLCA), Utrecht, The Netherlands, number 664 in Lecture Notes in
Computer Science, pages 146–162, Berlin, March 1993. Springer-Verlag.
Ghelli, Giorgio. Divergence of F type checking. Theoretical Computer Science, 139 (1,2):131–162, 1995.
rev. 104
B.3. Соглашения по именам и индексам 445
Ghelli, Giorgio. Termination of system F-bounded: A complete proof. Information and Computation,
139(1):39–56, 1997.
Ghelli, Giorgio and Benjamin Pierce. Bounded existentials and minimal typing. Theoretical Computer Science,
193:75–96, 1998.
Gifford, David, Pierre Jouvelot, John Lucassen, and Mark Sheldon. FX-87 Reference Manual. Technical Report
MIT/LCS/TR-407, Massachusetts Institute of Technology, Laboratory for Computer Science, September
1987.
Girard, Jean-Yves. Interpr´etation fonctionnelle et ´elimination des coupures de l’arithm´etique d’ordre sup´erieur.
Th`ese d’´etat, Universit´e Paris VII, 1972. Summary in Proceedings of the Second Scandinavian Logic
Symposium (J.E. Fenstad, editor), North-Holland, 1971(pp. 63–92).
Girard, Jean-Yves. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
Girard, Jean-Yves, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in
Theoretical Computer Science. Cambridge University Press, 1989.
Glew, Neal. Type dispatch for named hierarchical types. In International Conference on Functional
Programming (ICFP), Paris, France,pages 172–182, 1999.
Gordon, Andrew. A tutorial on co-induction and functional programming. In Functional Programming, Glasgow
1994, pages 78–95. Springer Workshops in Computing, 1995.
Gordon, Michael J. Adding eval to ML. Manuscript, circa 1980.
Gordon, Michael J., Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF. Springer-Verlag LNCS 78,
1979.
Goto, Eiichi. Monocopy and associative algorithms in extended Lisp. Technical Report TR 74-03, University
of Tokyo,May 1974.
Goubault-Larrecq, Jean and Ian Mackie. Proof Theory and Automated Deduction (Applied Logic Series, V.
6). Kluwer, 1997.
Grattan-Guinness, Ivor. The search for mathematical roots, 1870–1940: Logics, set theories and the foundations
of mathematics from Cantor through Russell to G¨odel. Princeton University Press, 2001.
Gries, David, editor.Programming Methodology. Springer-Verlag, New York, 1978.
Gunter, Carl A. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.
Gunter, Carl A. and John C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics,
and Language Design. MIT Press, 1994.
Hall, Cordelia V., Kevin Hammond, Simon L. Peyton Jones, and Philip L. Wadler. Type classes in Haskell.
ACM Transactions on Programming Languages and Systems, 18 (2):109–138, March 1996.
Halmos, Paul R. Naive Set Theory. Springer, New York, 1987.
Harper, Robert. A simplified account of polymorphic references. Information Processing Letters, 51(4):201–206,
August 1994. See also (Harper, 1996).
Harper, Robert. A note on: "A simplified account of polymorphic references"[Inform. Process. Lett. 51 (1994),
no. 4, 201–206; MR 95f:68142]. Information Processing Letters, 57(1):15–16, January 1996. See (Harper,
1994).
Harper, Robert, Bruce Duba, and David MacQueen. First-class continuations in ML. Journal of Functional
Programming, 3(4), October 1993. Short version in POPL ’91.
rev. 104
446 B.3. Соглашения по именам и индексам
Harper, Robert, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM,
40(1):143–184, 1992. Summary in LICS’87.
Harper, Robert and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In ACM
Symposium on Principles of Programming Language (POPL), Portland, Oregon, pages 123–137, January
1994.
Harper, Robert, John C. Mitchell, and Eugenio Moggi. Higher-order modules and the phase distinction. In ACM
Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 341–354,
January 1990.
Harper, Robert and Greg Morrisett. Compiling polymorphism using intensional type analysis. In ACM
Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 130–141,
1995.
Harper, Robert and Benjamin Pierce. A record calculus based on symmetric concatenation. In ACM Symposium
on Principles of Programming Languages (POPL), Orlando, Florida, pages 131–142, January 1991. Extended
version available as Carnegie Mellon Technical Report CMU-CS-90-157.
Harper, Robert and Christopher Stone. A type-theoretic interpretation of Standard ML. In Gordon Plotkin,
Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner.
MIT Press, 2000.
Hasegawa, Ryu. Parametricity of extensionally collapsed term models of polymorphism and their categorical
properties. In Takayasu Ito and Albert Meyer, editors, Theoretical Aspects of Computer Software (TACS),
Sendai, Japan, 1991.
Hayashi, Susumu. Singleton, union and intersection types for program extraction. In T. Ito and A. R. Meyer,
editors, Theoretical Aspects of Computer Software (Sendai, Japan), number 526 in Lecture Notes in Computer
Science, pages 701–730. Springer-Verlag, September 1991. Full version in Information and Computation,
109(1/2):174–210, 1994.
Henglein, Fritz. Type inference with polymorphic recursion. ACM Transactions on Programming Languages
and Systems, 15(2):253–289, 1993.
Henglein, Fritz. Dynamic typing: syntax and proof theory. Science of Computer Programming, 22(3):197–230,
June 1994. Selected papers of the Fourth European Symposium on Programming (Rennes, 1992).
Henglein, Fritz and Harry G. Mairson. The complexity of type inference for higher-order typed lambda-calculi.
In ACM Symposium on Principles of Programming Languages (POPL), Orlando, Florida, pages 119–130,
January 1991.
Hennessy, Matthew. A Semantics of Programming Languages: An Elementary Introduction Using Operational
Semantics. John Wiley and Sons, 1990. Currently out of print; available from http://www.cogs.susx.ac.
uk/users/matthewh/semnotes.ps.gz.
Hennessy, Matthew and James Riely. Resource access control in systems of mobile agents. In Uwe Nestmann
and Benjamin C. Pierce, editors, HLCL ’98: High-Level Concurrent Languages (Nice, France, September 12,
1998),volume 16.3 of ENTCS, pages 3–17. Elsevier Science Publishers, 1998. Full version available as CogSci
Report 2/98, University of Sussex,Brighton.
Hindley, J. Roger. The principal type-scheme of an object in combinatory logic. Transaction of the American
Mathematical Society, 146:29–60, 1969.
Hindley, J. Roger. Types with intersection, an introduction. Formal Aspects of Computing, 4:470–486, 1992.
Hindley, J. Roger. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science.
Cambridge University Press, Cambridge 1997.
rev. 104
B.3. Соглашения по именам и индексам 447
Hindley, J. Roger and Jonathan P. Seldin. Introduction to Combinators and λ-Calculus, volume 1 of London
Mathematical Society Student Texts. Cambridge University Press, 1986.
Hoang, My, John Mitchell, and Ramesh Viswanathan. Standard ML-NJ weak polymorphism and imperative
constructs. In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 15–25.
IEEE Computer Society Press, 1993.
Hodas, J. S. Lolli: An extension of λProlog with linear context management. In D. Miller, editor, Workshop on
the λProlog Programming Language, pages 159–168, Philadelphia, Pennsylvania, August 1992.
Hofmann, Martin. Syntax and semantics of dependent types. In Semantics and Logic of Computation.
Cambridge University Press, 1997.
Hofmann, Martin and Benjamin Pierce. Positive subtyping. In ACM Symposium on Principles of Programming
Languages (POPL), San Francisco, California, pages 186–197, January 1995a. Full version in Information and
Computation, volume 126, number 1, April 1996. Also available as University of Edinburgh technical report
ECS-LFCS-94-303, September 1994.
Hofmann, Martin and Benjamin Pierce. A unifying type-theoretic framework for objects. Journal of Functional
Programming, 5(4):593–635, October 1995b. Previous versions appeared in the Symposium on Theoretical
Aspects of Computer Science, 1994, (pages 251–262) and, under the title "An Abstract View of Objects
and Subtyping (Preliminary Report),"as University of Edinburgh, LFCS technical report ECS-LFCS-92-226,
1992.
Hofmann, Martin and Benjamin C. Pierce. Type destructors. In Didier R´emy, editor, Informal proceedings of
the Fourth International Workshop on Foundations of Object-Oriented Languages (FOOL), January 1998.
Full version to appear in Information and Computation.
Hook, J.G. Understanding Russell - a first attempt. In Proc. Int. Symp. on Semantics of Data Types, Sophia-
Antipolis (France), Springer LNCS 173, pages 69–85. Springer-Verlag, 1984.
Hopcroft, John E. and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation.
Addison-Wesley, 1979.
Hosoya, Haruo and Benjamin Pierce. Regular expression pattern matching. In ACM Symposium on Principles
of Programming Languages (POPL), London, England,2001.
Hosoya, Haruo and Benjamin C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17,
University of Pennsylvania,June 1999.
Hosoya, Haruo and Benjamin C. Pierce. XDuce: A typed XML processing language (preliminary report). In
International Workshop on the Web and Databases (WebDB), May 2000.
Hosoya, Haruo, J´erˆome Vouillon, and Benjamin C. Pierce. Regular expression types for XML. ACM
Transactions on Programming Languages and Systems (TOPLAS), 2001. To appear; short version in ICFP
2000.
Howard, William A. Hereditarily majorizable functionals of finite type. In Anne Sjerp Troelstra, editor,
Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in
Mathematics, pages 454–461. Springer-Verlag, Berlin, 1973. Appendix.
Howard, William A. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors,
To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479–490. Academic
Press, New York, 1980. Reprint of 1969 article.
Howe, Douglas. Automating Reasoning in an Implementation of Constructive Type Theory. PhD thesis, Cornell
University,1988.
Hudak, Paul, S. Peyton Jones, P. Wadler, B. Boutel, J. Fairbairn, J. Fasel, M. M. Guzman, K. Hammond,
J. Hughes, T. Johnsson, D. Kieburtz, R. Nikhil, W. Partain, and J. Peterson. Report on the programming
language Haskell, version 1.2. SIGPLAN Notices, 27(5), May 1992.
rev. 104
448 B.3. Соглашения по именам и индексам
Huet, G´erard. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
Huet, G´erard. R´esolution d’equations dans les langages d’ordre 1,2, . . . ,ω. Th`ese de Doctorat d’Etat, Universit´e
de Paris 7(France), 1976.
Huet, G´erard, editor. Logical Foundations of Functional Programming. University of Texas at Austin Year of
Programming Series.Addison-Wesley, 1990.
Hyland, J. Martin E. and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Information and
Computation, 163(2):285–408, December 2000.
Igarashi, Atsushi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java
and GJ. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications
(OOPSLA), October 1999. Full version to appear in ACM Transactions on Programming Languages and
Systems (TOPLAS), 2001.
Igarashi, Atsushi and Benjamin C. Pierce. On inner classes. In European Conference on Object-Oriented
Programming (ECOOP), 2000. Also in informal proceedings of the Seventh International Workshop on
Foundations of Object-Oriented Languages (FOOL). To appear in Information and Computation.
Igarashi, Atsushi, Benjamin C. Pierce, and Philip Wadler. A recipe for raw types. In Workshop on Foundations
of Object-Oriented Languages (FOOL), 2001.
Ishtiaq, Samin and Peter O’Hearn. Bi as an assertion language for mutable data structures. In ACM Symposium
on Principles of Programming Languages (POPL), London, England,2001.
Jacobs, Bart. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of
Mathematics.North Holland, Elsevier, 1999.
Jagannathan, Suresh and Andrew Wright. Effective flow analysis for avoiding run-time checks. In Proceedings of
the Second International Static Analysis Symposium, volume 983 of LNCS, pages 207–224. Springer-Verlag,
1995.
Jay, C. Barry and Milan Sekanina. Shape checking of array programs. In Computing: The Australasian Theory
Seminar (Proceedings), volume 19 of Australian Computer Science Communications, pages 113–121, 1997.
Jim, Trevor. Rank-2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531,
Massachusetts Institute of Technology, Laboratory for Computer Science, November 1995.
Jim, Trevor. What are principal typings and what are they good for? In ACM, editor,ACM Symposium on
Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 42–53, 1996.
Jim, Trevor and Jens Palsberg. Type inference in systems of recursive types with subtyping. Manuscript, 1999.
Jones, Mark P. ML typing, explicit polymorphism, and qualified types,1994a.
Jones, Mark P. Qualified Types: Theory and Practice. Cambridge University Press, 1994b.
Jones, Richard and Rafael D. Lins. Garbage Collection: Algorithms for Automatic Dynamic Memory
Management. Wiley, 1996.
Jouvelot, Pierre and David Gifford. Algebraic reconstruction of types and effects. In ACM Symposium on
Principles of Programming Languages (POPL), Orlando,Florida, pages 303–310, January 1991.
Jutting, L.S. van Benthem, James McKinna, and Robert Pollack. Checking algorithms for Pure Type Systems.
In Henk Barendregt and Tobias Nipkow, editors, Proceedings of the International Workshop on Types for
Proofs and Programs, pages 19–61, Nijmegen, The Netherlands, May 1994. Springer-Verlag LNCS 806.
Kaes, Stefan. Parametric overloading in polymorphic programming languages. In H. Ganzinger, editor,
Proceedings of the European Symposium on Programming, volume 300 of Lecture Notes in Computer Science,
pages 131–144. Springer-Verlag, 1988.
rev. 104
B.3. Соглашения по именам и индексам 449
Kahn, Gilles. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science
(STACS), volume 247 of Lecture Notes in Computer Science, pages 22–39. Springer-Verlag, 1987.
Kamin, Samuel N. Inheritance in Smalltalk-80: A denotational definition. In ACM Symposium on Principles
of Programming Languages (POPL), San Diego, California, pages 80–87, January 1988.
Kamin, Samuel N. and Uday S. Reddy. Two semantic models of object-oriented languages. In Carl A. Gunter
and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and
Language Design, pages 464–495. MIT Press, 1994.
Katiyar, Dinesh, David Luckham, and John Mitchell. A type system for prototyping languages. In ACM
Symposium on Principles of Programming Languages (POPL), Portland, Oregon, pages 138–150, January
1994.
Katiyar, Dinesh and Sriram Sankar. Completely bounded quantification is decidable. In Proceedings of the
ACM SIGPLAN Workshop on ML and its Applications, June 1992.
Kelsey, Richard, William Clinger, and Jonathan Rees. Revised5 report on the algorithmic language Scheme.
Higher-Order and Symbolic Computation, 11(1):7–105, 1998. Also appears in ACM SIGPLAN Notices 33(9),
September 1998.
Kennedy, Andrew. Dimension types. In Donald Sannella, editor, Programming Languages and
Systems—ESOP’94, 5th European Symposium on Programming, volume 788 of Lecture Notes in Computer
Science, pages 348–362, Edinburgh, U.K., 11–13 April 1994. Springer.
Kernighan, Brian W. and Dennis M. Ritchie. The C Programming Language. Prentice Hall, Englewood Cliffs,
second edition,1988.
Kfoury, Assaf J., Harry Mairson, Franklyn Turbak, and Joe B. Wells. Relating typability and expressiveness in
finite-rank intersection type systems. In International Conference on Functional Programming (ICFP), Paris,
France, volume 34.9 of ACM Sigplan Notices, pages 90–101, N.Y., September 27–29 1999. ACM Press.
Kfoury, Assaf J. and Jerzy Tiuryn. Type reconstruction in finite-rank fragments of the polymorphic λ-calculus.
In Fifth Annual IEEE Symposium on Logic in Computer Science, pages 2–11, Philadelphia, PA, June 1990.
Full version in Information and Computation, 98(2), 228–257, 1992.
Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. ML typability is DEXPTIME-complete. In Proc. 15th
Colloq. on Trees in Algebra and Programming, pages 206–220. Springer LNCS 431, 1990.
Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. Type reconstruction in the presence of polymorphic
recursion. ACM Transactions on Programming Languages and Systems, 15(2):290–311, April 1993a.
Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. The undecidability of the semi-unification problem.
Information and Computation, 102(1):83–101, January 1993b. Summary in STOC 1990.
Kfoury, Assaf J., Jerzy Tiuryn, and Pawel Urzyczyn. An analysis of ML typability. Journal of the ACM,
41(2):368–398, March 1994.
Kfoury, Assaf J. and Joe B. Wells. Principality and decidable type inference for finite-rank intersection types.
In ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 161–174,
New York, NY, January 1999. ACM.
Kiczales, Gregor, Jim des Rivi`eres, and Daniel G. Bobrow. The Art of the Metaobject Protocol. MIT Press,
Cambridge, MA, 1991.
Kirchner, Claude and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of
unification. Research Report 561, Universit´e de Paris Sud, Orsay, France, April 1990.
Klop, Jan W. Combinatory Reduction Systems. Mathematical Centre Tracts 127.Mathematisch Centrum,
Amsterdam, 1980.
rev. 104
450 B.3. Соглашения по именам и индексам
Kobayashi, Naoki, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. In ACM Symposium
on Principles of Programming Languages (POPL), St. Petersburg Beach,Florida, 1996. Full version in ACM
Transactions on Programming Languages and Systems, 21(5), pp. 914–947, September 1999.
Kozen, Dexter, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In ACM Symposium
on Principles of Programming Languages (POPL), Charleston, South Carolina, pages 419–428, 1993.
Laan, Twan Dismas Laurens. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Techn.
Univ. Eindhoven, 1997.
Landin, Peter J. The mechanical evaluation of expressions. Computer Journal, 6: 308–320, January 1964.
Landin, Peter J. A correspondence between ALGOL 60 and Church’s lambda-notation: Parts I and II.
Communications of the ACM, 8(2,3):89–101, 158–165, February and March 1965.
Landin, Peter J. The next 700 programming languages. Communications of the ACM, 9(3):157–166, March
1966.
Lassez, Jean-Louis and Gordin Plotkin, editors.Computational Logic, Essays in Honor of Alan Robinson. MIT
Press, 1991.
L¨aufer, Konstantin. Polymorphic Type Inference and Abstract Data Types. PhD thesis, New York University,
1992.
L¨aufer, Konstantin and Martin Odersky. Polymorphic type inference and abstract data types. ACM
Transactions on Programming Languages and Systems (TOPLAS), 16(5):1411–1430, September 1994.
Summary in Phoenix Seminar and Workshop on Declarative Programming, Nov. 1991.
League, Christopher, Zhong Shao, and Valery Trifonov. Representing Java classes in a typed intermediate
language. In International Conference on Functional Programming (ICFP), Paris, France, September 1999.
League, Christopher, Valery Trifonov, and Zhong Shao. Type-preserving compilation of Featherweight Java. In
Foundations of Object-Oriented Languages (FOOL8), London, January 2001.
Lee, Oukseh and Kwangkeun Yi. Proofs about a folklore let-polymorphic type inference algorithm. ACM
Transactions on Programming Languages and Systems, 20 (4):707–723, July 1998.
Leivant, Daniel. Polymorphic type inference. In Proceedings of the 10th Annual ACM Symposium on Principles
of Programming Languages. ACM, 1983.
Lemmon, E. John, Carew A. Meredith, David Meredith, Arthur N. Prior, and Ivo Thomas. Calculi of pure
strict implication,1957. Mimeographed version, 1957; published in Philosophical Logic, ed. Davis, Hockney,
and Wilson, D. Reidel Co., Netherlands, 1969, pp. 215–250.
Leroy, Xavier. Manifest types, modules and separate compilation. In ACM Symposium on Principles of
Programming Languages (POPL), Portland, Oregon, pages 109–122, Portland, OR, January 1994.
Leroy, Xavier. The Objective Caml system: Documentation and user’s manual,2000. With Damien Doligez,
Jacques Garrigue, Didier R´emy, and J´erˆome Vouillon. Available from http://caml.inria.fr.
Leroy, Xavier and Michel Mauny. Dynamics in ML. In John Hughes, editor, ACM Symposium on Functional
Programming Languages and Computer Architecture (FPCA) 1991, volume 523 of Lecture Notes in Computer
Science, pages 406–426. Springer-Verlag, 1991.
Leroy, Xavier and Fran¸cois Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on
Programming Languages and Systems, 22(2):340–377, March 2000. Summary in ACM Symposium on
Principles of Programming Languages (POPL), San Antonio, Texas, 1999.
Leroy, Xavier and Fran¸cois Rouaix. Security properties of typed applets. In ACM Symposium on Principles of
Programming Languages (POPL), San Diego, California, pages 391–403, January 1998.
rev. 104