Publication
Type-Preserving Compilation of Class-Based Languages
Related publications (44)
DFT plus U-type functional derived to explicitly address the flat plane condition
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 SOC2023Type-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 ...
2022A 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 York2022What is Trending on Wikipedia? Capturing Trends and Language Biases Across Wikipedia Editions
Pierre Vandergheynst, Nicolas Aspert, Volodymyr Miz, Benjamin Ricaud, Joëlle Hanna
In this work, we propose an automatic evaluation and comparison of the browsing behavior of Wikipedia readers that can be applied to any language editions of Wikipedia. As an example, we focus on English, French, and Russian languages during the last four ...
ACM2020Cross-Platform Language Design
Programming languages are increasingly compiled to multiple runtimes, each featuring their own rich structures such as their object model.
Furthermore, they need to interact with other languages targeting said runtimes.
A language targeting only one runtim ...
EPFL2018Negentropic linguistic evolution: A comparison of seven languages
Frédéric Kaplan, Vincent Christian Buntinx
The relationship between the entropy of language and its complexity has been the subject of much speculation – some seeing the increase of linguistic entropy as a sign of linguistic complexification or interpreting entropy drop as a marker of greater regul ...
2018Corpora Delicti
CORPORA DELICTI, The Significant Detail. The Corpus Delicti is the evidence of a crime. The term denotes the formation of a proof that allows the unmasking of a perpetrator. In the realm of interpretation and language, it could reveal matter on which an ac ...
MANSLAB2017Higher-Order Subtyping with Type Intervals
Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...
EPFL2017Design and implementation of an optimizing type-centric compiler for a high-level language
Production compilers for programming languages face multiple requirements. They should be correct, as we rely on them to produce code. They should be fast, in order to provide a good developer experience. They should also be easy to maintain and evolve. Th ...
EPFL2017Verification by Reduction to Functional Programs
In this thesis, we explore techniques for the development and verification of programs in a high-level, expressive, and safe programming language. Our programs can express problems over unbounded domains and over recursive and mutable data structures. We p ...
EPFL2017