The Essence of Dependent Object Types
Amin, Nada; Grütter, Karl Samuel; Odersky, Martin; Rompf, Tiark; Stucki, Sandro
2016

Files

Abstract

Focusing on path-dependent types, the paper develops foundations for Scala from first principles. Starting from a simple calculus D-<: of dependent functions, it adds records, intersections and recursion to arrive at DOT, a calculus for dependent object types. The paper shows an encoding of System F with subtyping in D-<: and demonstrates the expressiveness of DOT by modeling a range of Scala constructs in it.

Details

Title The Essence of Dependent Object Types
Author(s) Amin, Nada ; Grütter, Karl Samuel ; Odersky, Martin ; Rompf, Tiark ; Stucki, Sandro
Published in A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday
Editor(s)
Series Lecture Notes in Computer Science, 9600
Pages 249-272
Conference WadlerFest 2016, Edinburgh, UK, April 11-12, 2016
Date 2016
Publisher Springer International Publishing
ISBN 978-3-319-30936-1
Keywords
DOI https://doi.org/10.1007/978-3-319-30936-1_14
Additional link URL
Laboratories LAMP
Record Appears in Scientific production and competences > I&C - School of Computer and Communication Sciences > IINFCOM > LAMP - Programming Methods Laboratory
Peer-reviewed publications
Conference Papers
Work produced at EPFL
Published
Record creation date 2016-01-22

PDF