{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:25Z","timestamp":1725663685126},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569923"},{"type":"electronic","value":"9783540478904"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56992-8_23","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:00:20Z","timestamp":1330257620000},"page":"395-402","source":"Crossref","is-referenced-by-count":0,"title":["Kleene's slash and existence of values of open terms in type theory"],"prefix":"10.1007","author":[{"given":"Jan M.","family":"Smith","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"23_CR1","unstructured":"Peter Aczel. The strength of Martin-L\u00f6f's type theory with one universe. In Proceedings of the Symposium on Mathematical Logic, Oulu, 1974, pages 1\u201332. Report No 2, Department of Philosophy, University of Helsinki, 1977."},{"issue":"1","key":"23_CR2","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R. Burstall","year":"1969","unstructured":"Rod Burstall. Proving Properties of Programs by Structural Induction. Computer Journal, 12(1):41\u201348, 1969.","journal-title":"Computer Journal"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. An algorithm for testing conversion in type theory. In Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.011"},{"key":"23_CR4","unstructured":"Thierry Coquand. Pattern matching with dependent types. In In the informal proceeding from the logical framework workshop at B\u00e5stad, June 1992."},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Lars Halln\u00e4s. Partial Inductive Definitions. Theoretical Computer Science, (87), 1991.","DOI":"10.1016\/S0304-3975(06)80007-1"},{"key":"23_CR6","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"R. Harrop. Concerning formulas of the types A \u2192 B \u2228 C, A \u2192 (\u2203x)B(x) in intuitionistic formal systems. Journal of Symbolic Logic, 25:27\u201332, 1960.","journal-title":"Journal of Symbolic Logic"},{"key":"23_CR7","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/BF01806312","volume":"2","author":"N. D. Jones","year":"1989","unstructured":"N. D. Jones, P. Sestoft, and H. S\u00f8ndergaard. Mix: A self-applicable partial evaluator for experiments in compiler generation. Lisp and Symbolic Computation, (2):9\u201350, 1989.","journal-title":"Lisp and Symbolic Computation"},{"key":"23_CR8","doi-asserted-by":"crossref","first-page":"11","DOI":"10.2307\/2963675","volume":"27","author":"S. C. Kleene","year":"1962","unstructured":"S. C. Kleene. Disjunction and existence under implication in elementary intuitionistic formalisms. Journal of Symbolic Logic, 27:11\u201318, 1962.","journal-title":"Journal of Symbolic Logic"},{"key":"23_CR9","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1002\/malq.19830291004","volume":"29","author":"J. Lambek","year":"1983","unstructured":"J. Lambek and P. J. Scott. New proofs of some intuitionistic principles. Zeit. f Math. Logik und Grundlagen d. Math., 29:493\u2013504, 1983.","journal-title":"Zeit. f Math. Logik und Grundlagen d. Math."},{"key":"23_CR10","unstructured":"Per Martin-L\u00f6f. An Intuitionistic Theory of Types. Technical report, University of Stockholm, 1972."},{"key":"23_CR11","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. Programming in Martin-L\u00f6f 's Type Theory. An Introduction. Oxford University Press, 1990."},{"key":"23_CR12","unstructured":"Christine Paulin-Mohring. Extraction de Programmes dans le Calcul des Constructions. PhD thesis, L'Universite Paris VII, 1989."},{"key":"23_CR13","unstructured":"Jan M. Smith. An interpretation of kleene's slash in type theory. In G. Huet, G. Plotkin, and C. Jones, editors, Informal Proceedings of the Second Workshop on Logical Frameworks, pages 337\u2013342. Esprit Basic Research Action, May 1991. To appear in G. Huet and G. Plotkin, editors, Logical Frameworks, Cambridge University Press."},{"key":"23_CR14","volume-title":"Licentiate Thesis","author":"C. Svensson","year":"1990","unstructured":"Catarina Svensson. A normalization proof for Martin-L\u00f6f's type theory. Licentiate Thesis, Chalmers University of Technology and University of G\u00f6teborg, Sweden, March 1990."},{"issue":"2","key":"23_CR15","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. W. Tait","year":"1967","unstructured":"W. W. Tait. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic, 32(2):198\u2013212, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"23_CR16","unstructured":"Yukihide Takayama. Extracting redundancy-free programs from proofs in first order arithmetic. To appear in Journal of Symbolic Computation."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56992-8_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:55Z","timestamp":1605647275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56992-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569923","9783540478904"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-56992-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}