{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:57:25Z","timestamp":1773097045516,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600176","type":"print"},{"value":"9783540494041","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022247","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:12:29Z","timestamp":1132639949000},"page":"61-75","source":"Crossref","is-referenced-by-count":67,"title":["A \u03bb-calculus structure isomorphic to Gentzen-style sequent calculus structure"],"prefix":"10.1007","author":[{"given":"Hugo","family":"Herbelin","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"V. Breazu Tanen, D. Kesner, L. Puel: \u201cA typed pattern calculus\u201d, IEEE Symposium on Logic in Computer Science, Montr\u00e9al, Canada, June 1993, pp 262\u2013274.","DOI":"10.1109\/LICS.1993.287581"},{"key":"5_CR2","unstructured":"V. Danos, J-B. Joinet, H. Schellinx: \u201cLKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication\u201d, in Proceedings of the Workshop on Linear Logic, Cornell, edited by J-Y. Girard, Y. Lafont, L. R\u00e9gnier, 1993."},{"key":"5_CR3","volume-title":"Translations of mathematical monographs, Vol 67","author":"A. G. Dragalin","year":"1988","unstructured":"A. G. Dragalin: Mathematical Intuitionism: Introduction to Proof Theory, Translations of mathematical monographs, Vol 67, Providence, R.I.: American Mathematical Society, 1988."},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0304-3975(93)90011-H","volume":"110","author":"J. Gallier","year":"1993","unstructured":"J. Gallier: \u201cConstructive logics, part I: A tutorial on proof systems and typed \u03bb-calculi\u201d, Theoretical Computer Science, Vol 110, 1993, pp 249\u2013339.","journal-title":"Theoretical Computer Science"},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1017\/S0960129500001328","volume":"1","author":"J.-Y. Girard","year":"1991","unstructured":"J.-Y. Girard: \u201cA new constructive logic: classical logic\u201d, Mathematical Structures in Computer Science, Vol 1, 1991, pp 255\u2013296.","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J-Y. Girard","year":"1993","unstructured":"J-Y. Girard: \u201cOn the Unity of Logic\u201d, Annals of Pure and Applied Logic, Vol 59, 1993, pp 201\u2013217.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"G. Huet: \u201cConfluent Reductions: Abstract Properties and Applications to Term Rewriting Systems\u201d, Journal of the Association for Computing Machinery, Vol 27, 1980, pp 797\u2013821.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Z. Benaissa, D. Briaud, P. Lescanne, J. Rouyer-Degli, \u201c\u03bb\u03bd, a calculus of explicit substitutions which preserves strong normalisation\u201d, submitted to Journal of Functional Programming, 1995.","DOI":"10.1017\/S0956796800001945"},{"key":"5_CR9","unstructured":"G. Mints: \u201cNormal forms for sequent derivations\u201d, Private communication, 1994."},{"key":"5_CR10","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0003-4843(77)80004-1","volume":"12","author":"G. Pottinger","year":"1977","unstructured":"G. Pottinger: \u201cNormalization as a homomorphic image of cut-elimination\u201d, Annals of mathematical logic), Vol 12, 1977, pp 323\u2013357.","journal-title":"Annals of mathematical logic)"},{"key":"5_CR11","first-page":"90","volume-title":"Natural Deduction, a Proof-sTheoretical Study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz: Natural Deduction, a Proof-sTheoretical Study, Almquist and Wiksell, Stockholm, 1965, pp 90\u201391"},{"key":"5_CR12","unstructured":"W. A. Howard, \u201cThe Formulae-as-Types Notion of Constructions\u201d, in J.P. Seldin and J.R. Hindley Eds, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980 (unpublished manuscript of 1969)."},{"key":"5_CR13","unstructured":"P. Wadler: \u201cA Curry-Howard isomorphism for sequent calculus\u201d, Private communication, 1993."},{"key":"5_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. I. Zucker","year":"1974","unstructured":"J. I. Zucker: \u201cCorrespondence between cut-elimination and normalization, part I and II\u201d, Annals of mathematical logic, Vol 7, 1974, pp 1\u2013156.","journal-title":"Annals of mathematical logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:43:19Z","timestamp":1586572999000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022247"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/bfb0022247","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}