Document Open Access Logo

Towards the Type Safety of Pure Subtype Systems

Authors Valentin Pasquale , Álvaro García-Pérez

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.37.pdf
  • Filesize: 1 MB
  • 16 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Lambda calculus
  • Pure subtype systems
  • Dependent types
  • Higher-order subtyping
  • Type safety

Metrics

Abstract

Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems.
In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.

Cite As Get BibTex

Valentin Pasquale and Álvaro García-Pérez. Towards the Type Safety of Pure Subtype Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.37

Author Details

Valentin Pasquale
  • CEA List, Université Paris-Saclay, France
Álvaro García-Pérez
  • CEA List, Université Paris-Saclay, France

References

  1. Mads S. Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Proceedings of International Conference on Principles and Practice of Declarative Programming, pages 8-19, 2003. URL: https://doi.org/10.1145/888251.888254.
  2. Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 249-272, 2016. URL: https://doi.org/10.1007/978-3-319-30936-1_14.
  3. David Aspinall. Subtyping with singleton types. In International Workshop on Computer Science Logic, pages 1-15. Springer, 1994. URL: https://doi.org/10.1007/BFB0022243.
  4. Lennart Augustsson. Cayenne—a language with dependent types. ACM SIGPLAN Notices, 34(1):239-250, 1998. Google Scholar
  5. Henk Barendregt. Lambda Calculi with Types, volume 2. Oxford University Press, 1993. Google Scholar
  6. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of agda-a functional language with dependent types. In Theorem Proving in Higher Order Logics, pages 73-78. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_6.
  7. Edwin Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of functional programming, 23(5):552-593, 2013. URL: https://doi.org/10.1017/S095679681300018X.
  8. Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of System F with subtyping. Information and computation, 109(1-2):4-56, 1994. URL: https://doi.org/10.1006/INCO.1994.1013.
  9. Chris Casinghino. Combining proofs and programs. University of Pennsylvania, 2014. Google Scholar
  10. Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. Combining proofs and programs in a dependently typed language. ACM SIGPLAN Notices, 49(1):33-45, 2014. URL: https://doi.org/10.1145/2535838.2535883.
  11. Gang Chen. Subtyping calculus of construction. In International Symposium on Mathematical Foundations of Computer Science, pages 189-198. Springer, 1997. Google Scholar
  12. Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. Google Scholar
  13. Matthias Felleisen. The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Department of Computer Science, Indiana University, 1987. Google Scholar
  14. Herman Geuvers and Joep Verkoelen. On fixed point and looping combinators in type theory, 2009. Google Scholar
  15. J. Roger Hindley and Jonathan P. Seldin. Lambda-Calculus and Combinators, An Introduction, 2nd Edition. Cambridge University Press, 2008. Google Scholar
  16. Douglas J. Howe. The computational behaviour of girard’s paradox. In Proceedings of the Symposium on Logic in Computer Science, pages 205-214. IEEE Computer Society, 1987. Google Scholar
  17. Antonius J. C. Hurkens. A simplification of girard’s paradox. In Typed Lambda Calculi and Applications: Second International Conference on Typed Lambda Calculi and Applications, TLCA'95 Edinburgh, United Kingdom, April 10-12, 1995 Proceedings 2, pages 266-278. Springer, 1995. URL: https://doi.org/10.1007/BFB0014058.
  18. DeLesley S. Hutchins. Pure subtype systems: A type theory for extensible software. The University of Edinburgh, 2009. Google Scholar
  19. DeLesley S. Hutchins. Pure subtype systems. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '10, pages 287-298. Association for Computing Machinery, 2010. URL: https://doi.org/10.1145/1706299.1706334.
  20. Jean-Louis Krivine. A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation, 20(3):199-207, 2007. URL: https://doi.org/10.1007/S10990-007-9018-9.
  21. Simon Marlow et al. Haskell 2010 language report, 2010. URL: http://www.haskell.org/.
  22. James McKinna and Robert Pollack. Pure type systems formalized. In International Conference on Typed Lambda Calculi and Applications, pages 289-305. Springer, 1993. URL: https://doi.org/10.1007/BFB0037113.
  23. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  24. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical structures in computer science, 11(4):511-540, 2001. URL: https://doi.org/10.1017/S0960129501003322.
  25. Benjamin C. Pierce. Bounded quantification is undecidable. Information and Computation, 112(1):131-165, 1994. URL: https://doi.org/10.1006/INCO.1994.1055.
  26. Benjamin C. Pierce and Martin Steffen. Higher-order subtyping. Theoretical computer science, 176(1-2):235-282, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00096-5.
  27. Tiark Rompf and Nada Amin. Type soundness for dependent object types (dot). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 624-641, 2016. URL: https://doi.org/10.1145/2983990.2984008.
  28. Vilhelm Sjoberg. A dependently typed language with nontermination. University of Pennsylvania, 2015. Google Scholar
  29. Vincent van Oostrom. Confluence by decreasing diagrams. Theoretical computer science, 126(2):259-280, 1994. URL: https://doi.org/10.1016/0304-3975(92)00023-K.
  30. Philip Wadler. The expression problem, 1998. Posted to Java Genericity internet mailing list. URL: https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt.
  31. Yanpeng Yang and Bruno C. d. S. Oliveira. Unifying typing and subtyping. Proceedings of the ACM on Programming Languages, 1(OOPSLA):47:1-47:26, 2017. URL: https://doi.org/10.1145/3133871.
  32. Matthias Zenger and Martin Odersky. Independently extensible solutions to the expression problem. In Workshop on Foundations of Object-Oriented Languages, 2005. URL: http://zenger.org/papers/fool05.pdf.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact