https://hal.inria.fr/inria-00381525Herbelin, HugoHugoHerbelinLITP - Laboratoire Informatique Théorique et Programmation - UPMC - Université Pierre et Marie Curie - Paris 6 - UPD7 - Université Paris Diderot - Paris 7 - CNRS - Centre National de la Recherche ScientifiqueCOQ - Formal Specifications and Program Validation - Inria Paris-Rocquencourt - Inria - Institut National de Recherche en Informatique et en AutomatiqueA Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus StructureHAL CCSD1994sequent calculuslambda-calculusCurry-Howard[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]Herbelin, HugoLeszek Pacholski and Jerzy Tiuryn2009-05-05 16:39:362022-02-04 03:13:542009-05-06 08:23:50enConference papersapplication/pdf1We consider a lambda-calculus for which applicative terms have no longer the form (...((u u_1) u_2) ... u_n) but the form (u [u_1 ; ... ; u_n]), for which [u_1 ; ... ; u_n] is a list of terms. While the structure of the usual lambda-calculus is isomorphic to the structure of natural deduction, this new structure is isomorphic to the structure of Gentzen-style sequent calculus. To express the basis of the isomorphism, we consider intuitionistic logic with the implication as sole connective. However we do not consider Gentzen's calculus LJ, but a calculus LJT which leads to restrict the notion of cut-free proofs in LJ. We need also to explicitly consider, in a simply typed version of this lambda-calculus, a substitution operator and a list concatenation operator. By this way, each elementary step of cut-elimination exactly matches with a beta-reduction, a substitution propagation step or a concatenation computation step. Though it is possible to extend the isomorphism to classical logic and to other connectives, we do not treat of it in this paper.