Publication

The Essence of Dependent Object Types

Related publications (37)

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.

Type-Preserving Compilation of Class-Based Languages

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 ...

EPFL2023

A Mechanized Theory of the Box Calculus

Yichen Xu

Capture calculus is an extension of System Fsub that tracks free variables of terms in their type, allowing one to represent capabilities while limiting their scope. While previous calculi had mechanized soundness proofs, the latest version, namely the box ...

2023

Capturing Types

Martin Odersky, Aleksander Slawomir Boruch-Gruszecki, Ondrej Lhoták

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

New York2023

2022

Type-level programming is becoming more and more popular in the realm of functional programming. However, the combination of type-level programming and subtyping remains largely unexplored in practical programming languages. This paper presents match types ...

ASSOC COMPUTING MACHINERY2022

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

Studies on Types: Dormitories

Tiago André Pratas Borges, Anja Fröhlich, Estelle Lépine, Vanessa Pointet

Concepts of type and typology are not specific to architecture. Rather they represent an interdisciplinary approach to ordering knowledge and gaining insight. In the field of architecture, the study of types and typology offers a didactic perspective that ...

EPFL Press2022

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain, Jonathan Immanuel Brachthäuser

2021

Formal foundations for GADTs in Scala

GADTs are a very useful language feature that allow encoding some invariants in types. GADT reasoning is currently implemented in Scala and Dotty, but it’s plagued with soundness issues. To get a better understanding of GADTs in Scala, we explore how they ...

2020

Integral Convexity And Parabolic Systems

Bernard Dacorogna

In this work we give optimal, i.e., necessary and sufficient, conditions for integrals of the calculus of variations to guarantee the existence of solutions-both weak and variational solutions-to the associated L-2-gradient flow. The initial values are mer ...

SIAM PUBLICATIONS2020