Document Open Access Logo

Substructural Parametricity

Authors C. B. Aberlé , Karl Crary , Chris Martens , Frank Pfenning

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2025.4.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
Keywords
  • Substructural type systems
  • logical relations
  • ordered logic

Metrics

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

Abstract

Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.

Cite As Get BibTex

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning. Substructural Parametricity. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.FSCD.2025.4

Author Details

C. B. Aberlé
  • Carnegie Mellon University, Pittsburgh, PA, USA
Karl Crary
  • Carnegie Mellon University, Pittsburgh, PA, USA
Chris Martens
  • Northeastern University, Boston, MA, USA
Frank Pfenning
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This material is based upon work supported by the United States Air Force Office of Scientific Research under grant number A210038S002 (Tristan Nguyen, program manager). Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.

Acknowledgements

The authors thank Bob Atkey and Stephanie Balzer for helpful comments regarding related work.

References

  1. Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages, 4(ICFP):1-28, 2020. URL: https://doi.org/10.1145/3408972.
  2. Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26:e2, 2016. URL: https://doi.org/10.1017/S0956796816000022.
  3. Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In 36th Symposium on Principles of Programming Languages (POPL 2009), pages 340-353, Savannah, Georgia, USA, January 2009. ACM. URL: https://doi.org/10.1145/1480881.1480925.
  4. Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In 10th International Conference on Functional Programming (ICFP 2005), pages 78-91, 2005. URL: https://doi.org/10.1145/1086365.1086376.
  5. Amal Ahmed, Matthew Fluet, and Greg Morrisett. L³: a linear language with locations. Fundamenta Informaticae, 77(4):397-449, 2007. Google Scholar
  6. Bob Atkey and James Wood. Context constrained computation. In 3rd Workshop on Type-Driven Development (TyDe'18), 2018. Google Scholar
  7. 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. URL: https://doi.org/10.1145/3209108.3209189.
  8. Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. arXiv preprint arXiv:2309.00192, 2023. URL: https://doi.org/10.48550/arXiv.2309.00192.
  9. 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
  10. Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages, 5(ICFP):1-29, 2021. URL: https://doi.org/10.1145/3473586.
  11. Luís Caires, Jorge A Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In 22nd European Symposium on Programming (ESOP 2013), pages 330-349, Rome, Italy, March 2013. Springer LNCS 7792. URL: https://doi.org/10.1007/978-3-642-37036-6_19.
  12. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In P.Gastin and F.Laroussinie, editors, 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222-236, Paris, France, August 2010. Springer LNCS 6269. URL: https://doi.org/10.1007/978-3-642-15375-4_16.
  13. Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual Symposium on Logic in Computer Science (LICS 2021), pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470654.
  14. Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading policies for flexible information flow control in session-typed concurrency (artifact). Dagstuhl Artifacts Series, 10(2):4-1, 2024. Google Scholar
  15. Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In 35th Symposium on Logic in Computer Science (LICS 2020), pages 440-453, Saarbrücken, Germany, July 2020. ACM. Google Scholar
  16. Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19-50, January 2010. URL: https://doi.org/10.1017/S0956796809990268.
  17. Aïna Linn Georges, Benjamin Peters, Laila Albeheiry, Leo White, Stephan Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. Data race freedom à la mode. In Principles of Programming Languages (POPL 2025), volume 9 of Proceedings on Programming Languages, pages 656-686. ACM, January 2025. URL: https://doi.org/10.1145/3704859.
  18. 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. URL: https://doi.org/10.1007/BFB0014972.
  19. Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint natural deduction. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), pages 15:1-15:23, Tallinn, Estonia, July 2024. LIPIcs 299. Extended version available as URL: https://arxiv.org/abs/2402.01428.
  20. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  21. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In 42nd Annual Symposium on Principles of Programming Languages (POPL 2015), pages 637-650, Mumbai, India, January 2015. ACM. URL: https://doi.org/10.1145/2676726.2676980.
  22. Gilles Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22-39. Springer-Verlag LNCS 247, 1987. URL: https://doi.org/10.1007/BFB0039592.
  23. Norihiro Kamide. Kripke semantics for modal substructural logics. Journal of Logic, Language and Information, 11:453-470, 2002. URL: https://doi.org/10.1023/A:1019915908844.
  24. 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. URL: https://doi.org/10.1007/978-3-319-94205-6_16.
  25. Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154-170, 1958. Google Scholar
  26. Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. In Proceedings of the ACM on Programming Languages, volume 7 (OOPSLA 2023), pages 286-315, April 2023. Extended version available as URL: https://arxiv.org/abs/2303.05491.
  27. Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP²: Fully in-place functional programming. In International Conference on Functional Programming (ICFP 2023), Proceedings on Programming Languages, pages 275-304. ACM, August 2023. URL: https://doi.org/10.1145/3607840.
  28. Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley. The functional essence of imperative binary search trees. In Programming Language Design and Implementation (PLDI 2024), volume 8 of Proceedings on Programming Languages, pages 518-542. ACM, January 2024. URL: https://doi.org/10.1145/3656398.
  29. Wendy MacCaull. Relational semantics and a relational proof system for full Lambek calculus. Journal of Symbolic Logic, 63(2):623-637, 1998. URL: https://doi.org/10.2307/2586855.
  30. John C Mitchell. Representation independence and data abstraction. In Proceedings of the 13th Symposium on Principles of Programming Languages (POPL 1986), pages 263-276. ACM, 1986. URL: https://doi.org/10.1145/512644.512669.
  31. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. URL: https://doi.org/10.1145/1352582.1352591.
  32. Peter W O'Hearn and David J Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215-244, 1999. URL: https://doi.org/10.2307/421090.
  33. Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Termination in session-based concurrency via linear logical relations. In H. Seidl, editor, 22nd European Symposium on Programming (ESOP 2012), pages 539-558, Tallinn, Estonia, March 2012. Springer LNCS 7211. Google Scholar
  34. 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. URL: https://doi.org/10.1016/J.IC.2014.08.001.
  35. 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. URL: https://doi.org/10.1007/978-3-031-35361-1_1.
  36. Jeff Polakow. Ordered Linear Logic and Applications. PhD thesis, Department of Computer Science, Carnegie Mellon University, August 2001. Google Scholar
  37. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. URL: https://doi.org/10.1007/3-540-48959-2_21.
  38. Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed. Adjoint logic and its concurrent operational interpretation. Unpublished manuscript, January 2018. Google Scholar
  39. Jason Reed. Hybridizing a logical framework. In Proceedings of the International Workshop on Hybrid Logic (HyLo'06), pages 135-148. Electronic Notes in Theoretical Computer Science, v.174(6), 2007. Google Scholar
  40. Jason Reed and Frank Pfenning. A constructive approach to the resource semantics of substructural logics. Unpublished Manuscript, May 2010. URL: https://www.cs.cmu.edu/~jcreed/papers/rp-substruct.pdf.
  41. Jason C. Reed. A Hybrid Logical Framework. PhD thesis, Carnegie Mellon University, September 2009. Available as Technical Report CMU-CS-09-155. Google Scholar
  42. John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A. Mason, editor, Information Processing 83, pages 513-523. Elsevier, September 1983. Google Scholar
  43. Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13:11-49, 2000. Notes for lecture course given at the International Summer School in Computer Programming at Copenhagen, Denmark, August 1967. URL: https://doi.org/10.1023/A:1010000313106.
  44. Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information flow control in cyclic process networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024), pages 40:1-40:30. LIPIcs 313, 2024. URL: https://doi.org/10.4230/LIPICS.ECOOP.2024.40.
  45. Victoria Vollmer, Danielle Marshall, Harley Eades, III, and Dominic Orchard. A mixed linear and graded logic: Proofs, terms, and models. In 33rd Conference on Computer Science Logic (CSL 2025), pages 32:1-32:21, Amsterdam, The Netherlands, February 2025. LIPIcs 326. URL: https://doi.org/10.4230/LIPICS.CSL.2025.32.
  46. Philip Wadler. Theorems for free! In J. Stoy, editor, Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture (FPCA'89), pages 347-359, London, UK, September 1989. ACM. URL: https://doi.org/10.1145/99370.99404.
  47. Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational parametricity for a polymorphic linear lambda calculus. In K. Ueda, editor, 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), pages 344-359. Springer LNCS 6461, 2010. URL: https://doi.org/10.1007/978-3-642-17164-2_24.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact