{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:14Z","timestamp":1725663614574},"publisher-location":"Berlin, Heidelberg","reference-count":10,"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_40","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:47:03Z","timestamp":1330210023000},"page":"38-52","source":"Crossref","is-referenced-by-count":0,"title":["Monotone recursive definition of predicates and its realizability interpretation"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Tatsuta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"M. Beeson. Foundations of Constructive Mathematics. Springer, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"3_CR2","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"T. Coquand and C. Paulin. Inductively Defined Types. Manuscript, 1989.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"S. Feferman. Constructive theories of functions and classes, In: M. Boffa, D. van Dalen and K. McAloon, editors. Logic Colloquium '78, Proceedings of the Logic Colloquium at Mons, pages 159\u2013224. North-Holland, 1979.","DOI":"10.1016\/S0049-237X(08)71625-2"},{"key":"3_CR5","unstructured":"S. Hayashi and H. Nakano. PX: A Computational Logic. MIT Press, 1988."},{"key":"3_CR6","unstructured":"S. Kobayashi and M. Tatsuta. Realizability Interpretation of Generalized Inductive Definitions. Submitted, 1989."},{"key":"3_CR7","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F w's programs from proofs in the Calculus of Constructions. In 16 th Symp. Principles of Programming Languages, pages 89\u2013104. ACM, 1989.","DOI":"10.1145\/75277.75285"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Paulin-Mohring. Inductively Defined Types in the Calculus of Constructions. Technical Report CMU-CS-89-209, School of Computer Science, Carnegie Melon University, 1989.","DOI":"10.1007\/BFb0040259"},{"key":"3_CR10","unstructured":"M. Tatsuta. Program Synthesis Using Realizability. Theoretical Computer Science, to appear."}],"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_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:54:09Z","timestamp":1605646449000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}