{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T19:09:39Z","timestamp":1673723379121},"reference-count":16,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,7,1]],"date-time":"1991-07-01T00:00:00Z","timestamp":678326400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":8052,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1991,7]]},"DOI":"10.1016\/s0747-7171(08)80139-3","type":"journal-article","created":{"date-parts":[[2008,7,22]],"date-time":"2008-07-22T05:12:18Z","timestamp":1216703538000},"page":"29-69","source":"Crossref","is-referenced-by-count":11,"title":["Extraction of redundancy-free programs from constructive natural deduction proofs"],"prefix":"10.1016","volume":"12","author":[{"given":"Yukihide","family":"Takayama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(08)80139-3_bib1","series-title":"Ph.D. Thesis","article-title":"A logicfor correct program development","author":"Bates","year":"1979"},{"key":"10.1016\/S0747-7171(08)80139-3_bib2","series-title":"Foundation of Constructive Mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/S0747-7171(08)80139-3_bib3","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/S0747-7171(08)80139-3_bib4","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/S0747-7171(08)80139-3_bib5","series-title":"Ph.D. Thesis","article-title":"Computational uses of the manipulation of formal proofs","author":"Goad","year":"1980"},{"key":"10.1016\/S0747-7171(08)80139-3_bib6","series-title":"PX: A programming logic","author":"Hayashi","year":"1988"},{"key":"10.1016\/S0747-7171(08)80139-3_bib7","series-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/S0747-7171(08)80139-3_bib8","article-title":"Types and specifications","volume":"83","author":"Nordstr\u00f6m","year":"1983"},{"key":"10.1016\/S0747-7171(08)80139-3_bib9","article-title":"Extracting F\u03c9's programs from proofs in the calculus of constructions","author":"Paulin-Mohring","year":"1989","journal-title":"Conference Record of the 16th Annual ACM Symposium on Principles of Programming Languages"},{"key":"10.1016\/S0747-7171(08)80139-3_bib10","series-title":"Natural Deduction","author":"Prawitz","year":"1965"},{"key":"10.1016\/S0747-7171(08)80139-3_bib11","series-title":"Ph.D. Thesis","article-title":"Extracting efficient code from constructive proofs","author":"Sasaki","year":"1986"},{"key":"10.1016\/S0747-7171(08)80139-3_bib12","series-title":"Typed Logical Calculus. Technical Report 85-13","author":"Sato","year":"1985"},{"key":"10.1016\/S0747-7171(08)80139-3_bib13","article-title":"QJ: A constructive logical system with types","author":"Sato","year":"1986","journal-title":"France-Japan Artificial Intelligence and Computer Science Symposium 86, Tokyo"},{"key":"10.1016\/S0747-7171(08)80139-3_bib14","article-title":"Writing programs as QJ-proofs and compiling into PROLOG programs","author":"Takayama","year":"1987","journal-title":"Proceedings of 4th Symposium on Logic Programming"},{"key":"10.1016\/S0747-7171(08)80139-3_bib15","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-19027-9_4","article-title":"QPC: QJ-based proof compiler\u2014simple examples and analysis","volume":"300","author":"Takayama","year":"1988","journal-title":"Proceedings of 2nd European Symposium on Programming. Lecture Notes in Computer Science"},{"key":"10.1016\/S0747-7171(08)80139-3_bib16","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","article-title":"Mathematical investigations of intuitionistic arithmetic and analysis","volume":"344","author":"Troelstra","year":"1973","journal-title":"Springer Lecture Notes in Mathematics"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717108801393?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717108801393?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,12,26]],"date-time":"2018-12-26T22:52:36Z","timestamp":1545864756000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717108801393"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,7]]},"references-count":16,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,7]]}},"alternative-id":["S0747717108801393"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(08)80139-3","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1991,7]]}}}