Document Open Access Logo

Adjoint Natural Deduction

Authors Junyoung Jang , Sophia Roshal , Frank Pfenning , Brigitte Pientka

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.15.pdf
  • Filesize: 0.79 MB
  • 23 pages

Document Identifiers

Author Details

Junyoung Jang
  • McGill University, Montreal, Canada
Sophia Roshal
  • Carnegie Mellon University, Pittsburgh, USA
Frank Pfenning
  • Carnegie Mellon University, Pittsburgh, USA
Brigitte Pientka
  • McGill University, Montreal, Canada

Funding

  • Jang, Junyoung: Fonds de recherche du Québec - Nature et Technologies (FRQNT)
  • Pientka, Brigitte: Natural Sciences and Engineering Research Council of Canada (NSERC) and Fonds de recherche du Québec - Nature et Technologies (FRQNT)

Cite AsGet BibTex

Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint Natural Deduction. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 15:1-15:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.15

Abstract

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Linear logic
Keywords
  • Substructural Logic
  • Type Systems
  • Functional Programming

Metrics

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

Related Versions

References

  1. Andreas Abel, Nils Anders Danielsson, and Oskar Eriksson. A graded modal dependent type theory with a universe and erasure, formalized. Proc. ACM Program. Lang., 7(ICFP'23):920-954, 2023. Google Scholar
  2. Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3-57, 1993. Google Scholar
  3. Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In J. Jeuring and M. Chakravarty, editors, 19th International Conference on Functional Programming (ICFP 2014), pages 363-376, Gothenburg, Sweden, September 2014. ACM. Long version available at URL: arXiv:1406.2370.
  4. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. Journal of Logic and Computation, 2(3):197-347, 1992. Google Scholar
  5. Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, 33rd Conference on Logic in Computer Science (LICS 2018), pages 56-65, Oxford, UK, July 2018. ACM. Google Scholar
  6. Andrew Barber. Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, Department of Computer Science, University of Edinburgh, September 1996. Google Scholar
  7. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Leszek Pacholski and Jerzy Tiuryn, editors, Selected Papers from the 8th International Workshop on Computer Science Logic (CSL'94), pages 121-135, Kazimierz, Poland, September 1994. Springer LNCS 933. An extended version appears as Technical Report UCAM-CL-TR-352, University of Cambridge. Google Scholar
  8. P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models (preliminary report). Technical Report UCAM-CL-TR-352, University of Cambridge, October 1994. URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-352.html.
  9. P. N. Benton, G. M. Bierman, and V. C. V. de Paiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2):177-193, March 1998. Google Scholar
  10. P. N. Benton, Gavin M. Bierman, Martin Hyland, and Valeria de Paiva. A term calculus for intuitionistic linear logic. In International Conference on Typed Lambda Calculi and Applications, pages 75-90, Utrecht, The Netherlands, 1993. Springer LNCS 664. Google Scholar
  11. P. N. Benton and Philip Wadler. Linear logic, monads, and the lambda calculus. In E. Clarke, editor, Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 420-431, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. Google Scholar
  12. 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
  13. 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
  14. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1-2):133-163, February 2000. Special issue on Proof Search in Type-Theoretic Languages, D. Galmiche and D. Pym, editors. Google Scholar
  15. Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University, Department of Computer Science, December 2003. Google Scholar
  16. Kaustuv Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In Computer Science Logic, pages 185-199. Springer LNCS 6247, August 2010. Google Scholar
  17. Pritam Choudhury, Harley Eades III, Richard A. Eisenberg, and Stephanie Weirich. A graded dependent type system with a usage-aware semantics. Proc. ACM Program. Lang., 5(POPL'21):1-32, 2021. Google Scholar
  18. Alonzo Church. The Calculi of Lambda-Conversion, volume 6 of Annals of Mathematics Studies. Princeton University Press, 1941. Google Scholar
  19. Pierre-Louis Curien, Marcelo P. Fiore, and Guillaume Munch-Maccagnoni. A theory of effects and resources: Adjunction models and polarised calculi. In R. Bodík and R. Majumdar, editors, Proceedings of the 43rd Symposium on Principles of Programming Languages (POPL 2016), pages 44-56, St. Petersburgh, Florida, USA, January 2016. ACM. Google Scholar
  20. Vincent Danos, Jean Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, pages 159-171, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  21. Michael Dummett. The Logical Basis of Metaphysics. Harvard University Press, Cambridge, Massachusetts, 1991. The William James Lectures, 1976. Google Scholar
  22. 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
  23. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  24. Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 2, pages 52-66, Pisa, Italy, March 1987. Springer-Verlag LNCS 250. Google Scholar
  25. Peter Hanukaev and Harley Eades, III. Combining dependency, grades, and adjoint logic. In 8th Workshop on Type-Driven Development (TyDe 2023), pages 58-70, Seattle, Washington, 2023. ACM. URL: https://arxiv.org/abs/2307.09563.
  26. Robert Harper. Practical Foundations for Programming Languages. Cambridge University Press, second edition, April 2016. Google Scholar
  27. 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
  28. Jack Hughes and Dominic Orchard. Resourceful program synthesis from graded linear types. In M. Fernández, editor, 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), pages 151-170, Bologna, Italy, September 2020. Springer LNCS 12561. Google Scholar
  29. Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. Subexponentials in non-commutative linear logic. ArXiv e-prints, September 2017. URL: https://arxiv.org/abs/1709.03607.
  30. Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. A logical framework with commutative and non-commutative subexponentials. In International Joint Conference on Automated Reasoning (IJCAR 2018), pages 228-245. Springer LNAI 10900, 2018. Google Scholar
  31. Stephen Cole Kleene. Introduction to Metamathematics. North-Holland, 1952. Google Scholar
  32. John Launchbury. A natural semantics for lazy evaluation. In 20th Annual Symposium on Principles of Programming Languages (POPL 1993), pages 144-154, Charleston, South Carolina, January 1993. ACM. Google Scholar
  33. 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
  34. 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
  35. Daniel R. Licata, Michael Shulman, and Mitchell Riley. A fibrational framework for substructural and modal logics. In Dale Miller, editor, Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD'17), pages 25:1-25:22, Oxford, UK, September 2017. LIPIcs. Google Scholar
  36. 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. URL: http://www.hf.uio.no/ifikk/forskning/publikasjoner/tidsskrifter/njpl/vol1no1/meaning.pdf.
  37. Conor McBride. I got plenty o' nuttin'. In Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella, editors, A List of Successes That can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 207-233. Springer LNCS 9600, 2016. Google Scholar
  38. Benjamin Moon, Harley Eades III, and Dominic Orchard. Graded modal dependent type theory. In 30th European Symposium on Programming (ESOP'21), volume 12648 of Lecture Notes in Computer Science, pages 462-490. Springer, 2021. Google Scholar
  39. Alan Mycroft. The theory and practice of transforming call-by-need into call-by-value. In 4th International Symposium on Programming, pages 269-281. Springer LNCS 83, 1980. Google Scholar
  40. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In Proceedings of the 11th International Conference on Principles and Practice of Declarative Programming (PPDP), pages 129-140, Coimbra, Portugal, September 2009. ACM. Google Scholar
  41. Vivek Nigam, Elaine Pimental, and Giselle Reis. An extended framework for specifying and reasoning about proof systems. Journal of Logic and Computation, 26(2):539-576, 2016. Google Scholar
  42. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999. Google Scholar
  43. Frank Pfenning and Klaas Pruiksma. Relating message passing and shared memory, proof-theoretically. In S. Jongmans and A. Lopes, editors, 25th International Conference on Coordination Models and Languages (COORDINATION 2023), pages 3-27, Lisbon, Portugal, June 2023. Springer LNCS 13908. Notes to an invited talk. Google Scholar
  44. Dag Prawitz. Natural Deduction. Almquist & Wiksell, Stockholm, 1965. Google Scholar
  45. Klaas Pruiksma. Adjoint Logic with Applications. PhD thesis, Carnegie Mellon University, 2024. In preparation. Google Scholar
  46. 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.
  47. Klaas Pruiksma and Frank Pfenning. A message-passing interpretation of adjoint logic. Journal of Logical and Algebraic Methods in Programming, 120(100637), 2021. Google Scholar
  48. Klaas Pruiksma and Frank Pfenning. Back to futures. Journal of Functional Programming, 32:e6, 2022. Google Scholar
  49. Jason Reed. A judgmental deconstruction of modal logic. Unpublished manuscript, May 2009. URL: http://www.cs.cmu.edu/~jcreed/papers/jdml2.pdf.
  50. The Rust programming language. Available at https://www.rust-lang.org/. Accessed January 15, 2024.
  51. Jesse A. Tov and Riccardo Pucella. Practical affine types. In T. Ball and M. Sagiv, editors, Proceedings of the 38th Symposium on Principles of Programming Languages (POPL 2011), pages 447-458. ACM Press, January 2011. Google Scholar
  52. Anne S. Troelstra. Natural deduction for intuitionistic linear logic. Annals of Pure and Applied Logic, 73(1):79-108, 1995. Google Scholar
  53. Philip Wadler. Linear types can change the world. In IFIP TC, volume 2, pages 347-359, 1990. Google Scholar
  54. 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
  55. James Wood and Robert Atkey. A framework for substructural type systems. In Ilya Sergey, editor, 31st European Symposium on Programming (ESOP 2022), pages 376-402, Munich, Germany, April 2022. Springer LNCS 13240. 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