Skip to main content
SpringerLink
Log in

A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene

  • Conference paper
  • First Online:
Logic Based Program Synthesis and Transformation (LOPSTR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2664))

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.

This research was partially supported by the project TIC2001-2705-C03-02.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. H. Geuvers, M. Nederhof, Modular proof of Strong Normalization for the Calculus of Constructions, Journal of Functional Programming 1 (1991) 15–189.

    MathSciNet  Google Scholar 

  2. 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.

    Google Scholar 

  3. F. Pfenning, Logical frameworks, in: A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, Vol. II, Elsevier Science, 2001, Ch. 17, pp. 1063–1147.

    Google Scholar 

  4. 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.

    Google Scholar 

  5. G. Gentzen, Untersuchungen über das Logische Schliessen, Math. Zeitschrift 39 (1935) 176–210,405–431, translation in [24].

    Article  MathSciNet  Google Scholar 

  6. F. Barbanera, M. Dezani-Ciancaglini, U. de’Liguoro, Intersection and union types: Syntax and semantics, Information and Computation 119(2) (1995) 202–230.

    Article  MATH  MathSciNet  Google Scholar 

  7. H. P. Barendregt, S. Ghilezan, Lambda terms for natural deduction, secuent calculus and cut elimination, Journal of Functional Programming 10(1) (2000) 121–134.

    Article  MATH  MathSciNet  Google Scholar 

  8. M. Baaz, A. Leitsch, Comparing the complexity of cut-elimination methods, Lecture Notes in Computer Science 2183 (2001) 49–67.

    Article  MathSciNet  Google Scholar 

  9. D. Galmiche, D. J. Pym, Proof-search in type-theoretic languages: an introduction, Theoretical Computer Science 232(1–2) (2000) 5–53.

    Article  MATH  MathSciNet  Google Scholar 

  10. S. C. Kleene, Introduction to Metamathematics, D. van Nostrand, Princeton, New Jersey, 1952.

    MATH  Google Scholar 

  11. D. Pym, A note on the proof theory of the λΠ-calculus, Studia Logica 54 (1995) 199–230.

    Article  MATH  MathSciNet  Google Scholar 

  12. L. van Benthem Jutting, Typing in Pure Type Systems, Information and Computation 105(1) (1993) 30–41.

    Article  MATH  MathSciNet  Google Scholar 

  13. B. C. Ruiz, Sistemas de Tipos Puros con Universos, Ph.D. thesis, Universidad de Málaga (1999).

    Google Scholar 

  14. 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.

    Google Scholar 

  15. J. Gallier, Constructive logics. I. A tutorial on proof systems and typed lambda-calculi, Theoretical Computer Science 110(2) (1993) 249–339.

    Article  MATH  MathSciNet  Google Scholar 

  16. 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

  17. H. Yokouchi, Completeness of type assignment systems with intersection, union, and type quantifiers, Theoretical Computer Science 272 (2002) 341–398.

    Article  MATH  MathSciNet  Google Scholar 

  18. 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).

    Google Scholar 

  19. H. Geuvers, Logics and type systems, Ph.D. thesis, Computer Science Institute, Katholieke Universiteit Nijmegen (1993).

    Google Scholar 

  20. 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.

  21. E. Poll, Expansion Postponement for Normalising Pure Type Systems, Journal of Functional Programming 8(1) (1998) 89–96.

    Article  MATH  MathSciNet  Google Scholar 

  22. 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.

    Google Scholar 

  23. 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.

    Google Scholar 

  24. G. Gentzen, Investigations into logical deductions, in: M. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland, 1969, pp. 68–131.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Lenguajes y Ciencias de la Computación, Universidad de Málaga, Campus Teatinos, 29071, Málaga, Spain

    Francisco Gutiérrez & Blas Ruiz

Authors
  1. Francisco Gutiérrez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Blas Ruiz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Leuschel

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation