The Essence of Dependent Object Types

DOI10.1007/978-3-319-30936-1_14zbMath1343.68046OpenAlexW2289066165MaRDI QIDQ3188291

Sandro Stucki, Tiark Rompf, Samuel Gruetter, Martin Odersky, Nada Amin

Publication date: 17 August 2016

Published in: A List of Successes That Can Change the World (Search for Journal in Brave)

Full work available at URL: http://infoscience.epfl.ch/record/215280

zbMATH Keywords

dependent typesScalacalculus for dependent object types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18) Logic in computer science (03B70)

Related Items

Soundness Conditions for Big-Step Semantics ⋮ A calculus with recursive types, record concatenation and subtyping

Uses Software

• Scala
• 1ML
• MixML
• GitHub
• Dotty
• HMap
• Tribe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension of system \(F\) with subtyping
• Full Reduction in the Face of Absurdity
• 1ML – core and modules united (F-ing first-class modules)
• A framework for defining logics
• System F with coercion constraints
• F-ing modules
• Mixin' up the ML module system
• Modeling abstract types in modules with open existential types
• A virtual class calculus
• Type soundness proofs with definitional interpreters
• A Core Calculus for Scala Type Checking