{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:39:22Z","timestamp":1748367562689},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_71","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:47:32Z","timestamp":1330210052000},"page":"701-730","source":"Crossref","is-referenced-by-count":12,"title":["Singleton, union and intersection types for program extraction"],"prefix":"10.1007","author":[{"given":"Susumu","family":"Hayashi","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"34_CR1","unstructured":"H. Barendregt. Introduction to generalized type systems. Technical Report no.90\u20138, University of Nijmegen, May 1990."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In Theoretical Aspect of Computer Science, Sendai, 1991. To appear.","DOI":"10.1007\/3-540-54415-1_69"},{"key":"34_CR3","unstructured":"R. Burstall and J. McKinna. Deliverable: an approach to program development in the calculus of constructions. An earlier version is in the preliminary proceeding of the Logical Frameworks BRA meeting at Sophia Antipolis 1990, April 1991."},{"key":"34_CR4","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1016\/0890-5401(90)90044-I","volume":"85","author":"K.B. Bruce","year":"1990","unstructured":"K.B. Bruce, A.R. Meyer, and J. C. Mitchell. The semantics of second-order lambda calculus. Information and Computation, 85:76\u2013134, 1990.","journal-title":"Information and Computation"},{"key":"34_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand and G. Huet. Calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"34_CR6","unstructured":"Th. Coquand. An analysis of Girard's paradox. In Proceedings of First Annual Symposium on Logic in Computer Science, 1986."},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"T. Freeman and F. Pfenning. Refinement types for ML. In ACM SIGPLAN'91 Conference on Programming Language Design and Implementation, Toronto, Ontario. ACM Press, June 1991.","DOI":"10.1145\/113445.113468"},{"key":"34_CR8","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/978-1-4613-0609-2_4","volume-title":"MATHEMATICAL LOGIC","author":"S. Hayashi","year":"1990","unstructured":"S. Hayashi. Constructive mathematics and computer-aided reasoning systems. In P.P. Petkov, editor, MATHEMATICAL LOGIC, pages 43\u201352. Plenum Press, New York, 1990."},{"key":"34_CR9","volume-title":"PX: A Computational Logic","author":"S. Hayashi","year":"1988","unstructured":"S. Hayashi and H. Nakano. PX: A Computational Logic. The MIT Press, Cambridge, Mass., 1988."},{"key":"34_CR10","first-page":"149","volume":"26","author":"J.-L. Krivine","year":"1990","unstructured":"J.-L. Krivine and M. Parigot. Programming with proofs. Journal of Information Processing and Cybernetics EIK, 26:149\u2013167, 1990.","journal-title":"Journal of Information Processing and Cybernetics EIK"},{"key":"34_CR11","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","volume":"44","author":"D. Leivant","year":"1986","unstructured":"D. Leivant. Typing and convergence in the lambda calculus. Theoretical Computer Science, 44:51\u201368, 1986.","journal-title":"Theoretical Computer Science"},{"key":"34_CR12","unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, Department of Computer Science, University of Edinburgh, July 1990."},{"key":"34_CR13","unstructured":"P. Martin-L\u00f6f. A theory of types. Unpublished manuscript, 1972."},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"J. C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365\u2013458. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50013-5"},{"key":"34_CR15","unstructured":"E. Moggi. The Partial Lambda-Calculus. PhD thesis, Department of Computer Science, University of Edinburgh, 1988."},{"key":"34_CR16","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/S0019-9958(86)80019-5","volume":"71","author":"D. MacQueen","year":"1986","unstructured":"D. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95\u2013130, 1986.","journal-title":"Information and Control"},{"key":"34_CR17","volume-title":"Programming in Martin-L\u00f6f's type theory, an introduction","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J.M. Smith. Programming in Martin-L\u00f6f's type theory, an introduction. Clarendon Press, Oxford, 1990."},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"M. Parigot. Programming with proofs: a second order type theory. In ESOP '88 (Lecture Notes in Computer Science No. 300). Springer-Verlag, 1988.","DOI":"10.1007\/3-540-19027-9_10"},{"key":"34_CR19","unstructured":"M. Parigot. Recursive programming with proofs. In Proceedings of Symposium Mathematiques et Informatique, Luminy, France, October 1989. To appear in Theoretical Computer Science."},{"key":"34_CR20","unstructured":"B.C. Pierce. Preliminary investigation of a calculus with intersection and union types. Unpublished manuscript, June 1990."},{"key":"34_CR21","unstructured":"B.C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, School of Computer Science, Carnegie Mellon University, Feburary 1991."},{"key":"34_CR22","doi-asserted-by":"crossref","unstructured":"A.M. Pitts. Polymorphism is set theoretic constructively. In D.H. Pitt et al., editors, Category theory and computer science (Lecture Notes in Comuter Science No. 283), pages 12\u201339, Berlin, 1987. Springer-Verlag.","DOI":"10.1007\/3-540-18508-9_18"},{"key":"34_CR23","unstructured":"G. Plotkin. Lectures given at ASL Stanford meeting. Unpublished lecture notes, July 1985."},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\u03c9's programs from proofs in the calculus of construction. In Proceedings of 16th Annual ACM Symposium on Principles of Programming Languages, 1989.","DOI":"10.1145\/75277.75285"},{"key":"34_CR25","unstructured":"J.C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, School of Computer Science, Carnegie Mellon University, June 1988."},{"key":"34_CR26","unstructured":"G. Rosolini. Continuity and effectiveness in topoi. PhD thesis, Department of Computer Science, Carnegie-Mellon University, 1986."},{"key":"34_CR27","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1090\/conm\/092\/1003209","volume-title":"Categories in Computer Science and Logic, (Contemporary Mathematics Vol. 92)","author":"A. Scedrov","year":"1989","unstructured":"A. Scedrov. Normalization revisited. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, (Contemporary Mathematics Vol. 92), pages 357\u2013369, American Mathematical Society, Providence, Rhode Island, 1989."},{"key":"34_CR28","unstructured":"Y. Takayama and S Hayashi. Extended projection method and realizability interpretation. Submitted to Information and Computation, 1990."},{"key":"34_CR29","unstructured":"D. Turner. A new formulation of constructive type theory. In P. Dybjer et al., editors, Proceedings of the Workshop on Programming Logic, pages 258\u2013294, 1989. Report 54, Programming Methodology Group, Department of Computer Science, Chalmers University of Technology and University of G\u00f6teborg."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_71.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:21:33Z","timestamp":1619572893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_71"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_71","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}