{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T06:26:26Z","timestamp":1649053586230},"reference-count":22,"publisher":"Elsevier BV","issue":"5-6","license":[{"start":{"date-parts":[[1993,5,1]],"date-time":"1993-05-01T00:00:00Z","timestamp":736214400000},"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":7382,"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":[[1993,5]]},"DOI":"10.1016\/s0747-7171(06)80008-8","type":"journal-article","created":{"date-parts":[[2007,4,25]],"date-time":"2007-04-25T14:20:47Z","timestamp":1177510847000},"page":"641-672","source":"Crossref","is-referenced-by-count":1,"title":["QPC2: A constructive calculus with parameterized specifications"],"prefix":"10.1016","volume":"15","author":[{"given":"Yukihide","family":"Takayama","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(06)80008-8_bib1","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"issue":"2\/3","key":"10.1016\/S0747-7171(06)80008-8_bib2","article-title":"The Calculus of Constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/S0747-7171(06)80008-8_bib3","article-title":"The Calculus of Constructions, Documentation and users's guide Version 4.10","author":"Project FORMEL","year":"1989"},{"key":"10.1016\/S0747-7171(06)80008-8_bib4","article-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'order sup\u00e9rieur","volume":"7","author":"Girard","year":"1972","journal-title":"Th\u00e8se d'\u00e9tat. Universit\u00e9 Paris"},{"key":"10.1016\/S0747-7171(06)80008-8_bib5","doi-asserted-by":"crossref","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variable types, fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S0747-7171(06)80008-8_bib6","article-title":"Computational Uses of the Manipulation of Formal Proofs","author":"Goad","year":"1980","journal-title":"PhD thesis, Stanford University"},{"key":"10.1016\/S0747-7171(06)80008-8_bib7","series-title":"Proceedings of First International Conference on Theoretical Aspects of Computer Software, LNCS 526","article-title":"Singleton, Union and Intersection Types for Program Extraction","author":"Hayashi","year":"1991"},{"key":"10.1016\/S0747-7171(06)80008-8_bib8","series-title":"PX : A Computational Logic","author":"Hayashi","year":"1989"},{"key":"10.1016\/S0747-7171(06)80008-8_bib9","doi-asserted-by":"crossref","DOI":"10.1016\/0003-4843(70)90001-X","article-title":"Formal systems for some branches of intuitionistic analysis","volume":"1","author":"Kreisel","year":"1970","journal-title":"Annals of Mathematical Logic"},{"key":"10.1016\/S0747-7171(06)80008-8_bib10","series-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/S0747-7171(06)80008-8_bib11","series-title":"Proceedings of Symposium on Logic in Conputer Science","article-title":"Algorithm Development in the Calculus of Constructions","author":"Mohring","year":"1986"},{"key":"10.1016\/S0747-7171(06)80008-8_bib12","series-title":"Proceedings of 1981 Conference on Functional Programming Language and Computer Architecture","article-title":"Programming in constructive set theory: some examples","author":"Nordstr\u00f6m","year":"1981"},{"key":"10.1016\/S0747-7171(06)80008-8_bib13","article-title":"Programming in Martin-L\u00f6f's Type Theory, An Introduction","volume":"7","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/S0747-7171(06)80008-8_bib14","series-title":"16th Annual ACM Symposium on Principles of Programming Languages","article-title":"Extracting F\u03c9's Programs from Proofs in the Calculus of Constructions","author":"Paulin-Mohring","year":"1989"},{"key":"10.1016\/S0747-7171(06)80008-8_bib15","series-title":"Natural Deduction","author":"Prawitz","year":"1965"},{"key":"10.1016\/S0747-7171(06)80008-8_bib16","series-title":"Proceedings of the Japanese-Czechoslovak Seminar on Theoretical Foundations of Knowledge Information Processing","article-title":"Constructive Programming in SST","author":"Sato","year":"1990"},{"key":"10.1016\/S0747-7171(06)80008-8_bib17","series-title":"European Symposium on Programming '88, LNCS 300","article-title":"QPC: QJ-Based Proof Compiler \u2014 Simple Examples and Analysis","author":"Takayama","year":"1988"},{"key":"10.1016\/S0747-7171(06)80008-8_bib18","series-title":"Proceedings of 1989 Conference on Functional Programming Languages and Computer Architecture","article-title":"Extended Projection - a new method to extract efficient programs from constructive proofs","author":"Takayama","year":"1989"},{"issue":"1","key":"10.1016\/S0747-7171(06)80008-8_bib19","doi-asserted-by":"crossref","DOI":"10.1016\/S0747-7171(08)80139-3","article-title":"Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs","volume":"12","author":"Takayama","year":"1991","journal-title":"Journal of Symbolic Computation"},{"issue":"4","key":"10.1016\/S0747-7171(06)80008-8_bib20","article-title":"SHUTEN: A Constructive Programming System","volume":"7","author":"Takayama","year":"1992","journal-title":"Journal of Japanese Society for Artificial Intelligence"},{"key":"10.1016\/S0747-7171(06)80008-8_bib21","article-title":"Program Synthesis Using Realizability","volume":"90","author":"Tatsuta","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S0747-7171(06)80008-8_bib22","series-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","volume":"344","year":"1973"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717106800088?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717106800088?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,7]],"date-time":"2019-01-07T19:53:16Z","timestamp":1546890796000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717106800088"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,5]]},"references-count":22,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[1993,5]]}},"alternative-id":["S0747717106800088"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(06)80008-8","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[1993,5]]}}}