In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. Unfortunately there has been much less work on dependently typed calculi for object-oriented programming. This is partly because it is widely acknowledged that the combination between dependent types and subtyping is particularly challenging.
This paper presents λI≤, which is a dependently typed generalization of System F≤. The resulting calculus follows the style of Pure Type Systems, and contains a single unified syntactic sort that accounts for expressions, types and kinds. To address the challenges posed by the combination of dependent types and subtyping, λI≤ employs a novel technique that unifies typing and subtyping. In λI≤ there is only a judgement that is akin to a typed version of subtyping. Both the typing relation, as well as type well-formedness are just special cases of the subtyping relation. The resulting calculus has a rich metatheory and enjoys of several standard and desirable properties, such as subject reduction, transitivity of subtyping, narrowing as well as standard substitution lemmas. All the metatheory of λI≤ is mechanically proved in the Coq theorem prover. Furthermore, (and as far as we are aware) λI≤ is the first dependently typed calculus that completely subsumes System F≤, while preserving various desirable properties.
Wed 25 OctDisplayed time zone: Tijuana, Baja California change
10:30 - 12:00
|SAVI Objects: Sharing and Virtuality Incorporated
Izzat El Hajj University of Illinois at Urbana-Champaign, USA, Thomas B. Jablin University of Illinois at Urbana-Champaign, USA / Multicoreware, USA, Dejan Milojicic Hewlett Packard Labs, USA, Wen-mei Hwu University of Illinois at Urbana-Champaign, USADOI
|A Simple Soundness Proof for Dependent Object Types
Marianna Rapoport University of Waterloo, Canada, Ifaz Kabir University of Waterloo, Canada, Paul He University of Waterloo, Canada, Ondřej Lhoták University of Waterloo, CanadaDOI
|Unifying Typing and Subtyping
Avik Chaudhuri Facebook, USA, Panagiotis Vekris University of California at San Diego, USA, Sam Goldman Facebook, USA, Marshall Roch Facebook, USA, Gabriel Levi Facebook, USADOI