Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Journal articles
  4. Qualifying System F<inf>&lt;:</inf> Some Terms and Conditions May Apply
 
research article

Qualifying System F<: Some Terms and Conditions May Apply

Lee, Edward
•
Zhao, Yaoyu  
•
Lhoták, OndÅ™ej
Show more
April 29, 2024
Proceedings of the ACM on Programming Languages

Type qualifiers offer a lightweight mechanism for enriching existing type systems to enforce additional, desirable, program invariants. They do so by offering a restricted but effective form of subtyping. While the theory of type qualifiers is well understood and present in many programming languages today, polymorphism over type qualifiers remains an area less well examined. We explore how such a polymorphic system could arise by constructing a calculus, System F-sub-Q, which combines the higher-rank bounded polymorphism of System F-sub with the theory of type qualifiers. We explore how the ideas used to construct System F-sub-Q can be reused in situations where type qualifiers naturally arise - -in reference immutability, function colouring, and capture checking. Finally, we re-examine other qualifier systems in the literature in light of the observations presented while developing System F<-Q.

  • Details
  • Metrics
Type
research article
DOI
10.1145/3649832
Scopus ID

2-s2.0-85195782521

Author(s)
Lee, Edward

University of Waterloo

Zhao, Yaoyu  

École Polytechnique Fédérale de Lausanne

Lhoták, OndÅ™ej

University of Waterloo

You, James

University of Waterloo

Satheeskumar, Kavin

University of Waterloo

Brachthäuser, Jonathan Immanuel

Eberhard Karls Universität Tübingen

Date Issued

2024-04-29

Published in
Proceedings of the ACM on Programming Languages
Volume

8

Issue

OOPSLA1

Article Number

115

Subjects

System F-sub

•

Type Qualifiers

•

Type Systems

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LAMP1  
FunderFunding(s)Grant NumberGrant URL

Natural Sciences and Engineering Research Council of Canada

Available on Infoscience
January 21, 2025
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/243076
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés