Document Open Access Logo

Curry-Howard for Sequent Calculus at Last!

Author José Espírito Santo

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.165.pdf
  • Filesize: 464 kB
  • 15 pages

Document Identifiers

Author Details

José Espírito Santo

Cite AsGet BibTex

José Espírito Santo. Curry-Howard for Sequent Calculus at Last!. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 165-179, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TLCA.2015.165

Abstract

This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent calculus, namely the questions: What do variables in proof terms stand for? What is co-control and a co-continuation? How to define the dual of Parigot's mu-operator so that it is a co-control operator? Answering these questions leads to the interpretation that sequent calculus is a formal vector notation with first-class co-control. But this is just the "internal" interpretation, which has to be developed simultaneously with, and is justified by, an equivalent, "external" interpretation, offered by natural deduction: the sequent calculus corresponds to a bi-directional, agnostic (w.r.t. the call strategy), computational lambda-calculus. Next, the formal duality between control and co-control is studied, in the context of classical logic. The duality cannot be observed in the sequent calculus, but rather in a system unifying sequent calculus and natural deduction.
Keywords
  • co-control
  • co-continuation
  • vector notation
  • let-expression
  • formal sub- stitution
  • context substitution
  • computational lambda-calculus
  • classical lo

Metrics

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

References

  1. H. Barendregt and S. Ghilezan. Lambda terms for natural deduction, sequent calculus and cut elimination. Journal of Functional Programming, 10(1):121-134, 2000. Google Scholar
  2. S. Cerrito and D. Kesner. Pattern matching as cut elimination. In Proceedings of 14th annual IEEE Symposium on Logic in Computer Science (LICS'99), pages 98-108, 1999. Google Scholar
  3. I. Cervesato and F. Pfenning. A linear spine calculus. J. Log. Compt., 13(5):639-688, 2003. Google Scholar
  4. P.-L. Curien and H. Herbelin. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, September 18-21, 2000, SIGPLAN Notices 35(9), pages 233-243. ACM, 2000. Google Scholar
  5. R. Dyckhoff and C. Urban. Strong normalisation of Herbelin’s explicit substitution calculus with substitution propagation. Journal of Logic and Computation, 13(5):689-706, 2003. Google Scholar
  6. J. Espírito Santo. Revisiting the correspondence between cut-elimination and normalisation. In Proceedings of ICALP'00, volume 1853 of Lecture Notes in Computer Science, pages 600-611. Springer-Verlag, 2000. Google Scholar
  7. Jo. Espírito Santo. The λ-calculus and the unity of structural proof theory. Theory of Computing Systems, 45:963-994, 2009. Google Scholar
  8. G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The collected papers of Gerhard Gentzen, pages 68-131. North Holland, 1969. Google Scholar
  9. J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. C.U.P., 1989. Google Scholar
  10. H. Herbelin. A λ-calculus structure isomorphic to a Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, Proceedings of CSL'94, volume 933 of Lecture Notes in Computer Science, pages 61-75. Springer-Verlag, 1995. Google Scholar
  11. F. Joachimski and R. Matthes. Short proofs of normalization for the simply-typed lambda-calculus, permutative conversions and Gödel’s T. Arch. for Math. Logic, 42:59-87, 2003. Google Scholar
  12. E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, 1988. Google Scholar
  13. M. Parigot. λμ-calculus: an algorithmic interpretation of classic natural deduction. In Int. Conf. Logic Prog. Automated Reasoning, volume 624 of Lecture Notes in Computer Science, pages 190-201. Springer Verlag, 1992. Google Scholar
  14. B. Pierce and D. Turner. Local type inference. In Proc. of POPL'98, pages 252-265. ACM, 1998. Google Scholar
  15. D. Prawitz. Natural Deduction. Almquist and Wiksell, Stockholm, 1965. Google Scholar
  16. A. Sabry and P. Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916-941, 1997. Google Scholar
  17. José Espírito Santo. Towards a canonical classical natural deduction system. Ann. Pure Appl. Logic, 164(6):618-650, 2013. Google Scholar
  18. M. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006. Google Scholar
  19. Noam Zeilberger. On the unity of duality. Ann. Pure Appl. Logic, 153(1-3):66-96, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact