Document

# Curry-Howard for Sequent Calculus at Last!

## File

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

## Cite As

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

## 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.
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.
3. I. Cervesato and F. Pfenning. A linear spine calculus. J. Log. Compt., 13(5):639-688, 2003.
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.
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.
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.
7. Jo. Espírito Santo. The λ-calculus and the unity of structural proof theory. Theory of Computing Systems, 45:963-994, 2009.
8. G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The collected papers of Gerhard Gentzen, pages 68-131. North Holland, 1969.
9. J-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. C.U.P., 1989.
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.
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.
12. E. Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-86, University of Edinburgh, 1988.
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.
14. B. Pierce and D. Turner. Local type inference. In Proc. of POPL'98, pages 252-265. ACM, 1998.
15. D. Prawitz. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.
16. A. Sabry and P. Wadler. A reflection on call-by-value. ACM Transactions on Programming Languages and Systems, 19(6):916-941, 1997.
17. José Espírito Santo. Towards a canonical classical natural deduction system. Ann. Pure Appl. Logic, 164(6):618-650, 2013.
18. M. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
19. Noam Zeilberger. On the unity of duality. Ann. Pure Appl. Logic, 153(1-3):66-96, 2008.