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 and Stephen Zilles, Programming with Abstract Data Types, Proceedings of the ACM SIGPLAN symposium on Very high level languages, pp. 50-59, 1974. (doi) (citeseer)
Arthur Sale, Primitive data types, The Australian Computer Journal, Vol. 9, No. 2, July 1977 (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 January 20, 2024 at 10:55:10. See the history of this page for a list of all contributions to it.