Abstract
In this paper, a new notion for sequent calculus (à la Gentzen) for Pure Type Systems (PTS) is introduced. This new calculus, \( \mathcal{K} \) , is equivalent to the standard PTS, and it has a cut-free subsystem, \( \mathcal{K}^{{\text{cf}}} \), that will be proved to hold non-trivial properties such as the structural rules of Gentzen/Kleene: thinning, contraction, and interchange.
An interpretation of completeness of the \( \mathcal{K}^{{\text{cf}}} \) system yields the concept of Cut Elimination, (CE), and it is an essential technique in proof theory; thus we think that it will have a deep impact on PTS and in logical frameworks based on PTS.
Keywords
This research was partially supported by the project TIC2001-2705-C03-02.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
H. Geuvers, M. Nederhof, Modular proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming 1 (1991) 15–189.
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–309.
F. Pfenning, Logical frameworks, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science, 2001, Ch. 17, pp. 1063–1147.
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–1238.
G. Gentzen, Untersuchungen über das Logische Schliessen, Math. Zeitschrift 39 (1935) 176–210,405–431, translation in [24].
F. Barbanera, M. Dezani-Ciancaglini, U. de’Liguoro, Intersection and union types: Syntax and semantics, Information and Computation 119(2) (1995) 202–230.
H. P. Barendregt, S. Ghilezan, Lambda terms for natural deduction, secuent calculus and cut elimination, Journal of Functional Programming 10(1) (2000) 121–134.
M. Baaz, A. Leitsch, Comparing the complexity of cut-elimination methods, Lecture Notes in Computer Science 2183 (2001) 49–67.
D. Galmiche, D. J. Pym, Proof-search in type-theoretic languages: an introduction, Theoretical Computer Science 232(1–2) (2000) 5–53.
S. C. Kleene, Introduction to Metamathematics, D. van Nostrand, Princeton, New Jersey, 1952.
D. Pym, A note on the proof theory of the λΠ-calculus, Studia Logica 54 (1995) 199–230.
L. van Benthem Jutting, Typing in Pure Type Systems, Information and Computation 105(1) (1993) 30–41.
B. C. Ruiz, Sistemas de Tipos Puros con Universos, Ph.D. thesis, Universidad de Málaga (1999).
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’98) Proceedings, Vol. 1548 of LNCS, Springer-Verlag, 1999, pp. 422–437.
J. Gallier, Constructive logics. I. A tutorial on proof systems and typed lambda-calculi, Theoretical Computer Science 110(2) (1993) 249–339.
M. Baaz, A. Leitsch, Methods of cut elimination, Tec. rep., 11th European Summer School in Logic, Language and Information. Utrecht University (August 9–20 1999). URL http://www.let.uu.nl/esslli/Courses/baaz-leitsch.html
H. Yokouchi, Completeness of type assignment systems with intersection, union, and type quantifiers, Theoretical Computer Science 272 (2002) 341–398.
F. Gutiérrez, B. C. Ruiz, Sequent Calculi for Pure Type Systems, Tech. Report 06/02, Dept. de Lenguajes y Ciencias de la Computación, Universidad de Málaga (Spain), http://polaris.lcc.uma.es/~blas/publicaciones/ (may 2002).
H. Geuvers, Logics and type systems, Ph.D. thesis, Computer Science Institute, Katholieke Universiteit Nijmegen (1993).
F. Gutiérrez, B. C. Ruiz, Order functional PTS, in: 11th International Workshop on Functional and Logic Programming (WFLP’2002), Vol. 76 of ENTCS, Elsevier, 2002, pp. 1–16, http://www.elsevier.com/gej-ng/31/29/23/126/23/23/76012.pdf.
E. Poll, Expansion Postponement for Normalising Pure Type Systems, Journal of Functional Programming 8(1) (1998) 89–96.
B. C. Ruiz, The Expansion Postponement Problem for Pure Type Systems with Universes, in: 9th International Workshop on Functional and Logic Programming (WFLP’2000), Dpto. de Sistemas Informáticos y Computación, Technical University of Valencia (Tech. Rep.), 2000, pp. 210–224, september 28–30, Benicassim, Spain.
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’01), Évora, Portugal, 2001, pp. 149–163.
G. Gentzen, Investigations into logical deductions, in: M. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 68–131.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gutiérrez, F., Ruiz, B. (2003). A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene. In: Leuschel, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2002. Lecture Notes in Computer Science, vol 2664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45013-0_2
Download citation
DOI: https://doi.org/10.1007/3-540-45013-0_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40438-5
Online ISBN: 978-3-540-45013-9
eBook Packages: Springer Book Archive