乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T21:11:44Z","timestamp":1648933904624},"reference-count":37,"publisher":"Elsevier BV","issue":"6","license":[{"start":{"date-parts":[[2013,6,1]],"date-time":"2013-06-01T00:00:00Z","timestamp":1370044800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2017,6,1]],"date-time":"2017-06-01T00:00:00Z","timestamp":1496275200000},"content-version":"vor","delay-in-days":1461,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1016\/j.apal.2012.05.005","type":"journal-article","created":{"date-parts":[[2012,5,24]],"date-time":"2012-05-24T18:10:38Z","timestamp":1337883038000},"page":"676-701","source":"Crossref","is-referenced-by-count":2,"title":["The\u03bb<\/mml:mi>\u03bc<\/mml:mi><\/mml:mrow>T<\/mml:mi><\/mml:mrow><\/mml:msup><\/mml:math>-calculus"],"prefix":"10.1016","volume":"164","author":[{"given":"Herman","family":"Geuvers","sequence":"first","affiliation":[]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.apal.2012.05.005_br0010","unstructured":"Peter Aczel, A general Church\u2013Rosser theorem, Technical report, University of Manchester, 1978."},{"key":"10.1016\/j.apal.2012.05.005_br0020","series-title":"ICALP","first-page":"871","article-title":"Minimal classical logic and control operators","volume":"vol. 2719","author":"Ariola","year":"2003"},{"key":"10.1016\/j.apal.2012.05.005_br0030","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/S1571-0661(04)80878-8","article-title":"Parallel reduction in type free \u03bb\u03bc-calculus","volume":"42","author":"Baba","year":"2001","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"2","key":"10.1016\/j.apal.2012.05.005_br0040","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0025","article-title":"A symmetric lambda calculus for classical program extraction","volume":"125","author":"Barbanera","year":"1996","journal-title":"Inform. and Comput."},{"key":"10.1016\/j.apal.2012.05.005_br0050","series-title":"PEPM","first-page":"131","article-title":"CPS translating inductive and coinductive types","author":"Barthe","year":"2002"},{"key":"10.1016\/j.apal.2012.05.005_br0060","series-title":"Annals of Pure and Applied Logic","first-page":"77","article-title":"Refined program extraction from classical proofs","author":"Berger","year":"2000"},{"key":"10.1016\/j.apal.2012.05.005_br0070","series-title":"Proof and Computation, NATO Advanced Study Institute, International Summer School Held in Marktoberdorf, Germany, 1993","first-page":"1","article-title":"Program development by proof transformation","volume":"vol. 139","author":"Berger","year":"1995"},{"issue":"1\u20132","key":"10.1016\/j.apal.2012.05.005_br0080","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/S0304-3975(99)00170-X","article-title":"Search algorithms in type theory","volume":"232","author":"Caldwell","year":"2000","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"10.1016\/j.apal.2012.05.005_br0090","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/S0304-3975(98)00011-5","article-title":"System T, call-by-value and the minimum problem","volume":"206","author":"Colson","year":"1998","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.apal.2012.05.005_br0100","series-title":"Semantics and Logics of Computation","first-page":"470","article-title":"Computational content of classical logic","author":"Coquand","year":"1996"},{"issue":"6","key":"10.1016\/j.apal.2012.05.005_br0110","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1017\/S0956796899003512","article-title":"A confluent lambda-calculus with a catch\/throw mechanism","volume":"9","author":"Crolard","year":"1999","journal-title":"J. Funct. Programming"},{"key":"10.1016\/j.apal.2012.05.005_br0120","unstructured":"Tristan Crolard, Emmanuel Polonowski, A program logic for higher-order procedural variables and non-local jumps, Technical report TR-LACL-2011-4, http:\/\/arxiv.org\/abs\/1112.1554, 2011."},{"key":"10.1016\/j.apal.2012.05.005_br0130","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/j.entcs.2005.06.020","article-title":"Why the usual candidates of reducibility do not work for the symmetric \u03bb\u03bc-calculus","volume":"140","author":"Ren\u00e9","year":"2005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.apal.2012.05.005_br0140","series-title":"CAAP","first-page":"85","article-title":"A CPS-translation of the \u03bb\u03bc-calculus","volume":"vol. 787","author":"de Groote","year":"1994"},{"issue":"2","key":"10.1016\/j.apal.2012.05.005_br0150","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(92)90014-7","article-title":"The revised report on the syntactic theories of sequential control and state","volume":"103","author":"Felleisen","year":"1992","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.apal.2012.05.005_br0160","series-title":"ASIAN","first-page":"321","article-title":"Calculus of classical proofs I","volume":"vol. 1345","author":"Fujita","year":"1997"},{"key":"10.1016\/j.apal.2012.05.005_br0170","series-title":"TLCA","first-page":"162","article-title":"Explicitly typed \u03bb\u03bc-calculus for polymorphism and call-by-value","volume":"vol. 1581","author":"Fujita","year":"1999"},{"key":"10.1016\/j.apal.2012.05.005_br0180","series-title":"LerNet ALFA Summer School","first-page":"1","article-title":"Introduction to type theory","volume":"vol. 5520","author":"Geuvers","year":"2008"},{"key":"10.1016\/j.apal.2012.05.005_br0190","series-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/j.apal.2012.05.005_br0200","series-title":"POPL","first-page":"47","article-title":"A formulae-as-types notion of control","author":"Griffin","year":"1990"},{"key":"10.1016\/j.apal.2012.05.005_br0210","series-title":"LICS","first-page":"50","article-title":"An intuitionistic logic that proves Markov\u02bcs principle","author":"Herbelin","year":"2010"},{"issue":"4","key":"10.1016\/j.apal.2012.05.005_br0220","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.ipl.2006.03.009","article-title":"Strong normalization proofs by CPS-translations","volume":"99","author":"Ikeda","year":"2006","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/j.apal.2012.05.005_br0230","doi-asserted-by":"crossref","unstructured":"Yevgeni Makarov, Practical program extraction from classical proofs, in: MFPS, in: Electron. Notes Theor. Comput. Sci., vol. 155 2006, pp. 521\u2013542.","DOI":"10.1016\/j.entcs.2005.11.071"},{"key":"10.1016\/j.apal.2012.05.005_br0240","unstructured":"Chetan Murthy, Extracting constructive content from classical proofs, PhD thesis, Cornell University, 1990."},{"issue":"1","key":"10.1016\/j.apal.2012.05.005_br0250","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1016\/S0304-3975(01)00380-2","article-title":"Confluency and strong normalizability of call-by-value \u03bb\u03bc-calculus","volume":"290","author":"Nakazawa","year":"2003","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.apal.2012.05.005_br0260","unstructured":"C.-H. Luke Ong, Charles A. Stewart, A Curry\u2013Howard foundation for functional computation with control, in: POPL, 1997, pp. 215\u2013227."},{"key":"10.1016\/j.apal.2012.05.005_br0270","series-title":"LPAR","first-page":"190","article-title":"\u03bb\u03bc-Calculus: An algorithmic interpretation of classical natural deduction","volume":"vol. 624","author":"Parigot","year":"1992"},{"key":"10.1016\/j.apal.2012.05.005_br0280","series-title":"Kurt G\u00f6del Colloquium","first-page":"263","article-title":"Classical proofs as programs","volume":"vol. 713","author":"Parigot","year":"1993"},{"issue":"4","key":"10.1016\/j.apal.2012.05.005_br0290","doi-asserted-by":"crossref","first-page":"1461","DOI":"10.2307\/2275652","article-title":"Proofs of strong normalisation for second order classical natural deduction","volume":"62","author":"Parigot","year":"1997","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/j.apal.2012.05.005_br0300","series-title":"POPL","article-title":"Extracting F\u03c9\u02bcs programs from proofs in the calculus of constructions","author":"Paulin-Mohring","year":"1989"},{"key":"10.1016\/j.apal.2012.05.005_br0310","unstructured":"Walter Py, Confluence en \u03bb\u03bc-calcul, PhD thesis, Universit\u00e9 de Savoie, 1998 (in French)."},{"key":"10.1016\/j.apal.2012.05.005_br0320","series-title":"TACS","first-page":"516","article-title":"The \u03bb\u0394-calculus","volume":"vol. 789","author":"Rehof","year":"1994"},{"key":"10.1016\/j.apal.2012.05.005_br0330","article-title":"Lectures on the Curry\u2013Howard Isomorphism","volume":"vol. 149","author":"S\u00f8rensen","year":"2006"},{"key":"10.1016\/j.apal.2012.05.005_br0340","series-title":"Combinators, \u03bb-Terms and Proof Theory","author":"Stenlund","year":"1972"},{"issue":"2","key":"10.1016\/j.apal.2012.05.005_br0350","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretations of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symbolic Logic"},{"issue":"1","key":"10.1016\/j.apal.2012.05.005_br0360","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","article-title":"Parallel reductions in \u03bb-calculus","volume":"118","author":"Takahashi","year":"1995","journal-title":"Inform. and Comput."},{"key":"10.1016\/j.apal.2012.05.005_br0370","series-title":"ICTCS","first-page":"81","article-title":"The language \u03c7: Circuits, computations and classical logic","volume":"vol. 3701","author":"van Bakel","year":"2005"}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007212000814?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007212000814?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,11,23]],"date-time":"2018-11-23T06:25:37Z","timestamp":1542954337000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007212000814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6]]},"references-count":37,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["S0168007212000814"],"URL":"https:\/\/doi.org\/10.1016\/j.apal.2012.05.005","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2013,6]]}}}