{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T17:31:29Z","timestamp":1777915889055,"version":"3.51.4"},"reference-count":24,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2003,4,1]],"date-time":"2003-04-01T00:00:00Z","timestamp":1049155200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3772,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,4]]},"DOI":"10.1016\/s1571-0661(04)81004-1","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"20-39","source":"Crossref","is-referenced-by-count":3,"special_numbering":"C","title":["A New Machine-checked Proof of Strong Normalisation for Display Logic"],"prefix":"10.1016","volume":"78","author":[{"given":"Jeremy E.","family":"Dawson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB1","first-page":"1","article-title":"A Formalisation of Weak Normalisation (with respect to Permutations) of Sequent Calculus Proofs","volume":"3","author":"Adams","year":"2000","journal-title":"Journal of Computation and Mathematics"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB2","first-page":"13","article-title":"A formalization of the strong normalization proof for System F in LEGO","volume":"664","author":"Altenkirch","year":"1993"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB3","unstructured":"Barras, B and B Werner. Coq in Coq. http:\/\/pauillac.inria.fr\/~barras\/download\/coqincoq.ps.gz"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB4","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1006\/inco.2000.2858","article-title":"Structuring metatheory on inductive definitions","volume":"162","author":"Basin","year":"2000","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB5","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/BF00284976","article-title":"Display logic","volume":"11","author":"Belnap","year":"1982","journal-title":"J. of Philosophical Logic"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB6","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1017\/S0960129599003011","article-title":"On permuting cut with contraction","volume":"10","author":"Borisavljevic","year":"2000","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Dawson, J E and R Gor\u00e9. A mechanised proof system for relation algebra using display logic. In Proc. JELIA98, LNAI 1489:264\u2013278. Springer, 1998.","DOI":"10.1007\/3-540-49545-2_18"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB8","first-page":"89","volume":"42","author":"Dawson","year":"2001"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB9","doi-asserted-by":"crossref","unstructured":"Dawson, J E and R Gor\u00e9. Formalised Cut Admissibility for Display Logic. In Proc. TPHOLS'02 LNCS 2410, 131\u2013147, Springer, 2002.","DOI":"10.1007\/3-540-45685-6_10"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB10","series-title":"Introduction to HOL: a Theorem Proving Environment for Higher Order Logic","author":"Gordon","year":"1993"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB11","doi-asserted-by":"crossref","unstructured":"Gor\u00e9 R. Cur-free display calculi for relation algebras. In Proc. CSL96, LNCS 1258, 198\u2013210, Springer, 1997.","DOI":"10.1007\/3-540-63172-0_40"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB12","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1093\/jigpal\/6.5.669","article-title":"How to display your favourite substructural logic","volume":"6","author":"Gor\u00e9","year":"1998","journal-title":"Logic Journal of the IGPL"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB13","first-page":"451","volume":"6","author":"Gor\u00e9","year":"1998","journal-title":"Substructural logics on display"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB14","unstructured":"Heuerding A. Sequent Calculi for Proof Search in some Madal Logics. PhD thesis, Inst. for Applied Mathematics and Computer Science, Berne, 1998."},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB15","series-title":"What is a logic system?","first-page":"329","article-title":"Theory and its Metatheory in FS0","author":"Matthews","year":"1994"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB16","series-title":"Logical Environments","first-page":"61","article-title":"Experience with FS0 as a framework theory","author":"Matthews","year":"1993"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB17","doi-asserted-by":"crossref","unstructured":"Matthews, S. Implementing FS0 in Isabelle: adding structure at the metalevel. In J Calmet and C Limongelli(Eds), Proc. Disco'96. Springer, 1996.","DOI":"10.1007\/3-540-61697-7_24"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB18","series-title":"TPHOLs98, LNCS 1479","first-page":"295","article-title":"Proving isomorphism of first-order proof systems in HOL","author":"Mikhajlova","year":"1998"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB19","doi-asserted-by":"crossref","unstructured":"Nipkow, T, L C Paulson, and M Wenzel. Isabelle's logics: HOL. Technical report. 15 February 2001, doc\/logics-HOL.dvi in the Isabelle distribution.","DOI":"10.1007\/3-540-45949-9"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB20","unstructured":"Paulson, L C. The Isabelle reference manual. Technical report. 15 February 2001, doc\/ref.dvi in the Isabelle distribution."},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB21","unstructured":"Pfenning, F. Structural cut elimination. In Proc. LICS 94, 1994."},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB22","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1093\/logcom\/4.2.175","article-title":"A Uniform Proof-theoretic Investigation of Linear Logic Programming","volume":"4","author":"Pym","year":"1994","journal-title":"J. of Logic and Computation"},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB23","unstructured":"Sch\u00fcrmann C. Automating the Meta Theory of Deductive Systems. PhD thesis, Dept. of Comp. Sci., Carnegie Mellon University, USA, CMU-CS-00-146, 2000."},{"key":"10.1016\/S1571-0661(04)81004-1_NEWBIB24","series-title":"\u201cDisplaying Modal Logic\u201d volume 3 of Trends in Logic","author":"Wansing","year":"1998"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810041?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104810041?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T03:12:42Z","timestamp":1585883562000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104810041"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,4]]},"references-count":24,"alternative-id":["S1571066104810041"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)81004-1","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,4]]}}}