{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T23:56:54Z","timestamp":1676678214870},"reference-count":0,"publisher":"World Scientific Pub Co Pte Lt","issue":"01","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[1994,3]]},"abstract":"<jats:p> Realizability of monotone inductive definitions is studied to construct a logical system in which recursive data structures and recursive control structures of programs are naturally formalized by using inductive definitions and programs can be produced from constructive proofs by using realizability. Two q-realizability interpretations of monotone inductive definitions are presented. One interpretation is defined so that a realizer of an inductively defined predicate is the same as a realizer of its expansion. It is proved that the interpretation of restricted monotone inductive definitions is sound and that the interpretation of full monotone inductive definitions is not sound, though the interpretation seems very natural. Another interpretation is presented by using the higher order coding and q-realizability for the second order logic. The soundness of this interpretation of full monotone inductive definitions is also proved. To prove this result, greatest-lower-bound inductive definitions are introduced. <\/jats:p>","DOI":"10.1142\/s0129054194000025","type":"journal-article","created":{"date-parts":[[2004,11,18]],"date-time":"2004-11-18T21:21:13Z","timestamp":1100812873000},"page":"1-21","source":"Crossref","is-referenced-by-count":3,"title":["TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS"],"prefix":"10.1142","volume":"05","author":[{"given":"MAKOTO","family":"TATSUTA","sequence":"first","affiliation":[{"name":"Research Institute of Electrical Communication,  Tohoku University, Sendai 980, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0129054194000025","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T20:54:37Z","timestamp":1565124877000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0129054194000025"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,3]]},"references-count":0,"journal-issue":{"issue":"01","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[1994,3]]}},"alternative-id":["10.1142\/S0129054194000025"],"URL":"https:\/\/doi.org\/10.1142\/s0129054194000025","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,3]]}}}