Publication

Type-Preserving Compilation of Class-Based Languages

Abstract

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not enough to declare a particular subset of the language as sound. While a few examples of Scala snippets have been manually translated into DOT, no systematic compilation scheme has been presented so far. In this thesis we develop a series of calculi of increasing complexity to model Scala and present a type-preserving compilation scheme from each of these calculus into DOT. Along the way, we develop some necessary extensions to DOT.

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related concepts (38)
Scala (programming language)
Scala (ˈskɑːlə ) is a strong statically typed high-level general-purpose programming language that supports both object-oriented programming and functional programming. Designed to be concise, many of Scala's design decisions are aimed to address criticisms of Java. Scala source code can be compiled to Java bytecode and run on a Java virtual machine (JVM). Scala can also be compiled to JavaScript to run in a browser, or directly to a native executable.
Language
Language is a structured system of communication that consists of grammar and vocabulary. It is the primary means by which humans convey meaning, both in spoken and written forms, and may also be conveyed through sign languages. The vast majority of human languages have developed writing systems that allow for the recording and preservation of the sounds or signs of language. Human language is characterized by its cultural and historical diversity, with significant variations observed between cultures and across time.
Subtyping
In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutability, meaning that program elements, typically subroutines or functions, written to operate on elements of the supertype can also operate on elements of the subtype. If S is a subtype of T, the subtyping relation (written as S
Show more
Related publications (44)

DFT plus U-type functional derived to explicitly address the flat plane condition

Edward Baxter Linscott

A DFT+U-type corrective functional is derived from first principles to enforce the flat plane condition on localized subspaces, thus dispensing with the need for an ad hoc derivation from the Hubbard model. Small, molecular test systems at the dissociated ...
AMER PHYSICAL SOC2023

Type-preserving compilation of (most of) FGJ into DOT

Guillaume André Fradji Martres

The Dependent Object Type (DOT) calculus was designed to put Scala on a sound basis, but while DOT relies on structural subtyping, Scala is a fundamentally class-based language. This impedance mismatch means that a proof of DOT soundness by itself is not e ...
2022

A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning

Yichen Xu, Lionel Emile Vincent Parreaux, Aleksander Slawomir Boruch-Gruszecki

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies ...
New York2022
Show more
Related MOOCs (16)
Parallelism and Concurrency
(merge of parprog1, scala-reactive, scala-spark-big-data)
Functional Programming
In this course you will discover the elements of the functional programming style and learn how to apply them usefully in your daily programming tasks. You will also develop a solid foundation for rea
Functional Programming Principles in Scala [retired]
This advanced undergraduate programming course covers the principles of functional programming using Scala, including the use of functions as values, recursion, immutability, pattern matching, higher-
Show more

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.