natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The concept of type of data in computer science.
Jim Morris, Types are not sets, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages (POPL), 1973. (doi)
John C. Reynolds, Towards a Theory of Type Structure, Colloquium on Programming, Paris, 9-11 April 1974. (pdf)
Barbara Liskov, Stephen Zilles, Programming with Abstract Data Types, Proceedings of Symposium on very high level languages, ACM SIGPLAN Notices 9 4 (1974) 50-59 [doi:10.1145/800233.807045, doi:10.1145/942572.807045]
“An abstract data type defines a class of abstract objects which is completely characterized by the operations available on those objects. This means that an abstract data type can be defined by defining the characterizing operations for that type.”
Arthur Sale, Primitive data types, The Australian Computer Journal 9 2 (1977) [Sale-PrimitiveDataTypes.pdf]
D. J. Lehmann, M. B., Smyth, Algebraic specification of data types: A synthetic approach, Math. Systems Theory 14 (1981) 97–139 [doi:10.1007/BF01752392]
(via CPOs in domain theory)
Last revised on May 29, 2024 at 16:14:04. See the history of this page for a list of all contributions to it.