Publications by Martin Odersky

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.

Performance-critical industrial applications, including large-scale program, network, and distributed system analyses, are increasingly reliant on recursive queries for data analysis. Yet traditional relational algebra-based query optimization techniques d ...

As heterogeneous parallel systems become dominant, application developers are being forced to turn to an incompatible mix of low level programming models (e.g. OpenMP, MPI, CUDA, OpenCL). However, these models do little to shield developers from the difficult problems of parallelization, data decomposition and machine-specific details. Ordinary programmers are having a difficult time using these programming models effectively. To provide a programming model that addresses the productivity and performance re

State-of-the-art immutable collections have wildly differing performance characteristics across their operations, often forcing programmers to choose different collection implementations for each task. Thus, changes to the program can invalidate the choice ...

Pattern matching makes ML programs more concise and readable, and these qualities are also sought in object-oriented settings. However, objects and classes come with open class hierarchies, extensibility requirements and the need for data abstraction, which all conflict with matching on concrete data types. Extractor-based pattern matching has been proposed to address this conflict. Extractors are user-defined methods that perform the task of value discrimination and deconstruction during pattern matching.

In metaprogramming, code generation and code analysis are complementary. Traditionally, principled metaprogramming extensions for programming languages, like MetaML and BER MetaOCaml, offer strong foundations for code generation but lack equivalent support for code analysis. Similarly, existing macro systems are biased towards the code generation aspect. In this work, we present a calculus for macros featuring both code generation and code analysis. The calculus directly models separate compilation of macro

This article describes the design and implementation of named and default arguments in the Scala programming language. While these features are available in many other languages there are significant differences in the actual implementations. We present a ...

We design and study newObj, a calculus and dependent type system for objects and classes which can have types as members. Type members can be aliases, abstract types, or new types. The type system can model the essential concepts of Java's inner classes as well as virtual types and family polymorphism found in BETA or gbeta. It can also model most concepts of SML-style module systems, including sharing constraints and higher-order functors, but excluding applicative functors. The type system can thus be use

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 \emph{match types}, a type-level equivalent of pattern matching. Match types integrate seamlessly into programming languages with subtyping and, despite their simplicity, offer significant additional expressiveness. We formalize the feature of match types in a calcul

Transactions are commonly described as being ACID: All-or-nothing, Consistent, Isolated and Durable. However, although these words convey a powerful intuition, the ACID properties have never been given a precise semantics in a way that disentangles each property from the others. Among the benefits of such a semantics would be the ability to trade-off the value of a property against the cost of its implementation. This paper gives a sound equational semantics for the transaction properties. We define three c

Developing high-performance software is a difficult task that requires the use of low-level, architecture-specific programming models (e.g., OpenMP for CMPs, CUDA for GPUs, MPI for clusters). It is typically not possible to write a single application that ...

Most applications manipulate structured data. Modern languages and platforms provide collection frameworks with basic data structures like lists, hashtables and trees. These data structures come with a range of predefined operations which include sorting, filtering or finding elements. Such bulk operations usually traverse the entire collection and process the elements sequentially. Their implementation often relies on iterators, which are not applicable to parallel operations due to their sequential nature

Implicit parameters are used pervasively in Scala and are also present in a number of other programming and theorem proving languages. This paper describes a generalization of implicit parameters as they are currently found in Scala to implicit function types. We motivate the construct by a series of examples and provide formal foundations that closely follow the semantics implemented by the Scala compiler.

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

Pattern matching enables inspecting algebraic data types, but typically prevents hiding the implementation of the matched algebraic data type. In Scala, instead, extractors also allow pattern matching on non-algebraic data types and invoking methods on the ...

This document proposes a new serialization format for typed syntax trees of Scala programs. It aims to be ● compact: All numbers and references are length encoded, trees are inlined by default but may be shared. ● lazy: Trees can be explored from the top, and one can suspend reading subtrees at any time. The only section that needs to be scanned in full is the name table. Laziness is important for the compiler frontend as most of the information in a TASTY file is not needed then. ● extensible: New sections

We describe the implementation of first-class polymorphic delimited continuations in the programming language Scala. We use Scala's pluggable typing architecture to implement a simple type and effect system, which discriminates expressions with control eff ...

Claude Shannon, in his famous thesis (1938), revolutionized circuit design by showing that Boolean algebra subsumes all ad-hoc methods that are used in designing switching circuits, or combinational circuits as they are commonly known today. But what is the calculus for sequential circuits? Finite-state machines (FSM) are close, but not quite, as they do not support arbitrary parallel and hierarchical composition like that of Boolean expressions. We propose an abstraction called implicit state machine (

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 constructor via \emph{this}, has to observe the initialization states of the object for correctness, i.e.~only initialized fields may be used. Checking safe usage of \emph{this} statically, without manual annotation of initialization states in source code, is

Production compilers commonly perform dozens of transformations on an intermediate representation. Running those transformations in separate passes harms performance. One approach to recover performance is to combine transformations by hand in order to red ...

Martin Odersky

Chat with Graph Search

Adaptive Recursive Query Optimization

Language Virtualization for Heterogeneous Parallel Computing

RRB Vector: A Practical General Purpose Immutable Sequence

Translation Correctness for First-Order Object-Oriented Pattern Matching

Proof of Multi-Stage Programming with Generative and Analytical Macros

Named and default arguments for polymorphic object-oriented languages

A Nominal Theory of Objects with Dependent Types

Type-Level Programming with Match Types

An Equational Theory for Transactions

Delite: A Compiler Architecture for Performance-Oriented Embedded Domain-Specific Languages

An Equational Theory for Transactions

A Generic Parallel Collection Framework

Foundations of Implicit Function Types

Degrees of Separation: A Flexible Type System for Safe Concurrency

Truly abstract interfaces for algebraic data types: the extractor typing problem

A TASTY Alternative

Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform

Digital Design with Implicit State Machines

A Type-and-Effect System for Object Initialization

Miniphases: Compilation using Modular and Efficient Tree Transformations