research-article

Open access

A Logical Approach to Deciding Semantic Subtyping

Authors:

Pierre Genevès,

Nabil LayaïdaAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 38, Issue 1

Article No.: 3, Pages 1 - 31

https://doi.org/10.1145/2812805

Published: 16 October 2015 Publication History

Abstract

We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types, together with type variables. We consider the subtyping relation defined by Castagna and Xu [2011] over such type expressions and show how this relation can be decided in EXPTIME, answering an open question. The novelty, originality and strength of our solution reside in introducing a logical modeling for the semantic subtyping framework. We model semantic subtyping in a tree logic and use a satisfiability-testing algorithm in order to decide subtyping. We report on practical experiments made with a full implementation of the system. This provides a powerful polymorphic type system aiming at maintaining full static type-safety of functional programs that manipulate trees, even with higher-order functions, which is particularly useful in the context of XML.

References

[1]

Michael Benedikt and James Cheney. 2010. Destabilizers and independence of XML updates. Proceedings of the VLDB Endowment 3, 1, 906--917.

Digital Library

[2]

Véronique Benzaken, Giuseppe Castagna, and Alain Frisch. 2003. CDuce: An XML-centric general-purpose language. In Proceedings of the 8th International Conference on Functional Programming (ICFP’03). Uppsala, Sweden, 51--63. http://doi.acm.org/10.1145/944705.944711

Digital Library

[3]

Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, and David Langworthy. 2010. Semantic subtyping with an SMT solver. In Proceedings of the 15th International Conference on Functional Programming (ICFP’10). Baltimore, MD, 105--116. http://doi.acm.org/10.1145/1863543.1863560

Digital Library

[4]

Scott Boag, Don Chamberlin, Mary F. Fernández, Daniela Florescu, Jonathan Robie, and Jérôme Siméon. 2007. XQuery 1.0: An XML Query Language, W3C Recommendation.

[5]

Randal E. Bryant. 1986. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35, 8, 677--691.

Digital Library

[6]

Cristiano Calcagno, Luca Cardelli, and Andrew D. Gordon. 2005. Deciding validity in a spatial logic for trees. Journal of Functional Programming 15, 4, 543--572.

Digital Library

[7]

Luca Cardelli and Andrew D. Gordon. 2000. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’00). ACM, New York, NY, 365--377.

Digital Library

[8]

Giuseppe Castagna and Zhiwu Xu. 2011. Set-theoretic foundation of parametric polymorphism and subtyping. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP’11). ACM, Tokyo, 94--106.

Digital Library

[9]

James Clark and Steve DeRose. 1999. XML Path Language (XPath) Version 1.0, W3C Recommendation. Retrieved August 31, 2015 from http://www.w3.org/TR/1999/REC-xpath-19991116.

[10]

Edmund M. Clarke Jr., Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA.

Digital Library

[11]

Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08). Budapest, 337--340. http://dx.doi.org/10.1007/978-3-540-78800-3_24.

[12]

A. Frisch, G. Castagna, and V. Benzaken. 2008. Semantic subtyping: Dealing set-theoretically with function, union, intersection, and negation types. Journal of the ACM 55, 4, 1--64.

Digital Library

[13]

Pierre Genevès. 2006. Logics for XML. Ph.D. Dissertation. Institut National Polytechnique de Grenoble. Retrieved August 31, 2015 from http://wam.inrialpes.fr/publications/2006/geneves-phd.pdf.

[14]

Pierre Genevès, Nabil Layaïda, and Vincent Quint. 2009. Identifying query incompatibilities with evolving XML schemas. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP’09). ACM, New York, NY, 221--230.

Digital Library

[15]

Pierre Genevès, Nabil Layaïda, and Alan Schmitt. 2007. Efficient static analysis of XML paths and types. In Proceedings of the 28th Conference on Programming Language Design and iImplementation (PLDI’07). San Diego, CA, 342--351. http://doi.acm.org/10.1145/1250734.1250773

Digital Library

[16]

Pierre Genevès, Nabil Layaïda, Alan Schmitt, and Nils Gesbert. 2015. Efficiently deciding μ-calculus with converse over finite trees. ACM Transactions on Computational Logic 16, 2, 16:1--16:41.

Digital Library

[17]

Nils Gesbert, Pierre Genevès, and Nabil Layaïda. 2011. Parametric polymorphism and semantic subtyping: The logical connection. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP’11). ACM, Tokyo, 107--116.

Digital Library

[18]

H. Hosoya, A. Frisch, and G. Castagna. 2009. Parametric polymorphism for XML. ACM Transactions on Programming Languages and Systems 32, 1, 1--56.

Digital Library

[19]

Haruo Hosoya and Benjamin C. Pierce. 2003. XDuce: A statically typed XML processing language. ACM Transactions on Internet Technology 3, 2, 117--148. http://doi.acm.org/10.1145/767193.767195

Digital Library

[20]

Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. 2005. Regular expression types for XML. ACM Transactions on Programming Languages and Systems 27, 1, 46--90. http://doi.acm.org/10.1145/1053468.1053470.

Digital Library

[21]

Gérard P. Huet. 1997. The zipper. Journal of Functional Programming 7, 5, 549--554.

Digital Library

[22]

Barbara Liskov and Jeannette M. Wing. 1994. A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems 16, 6, 1811--1841.

Digital Library

[23]

R. Milner, L. Morris, and M. Newey. 1975. A logic for computable functions with reflexive and polymorphic types. In Conference on Proving and Improving Programs, Arc-et-Senans, France. IRIA-Laboria, 78150 Le Chesnay, France, 371--394.

[24]

Guoqiang Pan, Ulrike Sattler, and Moshe Y. Vardi. 2006. BDD-based decision procedures for the modal logic K. Journal of Applied Non-classical Logics 16, 1--2, 169--208.

[25]

John C. Reynolds. 1983. Types, abstraction and parametric polymorphism. In IFIP Congress. 513--523.

[26]

Jonathan Robie, Don Chamberlin, Michael Dyck, and John Snelson. 2014. XQuery 3.0: An XML Query Language, W3C Recommendation. Retrieved August 31, 2015 from http://www.w3.org/TR/xquery-30/.

[27]

Jérôme Vouillon. 2006. Polymorphic regular tree types and patterns. In Proceedings of the 33rd Symposium on Principles of Programming Languages (POPL’06). 103--114. http://doi.acm.org/10.1145/1111037.1111047.

Digital Library

Cited By

Chlyah SGesbert NGenevès PLayaïda N(2025)Efficient iterative programs with distributed data collectionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2025.101047144(101047)Online publication date: Mar-2025
https://doi.org/10.1016/j.jlamp.2025.101047
Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Castagna G(2023)Programming with Union, Intersection, and Negation TypesThe French School of Programming10.1007/978-3-031-34518-0_12(309-378)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_12
Show More Cited By

Index Terms

A Logical Approach to Deciding Semantic Subtyping
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

On the power of coercion abstraction
POPL '12

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
On the power of coercion abstraction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 38, Issue 1

October 2015

88 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/2836326

Editor:
Jens Palsberg
University of California, Los Angeles, USA

Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 October 2015

Accepted: 01 August 2015

Received: 01 April 2015

Published in TOPLAS Volume 38, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Agence Nationale de la Recherche

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
367
Total Downloads

Downloads (Last 12 months)88
Downloads (Last 6 weeks)20

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chlyah SGesbert NGenevès PLayaïda N(2025)Efficient iterative programs with distributed data collectionsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2025.101047144(101047)Online publication date: Mar-2025
https://doi.org/10.1016/j.jlamp.2025.101047
Castagna GLaurent MNguyễn K(2024)Polymorphic Type Inference for Dynamic LanguagesProceedings of the ACM on Programming Languages10.1145/36328828:POPL(1179-1210)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632882
Castagna G(2023)Programming with Union, Intersection, and Negation TypesThe French School of Programming10.1007/978-3-031-34518-0_12(309-378)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_12
Castagna GLanvin VPetrucciani TSiek J(2019)Gradual typing: a new perspectiveProceedings of the ACM on Programming Languages10.1145/32903293:POPL(1-32)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290329
Muehlboeck FTate R(2018)Empowering union and intersection types with integrated subtypingProceedings of the ACM on Programming Languages10.1145/32764822:OOPSLA(1-29)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276482

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents