Data types are values

ABSTRACT

An important goal of programming language research is to isolate the fundamenal concepts of languages, those basic ideas that allow us to understand the relationships among various language features. This paper examines one of these underlying notions, that of data type, with particular attention to the treatment of generic or polymorphic procedures and static type-checking.

REFERENCES

• 1: John Backus, Can programming be liberated from the von Neumann style?: a functional style and its algebra of programs, Communications of the ACM, v.21 n.8, p.613-641, Aug. 1978 [doi>10.1145/359576.359579]
• 2: Joseph L. Bates , Robert L. Constable, Proofs as Programs, Cornell University, Ithaca, NY, 1983
• 3: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• 4: Alan J. Demers , James E. Donahue, Data types, parameters and type checking, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-23, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567448]
• 5: Alan Demers , James Donahue, "Type-completeness" as a language principle, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-244, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567469]
• 6: Alan Demers , James Donahue, Making variables abstract: an equational theory for Russell, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.59-72, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567075]
• 7: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 8: DIJKSTRA, E.W. On the BLUE language submitted to the DoD. SIGPLAN Not. 13, 10 (Oct. 1978), 10-15.
• 9: DONAHUE, J. On the semantics of "data types." SIAM J. Comput. 8, 4 (Nov. 1979), 546-560.
• 10: GOGUEN, J. A., THATCHER, J. W., AND WAGNER, E. G. An initial algebra approach to the specification, correctness, and implementation of abstract data types. Tech. Rep. RC6487, IBM Thomas J. Watson Research Center, 1976.
• 11: David Gries , Narain Gehani, Some ideas on data types in high-level languages, Communications of the ACM, v.20 n.6, p.414-420, June 1977 [doi>10.1145/359605.359624]
• 12: GUTTAG, J.V. The specification and application to programming of abstract data types. Tech. Rep. CSRG-59, Computer Systems Research Group, Univ. of Toronto, 1975.
• 13: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 14: Christopher Thomas Haynes, A theory of data type representation independence, 1982
• 15: HOARE, C. A.R. Notes on data structuring. In Structured Programming, Dahl, Dijkstra, and Hoare, Eds., Academic Press, New York, 1972, 83-174.
• 16: K Jensen , N Wirth , A B Mickel , J F Miner, Pascal user manual and report; 3rd ed., Springer-Verlag New York, Inc., New York, NY, 1985
• 17: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 18: LANDIN, P.J. A formal description of Algol60. In Formal Language Description Languages. Steele, Ed., North-Holland, Amsterdam, 1966.
• 19: Barbara Liskov , Alan Snyder , Russell Atkinson , Craig Schaffert, Abstraction mechanisms in CLU, Communications of the ACM, v.20 n.8, p.564-576, Aug. 1977 [doi>10.1145/359763.359789]
• 20: MARTIN-LOt, P. Constructive mathematics and computer programming. In Proceedings of the 6th International Congress {or Logic, Methodology, and Philosophy of Science (Hanover, Aug. 1979).
• 21: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 22: Robert Milne , C. Strachey, A Theory of Programming Language Semantics, Halsted Press, New York, NY, 1977
• 23: MILNER, g. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17 (1978), 348-375.
• 24: POLYA, G. How to Solve It. Princeton University Press, Princeton, N.J., 1973.
• 25: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 26: John C. Reynolds, Syntactic control of interference, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.39-46, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512766]
• 27: SCOTT, D. Data types as lattices. SlAM J. Comput. 5, 3 (Sept. 1976), 522-587.}
• 28: Dana S. Scott, Logic and programming languages, Communications of the ACM, v.20 n.9, p.634-641, Sept. 1977 [doi>10.1145/359810.359826]
• 29: TENNENT, R. Language design methods based on semantic principles. Acta Inf. 8, 2 (1977), 97- 112.
• 30: WULF, W., LONDON, R., AND SHAW, M. Abstraction and verification in Alphard: Introduction to language and methodology. In ALPHARD: Form and Content, M. Shaw, Ed., Springer-Verlag, New York, 1981.
• 31: WULF, W. Private communication.
• 32: WULF, W., E. An information definition of Alphard. In ALPHARD: Form and Content, M. Shaw, Ed., Springer-Verlag, New York, 1981.

INDEX TERMS

Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: RUSSELL
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Languages, Theory