{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:19:20Z","timestamp":1725455960067},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556312"},{"type":"electronic","value":"9783540472650"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/bfb0021082","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T00:35:18Z","timestamp":1132619718000},"page":"46-57","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Are subsets necessary in Martin-L\u00f6f type theory?"],"prefix":"10.1007","author":[{"given":"Simon","family":"Thompson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,16]]},"reference":[{"key":"4_CR1","unstructured":"Samson Abramsky and Chris Hankin, editors. Abstract Interpretation of Declarative Languages. Ellis-Horwood, 1987."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Roland Backhouse, Paul Chisholm, Grant Malcolm, and Erik Saaman. Do-it-yourself type theory. Formal Aspects of Computing, 1, 1989.","DOI":"10.1007\/BF01887198"},{"key":"4_CR3","unstructured":"Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc., 1986."},{"key":"4_CR4","unstructured":"Robert Harper. Introduction to Standard ML. Technical Report ECS-LFCS-86-14, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, November 1986."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In H. Rose and J. C. Shepherdson, editors, Logic Colloquium 1973. North-Holland, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"4_CR6","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In C. A. R. Hoare, editor, Mathematical Logic and Programming Languages. Prentice-Hall, 1985."},{"key":"4_CR7","unstructured":"Bengt Nordstr\u00f6m and Kent Petersson. Types and specifications. In IFIP'83. Elsevier, 1983."},{"key":"4_CR8","unstructured":"Bengt Nordstrom, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f's Type Theory \u2014 An Introduction, volume 7 of International Series of Monographs on Computer Science. Oxford University Press, 1990."},{"key":"4_CR9","unstructured":"Kent Petersson and Jan Smith. Program derivation in type theory: The Polish flag problem. In Peter Dybjer et al., editors, Proceedings of the Workshop on Specification and Derivation of Programs. Programming Methodology Group, University of Goteborg and Chalmers University of Technology, 1985. Technical Report, number 18."},{"key":"4_CR10","unstructured":"Simon Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall International, 1987."},{"key":"4_CR11","unstructured":"Anne Salvesen and Jan Smith. The strength of the subset type in Martin-L\u00f6f's type theory. In Proceedings of the Third Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, 1989."},{"key":"4_CR12","unstructured":"Peter Schroeder-Heister. Judgements of higher levels and standardized rules for logical constants in Martin-L\u00f6f's theory of logic. In Peter Dybjer et al., editors, Proceedings of the Workshop on Programming Logic. Programming Methodology Group, University of Goteborg and Chalmers University of Technology, 1989. Technical Report, number 54. This paper was written in 1985."},{"key":"4_CR13","unstructured":"Marco D. G. Swaen. Weak and Strong Sum-Elimination in Intuitionistic Type Theory. PhD thesis, University of Amsterdam, 1989."},{"key":"4_CR14","unstructured":"Simon Thompson. Type Theory and Functional Programming. Addison Wesley, 1991."}],"container-title":["Lecture Notes in Computer Science","Constructivity in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0021082","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T18:01:47Z","timestamp":1580320907000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0021082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556312","9783540472650"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0021082","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]},"assertion":[{"value":"16 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}