The essence of dependent object types

DOI10.1007/978-3-319-30936-1_14MaRDI QIDQ3188291zbMATH OpenOpenAlexFDO

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

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

calculus for dependent object typesdependent typesScala

Mathematics Subject Classification ID

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

Recommendations

• A Core Calculus for Scala Type Checking
• Dependent ML An approach to practical programming with dependent types
• Dependent type system with subtyping I: Type level transitivity elimination
• scientific article; zbMATH DE number 2090721
• Dependent types with subtyping and late-bound overloading

Cites work

• 1ML -- core and modules united (F-ing first-class modules)
• A Core Calculus for Scala Type Checking
• A framework for defining logics
• A virtual class calculus
• An extension of system \(F\) with subtyping
• F-ing modules
• Full Reduction in the Face of Absurdity
• scientific article; zbMATH DE number 1728245 (Why is no real title available?)
• scientific article; zbMATH DE number 2089395 (Why is no real title available?)
• scientific article; zbMATH DE number 3637819 (Why is no real title available?)
• scientific article; zbMATH DE number 1231468 (Why is no real title available?)
• Mixin' up the ML module system
• Modeling abstract types in modules with open existential types
• System F with coercion constraints
• Type soundness proofs with definitional interpreters

Cited in

(7)

• Fighting bit rot with types (Experience report: Scala collections)
• Soundness conditions for big-step semantics
• Dependent ML An approach to practical programming with dependent types
• Type soundness proofs with definitional interpreters
• A calculus with recursive types, record concatenation and subtyping
• Revisiting decidable bounded quantification, via dinaturality
• A simple blame calculus for explicit nulls

Describes a project that uses

Uses Software

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

This page was built for publication: The essence of dependent object types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3188291)