Semi-Axiomatic Sequent Calculus
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.
Sequent calculus
Curry-Howard isomorphism
shared memory concurrency
Theory of computation~Proof theory
Computing methodologies~Concurrent programming languages
29:1-29:22
Regular Paper
This material is based upon work supported by the National Science Foundation under Grant No. 1718276.
We would like to thank Siva Somayyajula and the anonymous reviewers for suggestions on an earlier version of this paper.
Henry
DeYoung
Henry DeYoung
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Frank
Pfenning
Frank Pfenning
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Klaas
Pruiksma
Klaas Pruiksma
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
10.4230/LIPIcs.FSCD.2020.29
Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 1992.
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.
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.
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.
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.
Iliano Cervesato and Andre Scedrov. Relating state-based and process-based concurrency through linear logic. Information and Computation, 207(10):1044-1077, October 2009.
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.
H. B. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences, U.S.A., 20:584-590, 1934.
H. B. Curry and R. Feys. Combinatory Logic. North-Holland, Amsterdam, 1958.
Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, Cambridge, Massachusetts, 1991. The William James Lectures, 1976.
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.
Robert H. Halstead. Multilisp: A language for parallel symbolic computation. ACM Transactions on Programming Languages and Systems, 7(4):501-539, October 1985.
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.
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.
Stephen Cole Kleene. Introduction to Metamathematics. North-Holland, 1952.
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.
Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, November 2009.
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.
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.
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.
Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000.
Frank Pfenning. Types and programming languages. Lecture Notes, 2019. URL: http://www.cs.cmu.edu/~fp/courses/15814-f19.
http://www.cs.cmu.edu/~fp/courses/15814-f19
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.
http://www.cs.cmu.edu/~fp/papers/adjoint18b.pdf
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.
Klaas Pruiksma and Frank Pfenning. Back to futures. CoRR, abs/2002.04607, February 2020. URL: http://arxiv.org/abs/2002.04607.
http://arxiv.org/abs/2002.04607
Jason Reed. A judgmental deconstruction of modal logic. Unpublished manuscript, May 2009. URL: http://www.cs.cmu.edu/~jcreed/papers/jdml2.pdf.
http://www.cs.cmu.edu/~jcreed/papers/jdml2.pdf
Robert J. Simmons. Substructural Logical Specifications. PhD thesis, Carnegie Mellon University, November 2012. Available as Technical Report CMU-CS-12-142.
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.
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.
Henry DeYoung, Frank Pfenning, and Klaas Pruiksma
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode