Document Open Access Logo

Semi-Axiomatic Sequent Calculus

Authors Henry DeYoung, Frank Pfenning, Klaas Pruiksma

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.29.pdf
  • Filesize: 0.58 MB
  • 22 pages

Document Identifiers

Author Details

Henry DeYoung
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Frank Pfenning
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Klaas Pruiksma
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. 1718276.

Acknowledgements

We would like to thank Siva Somayyajula and the anonymous reviewers for suggestions on an earlier version of this paper.

Cite AsGet BibTex

Henry DeYoung, Frank Pfenning, and Klaas Pruiksma. Semi-Axiomatic Sequent Calculus. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.29

Abstract

We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen’s sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Computing methodologies → Concurrent programming languages
Keywords
  • Sequent calculus
  • Curry-Howard isomorphism
  • shared memory concurrency

Metrics

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

References

  1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 1992. Google Scholar
  2. Zena M. Ariola, Aaron Bohannon, and Amr Sabry. Sequent calculi and abstract machines. ACM Transactions on Programming Languages and Systems, 31(4):13:1-13:48, May 2009. Google Scholar
  3. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222-236, Paris, France, August 2010. Springer LNCS 6269. Google Scholar
  4. Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. Mathematical Structures in Computer Science, 26(3):367-423, 2016. Special Issue on Behavioural Types. Google Scholar
  5. Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. Google Scholar
  6. Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Information and Computation, 207(10):1044-1077, October 2009. Google Scholar
  7. Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In International Conference on Functional Programming (ICFP 2000), pages 233-243. ACM Press, September 2000. Google Scholar
  8. H. B. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences, U.S.A., 20:584-590, 1934. Google Scholar
  9. H. B. Curry and R. Feys. Combinatory Logic. North-Holland, Amsterdam, 1958. Google Scholar
  10. Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, Cambridge, Massachusetts, 1991. The William James Lectures, 1976. Google Scholar
  11. Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176-210, 405-431, 1935. English translation in M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68-131, North-Holland, 1969. Google Scholar
  12. Robert H. Halstead. Multilisp: A language for parallel symbolic computation. ACM Transactions on Programming Languages and Systems, 7(4):501-539, October 1985. Google Scholar
  13. Hugo Herbelin. A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In L. Pacholski and J. Tiuryn, editors, 8th International Workshop on Computer Science Logic, pages 61-75, Kazimierz, Poland, September 1994. Springer LNCS 933. Google Scholar
  14. W. A. Howard. The formulae-as-types notion of construction. Unpublished note. An annotated version appeared in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 479-490, Academic Press (1980), 1969. Google Scholar
  15. Stephen Cole Kleene. Introduction to Metamathematics. North-Holland, 1952. Google Scholar
  16. Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, 2006. Google Scholar
  17. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, November 2009. Google Scholar
  18. Daniel R. Licata and Michael Shulman. Adjoint logic with a 2-category of modes. In International Symposium on Logical Foundations of Computer Science (LFCS), pages 219-235. Springer LNCS 9537, January 2016. Google Scholar
  19. Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Notes for three lectures given in Siena, Italy. Published in Nordic Journal of Philosophical Logic, 1(1):11-60, 1996, April 1983. Google Scholar
  20. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254-302, 2014. Google Scholar
  21. Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. Google Scholar
  22. Frank Pfenning. Types and programming languages. Lecture Notes, 2019. URL: http://www.cs.cmu.edu/~fp/courses/15814-f19.
  23. Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed. Adjoint logic. Unpublished manuscript, April 2018. URL: http://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf.
  24. Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. In F. Martins and D. Orchard, editors, Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES), pages 60-79, Prague, Czech Republic, April 2019. EPTCS 291. Google Scholar
  25. Klaas Pruiksma and Frank Pfenning. Back to futures. CoRR, abs/2002.04607, February 2020. URL: http://arxiv.org/abs/2002.04607.
  26. Jason Reed. A judgmental deconstruction of modal logic. Unpublished manuscript, May 2009. URL: http://www.cs.cmu.edu/~jcreed/papers/jdml2.pdf.
  27. Robert J. Simmons. Substructural Logical Specifications. PhD thesis, Carnegie Mellon University, November 2012. Available as Technical Report CMU-CS-12-142. Google Scholar
  28. Gerald Jay Sussman and Guy L. Steele. Scheme: An intepreter for extended lambda calculus. Higher-Order and Symbolic Computation, 11(4):405-439, December 1998. Reprint of the MIT AI Memo 349:19, December 1975. Google Scholar
  29. Philip Wadler. Propositions as sessions. In Proceedings of the 17th International Conference on Functional Programming, ICFP 2012, pages 273-286, Copenhagen, Denmark, September 2012. ACM Press. 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