Publication

Abstractions for Type-Level Programming

Publications associées (46)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Developers write low-level systems code in unsafe programming languages due to performance concerns. The lack of safety causes bugs and vulnerabilities that safe languages avoid. We argue that safety without run-time overhead is possible through type invar ...

IEEE COMPUTER SOC2023

Type-Level Programming with Match Types

Martin Odersky, Olivier Eric Paul Blanvillain

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

Type-Level Programming with Match Types

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

2021

Enclosure: Language-Based Restriction of Untrusted Libraries

James Richard Larus, Mathias Josef Payer, Edouard Bugnion, Evangelos Marios Kogias, Adrien Ghosn

Programming languages and systems have failed to address the security implications of the increasingly frequent use of public libraries to construct modern software. Most languages provide tools and online repositories to publish, import, and use libraries ...

2021

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Lionel Emile Vincent Parreaux

Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various impl ...

EPFL2020

Safe Initialization of Objects

Martin Odersky, Fengyun Liu, Paolo Giosuè Giarrusso, Ondrej Lhoták

Every newly created object goes through several initialization states: starting from a state where all fields are uninitialized until all of them are assigned. Any operation on the object during its initialization process, which usually happens in the cons ...

2020

A Type-and-Effect System for Object Initialization

Martin Odersky, Fengyun Liu, Paolo Giosuè Giarrusso, Ondrej Lhoták

ASSOC COMPUTING MACHINERY2020

Verified Functional Programming

Nicolas Charles Yves Voirol

In this thesis, we present Stainless, a verification system for an expressive subset of the Scala language. Our system is based on a dependently-typed language and an algorithmic type checking procedure which ensures total correctness. We rely on SMT solve ...

EPFL2019

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

EPFL2018