Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Boilerplate code

Publications associées (14)

Semantics-preserving inlining for metaprogramming

Martin Odersky, Nicolas Alexander Stucki, Sébastien Jean Robert Doeraene, Angelos Bimpoudis

Inlining is used in many different ways in programming languages: some languages use it as a compiler-directive solely for optimization, some use it as a metaprogramming feature, and others lay their design in-between. This paper presents inlining through ...

2020

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

Secured Routines: Language-based Construction of Trusted Execution Environments

James Richard Larus, Edouard Bugnion, Adrien Ghosn

Trusted Execution Environments (TEEs), such as Intel SGX enclaves, use hardware to ensure the confidentiality and integrity of operations on sensitive data. While the technology is available on many processors, the complexity of its programming model and i ...

USENIX ASSOC2019

Theory and Practice of Coroutines with Snapshots

Fengyun Liu, Aleksandar Prokopec

While event-driven programming is a widespread model for asynchronous computing, its inherent control flow fragmentation makes event-driven programs notoriously difficult to understand and maintain. Coroutines are a general control flow construct that can ...

2018

Unifying Analytic and Statically-Typed Quasiquotes

Christoph Koch, Amir Shaikhha, Lionel Emile Vincent Parreaux

Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by quasiquotation, a technique to construct and deconstruct program fragments using quoted code templates expressed in the syntax ...

2018

Contract-Based Resource Verification for Higher-Order Functions with Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. a ...

Assoc Computing Machinery2017

IT Service Alignment Verification of Quantitative Properties in Service Design

Alain Wegmann, Gorica Tapandjieva Sekulovska

Despite many years of research, alignment of business and IT services remains a challenge. In this paper we show how to verify the quantitative properties of a service against stakeholder requirements during service design. We model the service with the Sy ...

2015

Functional Pearl: A SQL to C Compiler in 500 Lines of Code

Tiark Rompf, Nada Amin

We present the design and implementation of a SQL query processor that outperforms existing database systems and is written in just about 500 lines of Scala code - a convincing case study that high-level functional programming can handily beat C for system ...

Assoc Computing Machinery2015

Building Efficient Query Engines in a High-Level Language

Christoph Koch, Tiark Rompf, Ioannis Klonatos

In this paper we advocate that it is time for a radical rethinking of database systems design. Developers should be able to leverage high-level programming languages without having to pay a price in efficiency. To realize our vision of abstraction without ...

2014

Forge: Generating a High Performance DSL Implementation from a Declarative Specification

Martin Odersky, Tiark Rompf

Domain-specific languages provide a promising path to automatically compile high-level code to parallel, heterogeneous, and distributed hardware. However, in practice high performance DSLs still require considerable software expertise to develop and force ...

Assoc Computing Machinery2014

Spiral in Scala: Towards the Systematic Construction of Generators for Performance Libraries

Martin Odersky, Tiark Rompf

Program generators for high performance libraries are an appealing solution to the recurring problem of porting and optimizing code with every new processor generation, but only few such generators exist to date. This is due to not only the difficulty of t ...

Assoc Computing Machinery2014

Scala to the Power of Z3: Integrating SMT and Programming

Viktor Kuncak, Philippe Paul Henri Suter

We describe a system that integrates the SMT solver Z3 with the Scala programming language. The system supports the use of the SMT solver for checking satisfiability, unsatisfiability, as well as solution enumeration. The embedding of formula trees into Sc ...

Springer-Verlag Berlin2011

Programming language abstractions for mobile code

Scala is a general-purpose programming language developed at EPFL. It combines the most important concepts found in object-oriented and functional languages. Scala is a statically typed language; in particular it features an advanced type system and suppor ...

EPFL2009

A typed intermediate language and algorithms for compiling scala by successive rewritings

Philippe Altherr

Scala is a general-purpose programming language developed at EPFL. It combines concepts coming from object-oriented languages with other ones coming from functional languages. Scala is strongly typed and comes with a relatively complex type system, which i ...

EPFL2006