{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:02:58Z","timestamp":1725487378647},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540404385"},{"type":"electronic","value":"9783540450139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-45013-0_2","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:06:29Z","timestamp":1184601989000},"page":"17-31","source":"Crossref","is-referenced-by-count":2,"title":["A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen\/Kleene"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Blas","family":"Ruiz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,6,24]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers, M. Nederhof, Modular proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming 1 (1991) 15\u2013189.","journal-title":"Journal of Functional Programming"},{"key":"2_CR2","unstructured":"H. P. Barendregt, Lambda Calculi with Types, in: S. Abramsky, D. Gabbay, T. S. Maibaum (Eds.), Handbook of Logic in Computer Science, Oxford University Press, 1992, Ch. 2.2, pp. 117\u2013309."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"F. Pfenning, Logical frameworks, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science, 2001, Ch. 17, pp. 1063\u20131147.","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"H. Barendregt, H. Geuvers, Proof-assistants using dependent type systems, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science, 2001, Ch. 18, pp. 1149\u20131238.","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen, Untersuchungen \u00fcber das Logische Schliessen, Math. Zeitschrift 39 (1935) 176\u2013210,405\u2013431, translation in [24].","journal-title":"Math. Zeitschrift"},{"issue":"2","key":"2_CR6","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1006\/inco.1995.1086","volume":"119","author":"F. Barbanera","year":"1995","unstructured":"F. Barbanera, M. Dezani-Ciancaglini, U. de\u2019Liguoro, Intersection and union types: Syntax and semantics, Information and Computation 119(2) (1995) 202\u2013230.","journal-title":"Information and Computation"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1017\/S0956796899003524","volume":"10","author":"H. P. Barendregt","year":"2000","unstructured":"H. P. Barendregt, S. Ghilezan, Lambda terms for natural deduction, secuent calculus and cut elimination, Journal of Functional Programming 10(1) (2000) 121\u2013134.","journal-title":"Journal of Functional Programming"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45504-3_4","volume":"2183","author":"M. Baaz","year":"2001","unstructured":"M. Baaz, A. Leitsch, Comparing the complexity of cut-elimination methods, Lecture Notes in Computer Science 2183 (2001) 49\u201367.","journal-title":"Lecture Notes in Computer Science"},{"issue":"1\u20132","key":"2_CR9","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0304-3975(99)00169-3","volume":"232","author":"D. Galmiche","year":"2000","unstructured":"D. Galmiche, D. J. Pym, Proof-search in type-theoretic languages: an introduction, Theoretical Computer Science 232(1\u20132) (2000) 5\u201353.","journal-title":"Theoretical Computer Science"},{"key":"2_CR10","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"S. C. Kleene, Introduction to Metamathematics, D. van Nostrand, Princeton, New Jersey, 1952."},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/BF01063152","volume":"54","author":"D. Pym","year":"1995","unstructured":"D. Pym, A note on the proof theory of the \u03bb\u03a0-calculus, Studia Logica 54 (1995) 199\u2013230.","journal-title":"Studia Logica"},{"issue":"1","key":"2_CR12","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L.V. Jutting van","year":"1993","unstructured":"L. van Benthem Jutting, Typing in Pure Type Systems, Information and Computation 105(1) (1993) 30\u201341.","journal-title":"Information and Computation"},{"key":"2_CR13","unstructured":"B. C. Ruiz, Sistemas de Tipos Puros con Universos, Ph.D. thesis, Universidad de M\u00e1laga (1999)."},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","first-page":"422","volume-title":"7th International Conference on Algebraic Methodology and Software Technology (AMAST\u201998) Proceedings","author":"B. C. Ruiz","year":"1999","unstructured":"B. C. Ruiz, Condensing lemmas in Pure Type Systems with Universes, in: A. M. Haeberer (Ed.), 7th International Conference on Algebraic Methodology and Software Technology (AMAST\u201998) Proceedings, Vol. 1548 of LNCS, Springer-Verlag, 1999, pp. 422\u2013437."},{"issue":"2","key":"2_CR15","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, Constructive logics. I. A tutorial on proof systems and typed lambda-calculi, Theoretical Computer Science 110(2) (1993) 249\u2013339.","journal-title":"Theoretical Computer Science"},{"key":"2_CR16","unstructured":"M. Baaz, A. Leitsch, Methods of cut elimination, Tec. rep., 11th European Summer School in Logic, Language and Information. Utrecht University (August 9\u201320 1999). URL http:\/\/www.let.uu.nl\/esslli\/Courses\/baaz-leitsch.html"},{"key":"2_CR17","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/S0304-3975(00)00356-X","volume":"272","author":"H. Yokouchi","year":"2002","unstructured":"H. Yokouchi, Completeness of type assignment systems with intersection, union, and type quantifiers, Theoretical Computer Science 272 (2002) 341\u2013398.","journal-title":"Theoretical Computer Science"},{"key":"2_CR18","series-title":"Tech. Report","volume-title":"Sequent Calculi for Pure Type Systems","author":"F. Guti\u00e9rrez","year":"2002","unstructured":"F. Guti\u00e9rrez, B. C. Ruiz, Sequent Calculi for Pure Type Systems, Tech. Report 06\/02, Dept. de Lenguajes y Ciencias de la Computaci\u00f3n, Universidad de M\u00e1laga (Spain), http:\/\/polaris.lcc.uma.es\/~blas\/publicaciones\/ (may 2002)."},{"key":"2_CR19","unstructured":"H. Geuvers, Logics and type systems, Ph.D. thesis, Computer Science Institute, Katholieke Universiteit Nijmegen (1993)."},{"key":"2_CR20","unstructured":"F. Guti\u00e9rrez, B. C. Ruiz, Order functional PTS, in: 11th International Workshop on Functional and Logic Programming (WFLP\u20192002), Vol. 76 of ENTCS, Elsevier, 2002, pp. 1\u201316, http:\/\/www.elsevier.com\/gej-ng\/31\/29\/23\/126\/23\/23\/76012.pdf ."},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1017\/S095679689700292X","volume":"8","author":"E. Poll","year":"1998","unstructured":"E. Poll, Expansion Postponement for Normalising Pure Type Systems, Journal of Functional Programming 8(1) (1998) 89\u201396.","journal-title":"Journal of Functional Programming"},{"key":"2_CR22","unstructured":"B. C. Ruiz, The Expansion Postponement Problem for Pure Type Systems with Universes, in: 9th International Workshop on Functional and Logic Programming (WFLP\u20192000), Dpto. de Sistemas Inform\u00e1ticos y Computaci\u00f3n, Technical University of Valencia (Tech. Rep.), 2000, pp. 210\u2013224, september 28\u201330, Benicassim, Spain."},{"key":"2_CR23","unstructured":"G. Barthe, B. Ruiz, Tipos Principales y Cierre Semi-completo para Sistemas de Tipos Puros Extendidos, in: 2001 Joint Conference on Declarative Programming (APPIA-GULP-PRODE\u201901), \u00c9vora, Portugal, 2001, pp. 149\u2013163."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"G. Gentzen, Investigations into logical deductions, in: M. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 68\u2013131.","DOI":"10.1016\/S0049-237X(08)70822-X"}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45013-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,25]],"date-time":"2020-04-25T01:40:26Z","timestamp":1587778826000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45013-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540404385","9783540450139"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45013-0_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}