Document Open Access Logo

Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints

Authors Olivier Laurent , Jui-Hsuan Wu

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.22.pdf
  • Filesize: 0.81 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Lambda calculus
Keywords
  • Intersection types
  • subtyping
  • non-wellfounded proofs
  • fixpoints
  • cut elimination

Metrics

Abstract

Subtyping is a key ingredient of many intersection type systems. In the case of the BCD system, B. Pierce gave a transitivity-free presentation of subtyping. This provides better structural properties for the analysis of this relation and leads to a simple decision algorithm.
We generalize this transitivity-free approach to a general class of extensions of BCD allowing to impose some pre-order as well as some fixpoint equations on atoms. This includes in particular the case of various intersection type systems compatible with η-equality (Scott, Park, etc.).
Proving the equivalence between the transitivity-free systems and their BCD-style presentation is addressed by means of cut-elimination techniques from proof theory. Due to the presence of fixpoints, we are led to introduce non-wellfounded derivations. In the context of the structural analysis of intersection subtyping, this happens to be the first use of infinitary derivations.

Cite As Get BibTex

Olivier Laurent and Jui-Hsuan Wu. Non-Wellfounded Derivations for Intersection Subtyping with Fixpoints. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.22

Author Details

Olivier Laurent
  • CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France
Jui-Hsuan Wu
  • CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, Lyon, France

Funding

This work was supported by the project ReCiProg (ANR-21-CE48-0019) operated by the French National Research Agency (ANR).

Acknowledgements

Thanks to A. Saurin and D. Pous for discussions about infinitary proofs.

Supplementary Materials

References

  1. Fabio Alessi, Franco Barbanera, and Mariangiola Dezani-Ciancaglini. Intersection types and lambda models. Theoretical Computer Science, 355(2):108-126, April 2006. URL: https://doi.org/10.1016/j.tcs.2006.01.004.
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48:931-940, 1983. URL: https://doi.org/10.2307/2273659.
  3. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  4. Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The essence of nested composition. In Todd Millstein, editor, 32nd European Conference on Object-Oriented Programming (ECOOP), volume 109 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:33. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.22.
  5. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and D_∞-lambda-models. Information and Computation, 72(2):85-116, 1987. URL: https://doi.org/10.1016/0890-5401(87)90042-3.
  6. Nils Anders Danielsson and Thorsten Altenkirch. Subtyping, declaratively. In Claude Bolduc, Jules Desharnais, and Béchir Ktari, editors, Mathematics of Program Construction, pages 100-118. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13321-3_8.
  7. Anupam Das, Abhishek De, and Alexis Saurin. Comparing infinitary systems for linear logic with fixed points. In Patricia Bouyer and Srikanth Srinivasan, editors, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023), volume 284 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1-40:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2023.40.
  8. Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable terms in filter models. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction, volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.3.
  9. Mariangiola Dezani-Ciancaglini, Furio Honsell, and Yoko Motohama. Compositional characterisations of λ-terms using intersection types. Theoretical Computer Science, 340(3):459-495, 2005. URL: https://doi.org/10.1016/j.tcs.2005.03.011.
  10. Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49-75, 1992. URL: https://doi.org/10.1016/0022-0000(92)90040-P.
  11. Olivier Laurent. A syntactic introduction to intersection types. Unpublished note, April 2012. URL: http://perso.ens-lyon.fr/olivier.laurent/tutinter.pdf.
  12. Olivier Laurent and Jui-Hsuan Wu. Intersection Subtyping with Fixpoints. Software, ANR-21-CE48-0019, (visited on 2026-06-30). URL: https://github.com/olaure01/islogic/tree/FSCD2026
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.26938
  13. David Park. The Y-combinator in Scott’s lambda-calculus models. Technical Report 13, University of Warwick, Department of Computer Science, June 1976. URL: https://wrap.warwick.ac.uk/46310/.
  14. Benjamin C. Pierce. A decision procedure for the subtype relation on intersection types with bounded variables. Technical Report CMU-CS-89-169, School of Computer Science, Carnegie Mellon University, August 1989. URL: https://doi.org/10.1184/R1/6587339.v1.
  15. Dana Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. URL: https://doi.org/10.1007/BFb0073967.
  16. Pawel Urzyczyn. Which equations on intersection types preserve normalization? TLCA List of Open Problems, problem #11, 1993. URL: https://tlca.di.unito.it/opltlca/opltlcasu18.html.
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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact