Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts

Authors José Espírito Santo, Maria João Frade, Luís Pinto

Thumbnail PDF


  • Filesize: 0.6 MB
  • 27 pages

Document Identifiers

Author Details

José Espírito Santo
Maria João Frade
Luís Pinto

Cite AsGet BibTex

José Espírito Santo, Maria João Frade, and Luís Pinto. Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 10:1-10:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


This paper gives a comprehensive and coherent view on permutability in the intuitionistic sequent calculus with cuts. Specifically we show that, once permutability is packaged into appropriate global reduction procedures, it organizes the internal structure of the system and determines fragments with computational interest, both for the computation-as-proof-normalization and the computation-as-proof-search paradigms. The vehicle of the study is a lambda-calculus of multiary proof terms with generalized application, previously developed by the authors (the paper argues this system represents the simplest fragment of ordinary sequent calculus that does not fall into mere natural deduction). We start by adapting to our setting the concept of normal proof, developed by Mints, Dyckhoff, and Pinto, and by defining natural proofs, so that a proof is normal iff it is natural and cut-free. Natural proofs form a subsystem with a transparent Curry-Howard interpretation (a kind of formal vector notation for lambda-terms with vectors consisting of lists of lists of arguments), while searching for normal proofs corresponds to a slight relaxation of focusing (in the sense of LJT). Next, we define a process of permutative conversion to natural form, and show that its combination with cut elimination gives a concept of normalization for the sequent calculus. We derive a systematic picture of the full system comprehending a rich set of reduction procedures (cut elimination, flattening, permutative conversion, normalization, focalization), organizing the relevant subsystems and the important subclasses of cut-free, normal, and focused proofs.
  • sequent calculus
  • permutative conversion
  • Curry-Howard isomorphism
  • vector of arguments
  • generalized application
  • normal proof
  • natural proof
  • cut eli


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. T. Brock-Nannestad, N. Guenot, and D. Gustafsson. Computation in focused intuitionistic logic. In Proc. of PPDP'15, pages 43-54. ACM, 2015. Google Scholar
  2. I. Cervesato and F. Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639-688, 2003. Google Scholar
  3. P.-L. Curien and H. Herbelin. The duality of computation. In Proc. of ICFP'00, pages 233-243. IEEE, 2000. Google Scholar
  4. R. Dyckhoff and L. Pinto. Permutability of proofs in intuitionistic sequent calculi. Theoretical Computer Science, 212:141-155, 1999. Google Scholar
  5. J. Espírito Santo. Curry-Howard for sequent calculus at last! In Proc. of TLCA'15, volume 38 of LIPIcs, pages 165-179. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  6. J. Espírito Santo, M. J. Frade, and L. Pinto. Structural proof theory as rewriting. In Proc. of RTA'06, volume 4098 of Lecture Notes in Computer Science, pages 197-211. Springer, 2006. Google Scholar
  7. J. Espírito Santo, R. Matthes, and L. Pinto. Continuation-passing style and strong normalisation for intuitionistic sequent calculi. Logical Methods in Computer Science, 5(2), 2009. Google Scholar
  8. J. Espírito Santo and L. Pinto. Confluence and strong normalisation of the generalised multiary λ-calculus. In Revised selected papers from TYPES'03, volume 3085 of Lecture Notes in Computer Science, pages 286-300. Springer, 2004. Google Scholar
  9. J. Espírito Santo and L. Pinto. A calculus of multiary sequent terms. ACM Trans. Comput. Log., 12(3):22, 2011. Google Scholar
  10. J-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  11. J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Univ. Press, 1989. Google Scholar
  12. H. Herbelin. A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In Proc. of CSL'94, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer, 1995. Google Scholar
  13. F. Joachimski and R. Matthes. Standardization and confluence for a lambda calculus with generalized applications. In Proc. of RTA'00, volume 1833 of Lecture Notes in Computer Science, pages 141-155. Springer, 2000. Google Scholar
  14. S. Kleene. Permutability of inferences in gentzen’s calculi LK and LJ. Memoirs of the American Mathematical Society, 10:1-26, 1952. Google Scholar
  15. C. Liang and D. Miller. Focusing and polarization in linear, intuitionistic, and classical logic. Theoretical Computer Science, 410:4747-4768, 2009. Google Scholar
  16. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1-2):125-157, 1991. Google Scholar
  17. G. Mints. Normal forms for sequent derivations. In P. Odifreddi, editor, Kreiseliana, pages 469-492. A. K. Peters, Wellesley, Massachusetts, 1996. Google Scholar
  18. S. Negri and J. von Plato. Structural proof theory. Cambridge University Press, 2001. Google Scholar
  19. D. Prawitz. Natural Deduction. A Proof-Theoretical Study. Almquist and Wiksell, 1965. Google Scholar
  20. H. Schwichtenberg. Termination of permutative conversions in intuitionistic gentzen calculi. Theoretical Computer Science, 212(1-2):247-260, 1999. Google Scholar
  21. R. J. Simmons. Structural focalization. ACM Transactions on Computational Logic, 15(3):21:1-21:33, 2014. Google Scholar
  22. A. Troelstra and H. Schwitchtenberg. Basic Proof Theory. Cambridge Univ. Press, 2000. Google Scholar
  23. J. von Plato. Natural deduction with general elimination rules. Annals of Mathematical Logic, 40(7):541-567, 2001. Google Scholar
  24. N. Zeilberger. On the unity of duality. Annals of Pure and Appllied Logic, 153(1-3):66-96, 2008. Google Scholar
  25. J. Zucker. The correspondence between cut-elimination and normalization. Annals of Mathematical Logic, 7:1-112, 1974. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail