{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:37:54Z","timestamp":1725457074958},"publisher-location":"Berlin\/Heidelberg","reference-count":14,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540579354"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0032391","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:30:32Z","timestamp":1134282632000},"page":"1-9","source":"Crossref","is-referenced-by-count":0,"title":["Lifschitz's logic of calculable numbers and optimizations in program extraction"],"prefix":"10.1007","author":[{"given":"Susumu","family":"Hayashi","sequence":"first","affiliation":[]},{"given":"Yukihide","family":"Takayama","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Constable, R.L. and others: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986"},{"key":"1_CR2","unstructured":"Dowek, C. and others: The Coq Proof Assistant User's Guide, Version 5.6, Technical report, No. 134, INRIA, December, 1991"},{"key":"1_CR3","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1007\/3-540-54415-1_71","volume":"526","author":"S. Hayashi","year":"1991","unstructured":"Hayashi, S.: Singleton, Union and Intersection Types for Program Extraction, Lecture Notes in Computer Science 526 (1991) 701\u2013730","journal-title":"Lecture Notes in Computer Science"},{"key":"1_CR4","unstructured":"Hayashi, S: Logic of refinement types, in Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs, Nijmegen, (1993) 157\u2013172, the formal version of the proceedings is to appear in Springer LNCS."},{"key":"1_CR5","unstructured":"Hayashi, S. and Nakano, H.: PX: A Computational Logic, The MIT Press, 1988"},{"key":"1_CR6","unstructured":"Hayashi, S. and Takayama, Y.: Extended projection method and realizability interpretation, a talk presented at Workshop on Programming Logic, Bastad, Sweden, 1990"},{"key":"1_CR7","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0003-4843(70)90001-X","volume":"1","author":"G. Kreisel","year":"1970","unstructured":"Kreisel, G. and Troelstra, A. S.: Formal Systems for Some Branches of Intuitionistic Analysis, Annals of Math. Logic 1 1970) 229\u2013387","journal-title":"Annals of Math. Logic"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Lifschitz, V.: Calculable Natural Numbers. Intensional Mathematics, S. Shapiro ed. (1985) 173\u2013190, North-Holland","DOI":"10.1016\/S0049-237X(08)70143-5"},{"key":"1_CR9","first-page":"359","volume":"47","author":"V. Lifschitz","year":"1982","unstructured":"Lifschitz, V.: Constructive Assertions in an Extension of Classical Mathematics. J.S.L. 47 (1982) 359\u2013387","journal-title":"J.S.L."},{"key":"1_CR10","first-page":"73","volume-title":"Logicheskii Vyvod","author":"G. E. Mints","year":"1979","unstructured":"Mints, G. E.: Normalization of Natural Deduction and the effectivity of classical existence, in \u201dLogicheskii Vyvod\u201d, Moscow, Nauka (1979) 73\u201377 (in Russian), English translation is in G. E. Mints, Selected Papers in Proof Theory, Biblioplis, Napoli, Italia and North-Holland, Amsterdam, Distributed by North-Holland (1992) 123\u2013146."},{"key":"1_CR11","unstructured":"Mitchell, J. C.: Type systems for programming languages, in Handbook of Theoretical Computer Science, Volume B, J. van Leeuwen ed., (1990) 365\u2013458, North-Holland"},{"key":"1_CR12","unstructured":"Nordstr\u00f6m, B. and Petersson, K. and Smith, J.M.: Programming in Martin-L\u00f6f's type theory, an introduction, Clarendon Press, 1990"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Takayama, Y.: Extended Projection: a new technique to extract efficient programs from constructive proofs, Proceedings of 1989 Conference on Functional Programming Languages and Computer Architecture, ACM Press, 1989","DOI":"10.1145\/99370.99396"},{"key":"1_CR14","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/S0747-7171(08)80139-3","volume":"12","author":"Y. Takayama","year":"1991","unstructured":"Takayama, Y.: Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs, Journal of Symbolic Computation 12 (1991) 29\u201369.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Logic, Language and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0032391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:47:32Z","timestamp":1586612852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0032391"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540579354"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0032391","relation":{},"subject":[]}}