{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:12Z","timestamp":1725663612909},"publisher-location":"Berlin, Heidelberg","reference-count":8,"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_41","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:46:46Z","timestamp":1330210006000},"page":"53-87","source":"Crossref","is-referenced-by-count":2,"title":["Adding proof objects and inductive definition mechanisms to frege structures"],"prefix":"10.1007","author":[{"given":"Masahiko","family":"Sato","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Aczel, P., Frege structures and the notions of proposition, truth and set, pp. 31\u201359 in The Kleene Symposium, Barwise, J., Keisler, H.J., Kunen, K. (eds.), North-Holland, 1980.","DOI":"10.1016\/S0049-237X(08)71252-7"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Beeson, M.J., Foundations of Constructive Mathematics, Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Feferman, S., A language and axioms for explicit mathematics, pp. 87\u2013139 in Algebra and Logic, Lect. Notes in Math. 450, Crossley, J.N. (ed.), Springer-Verlag, 1975.","DOI":"10.1007\/BFb0062852"},{"key":"4_CR4","unstructured":"Kobayashi, S., Consistency of Beeson's formal system RPS and some related results, pp. 120\u2013140 in Mathematical Logic and Applications, Lect. Notes in Math. 1388, Shinoda, J., Slaman, T.A. and Tugu\u00e9, T. (eds.), Springer-Verlag, 1987."},{"key":"4_CR5","unstructured":"Martin-L\u00f6f, P., Intuitionistic Type Theory, Bibliopolis, 1984."},{"key":"4_CR6","unstructured":"Sato, M. and Kameyama, Y., Constructive Programming in SST, pp. 23\u201330 in Proceedings of the Japanese-Czechoslovak Seminar on Theoretical Foundations of Knowledge Information Processing (ed. Arikawa, S. and Vlach, M.), Inorga, 1990."},{"key":"4_CR7","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/S0747-7171(89)80045-8","volume":"7","author":"M. Takahashi","year":"1989","unstructured":"Takahashi, M., Parallel Reductions in \u03bb-Calculus, J. Symbolic Computation, 7, pp. 113\u2013123, 1989.","journal-title":"J. Symbolic Computation"},{"key":"4_CR8","unstructured":"Tatsuta, M., Program Synthesis Using Realizability, Theoret. Computer Sci., 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_41.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_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}