Concept

Boilerplate code

Publications associées (27)

Semantics-preserving inlining for metaprogramming

Martin Odersky, Sébastien Jean R Doeraene, Nicolas Alexander Stucki

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

Aleksandar Prokopec, Fengyun Liu

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

Termination of Open Higher-Order Programs

Viktor Kuncak, Nicolas Charles Yves Voirol, Ravichandhran Kandhadai Madhavan

We study the problem of proving termination of open, higher-order programs with recursive functions and datatypes. We identify a new point in the design space of solutions, with an appealing trade-off between simplicity of specification, modularity, and am ...

2017

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

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

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

Building Efficient Query Engines in a High-Level Language

Christoph Koch, Ioannis Klonatos, Amir Shaikhha

Abstraction without regret refers to the vision of using high-level programming languages for systems development without experiencing a negative impact on performance. A database system designed according to this vision offers both increased productivity ...

2016

Verifying Resource Bounds of Programs with Lazy Evaluation and Memoization

Viktor Kuncak, Ravichandhran Kandhadai Madhavan, Sumith Kulal

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

2016

Modular interface for embedded audio acquisition platforms

Basile Gérard Pierre Bruneau

In this project, I developed a browser based interface for prototyping real-time processing algorithms using embedded multi channel audio acquisition platforms. The interface allows to interact in an easy manner with a GNU/Linux enabled single board comput ...

2016

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