A Gentzen-style sequent calculus of constructions with expansion rules
.A Gentzen-style L-formulation of the calculus of constructions is presented and proved equivalent to a natural deduction formulation based on that of Seldin (1997). The L-rules corresponding to the conversion rules of the natural deduction system are expansion rules. Cut elimination follows from the equivalence to the natural deduction formulation and the normalization theorem for the latter. (C) 2000 Elsevier Science B.V. All rights reserved.
calculus of constructions gentzen-style l-formulation typed lambda-calculus