Publication

On Verification by Translation to Recursive Functions

Publications associées (34)

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

Quasiquotes for Scala

Martin Odersky, Eugene Burmako, Denys Shabalin

We introduce quasiquotes for the Scala programming language, which solve the problem of manual tree construction and deconstruction. Included case studies show that quasiquotes indeed are easier to work with than existing tools for tree construction. When ...

2013

Lightweight Polymorphic Effects

Martin Odersky, Philipp Haller, Lukas Rytz

Type-and-effect systems are a well-studied approach for reasoning about the computational behavior of programs. Nevertheless, there is only one example of an effect system that has been adopted in a wide-spread industrial language: Java’s checked exception ...

Springer-Verlag2012

Scala Macros, a Technical Report

Martin Odersky, Eugene Burmako

Metaprogramming is a powerful technique of software development, which allows to automate program generation. Applications of metaprogramming range from improving expressiveness of a programming language via deep embedding of domain-specific languages to b ...

2012

Satisfiability Modulo Recursive Programs

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, a subset of Scala. We impl ...

Springer-Verlag Berlin2011

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

On Satisfiability Modulo Computable Functions

Viktor Kuncak, Philippe Paul Henri Suter, Ali Sinan Köksal

We present a semi-decision procedure for checking satisfiability of formulas in the language of algebraic data types and integer linear arithmetic extended with user-defined terminating recursive functions. Our procedure is designed to integrate into a DPL ...

2010

Compiling Scala for Performance

Iulian Dragos

Scala is a new programming language bringing together object-oriented and functional programming. Its defining features are uniformity and extensibility. Scala offers great flexibility for programmers, allowing them to grow the language through libraries. ...

EPFL2010

Named and default arguments for polymorphic object-oriented languages

Martin Odersky, Lukas Rytz

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

ACM2010

State Exploration of Scala Actor Programs

Mirco Dotta

The growing use of multicore and networked computing systems is increasing the importance of developing reliable parallel and distributed code. Unfortunately, developing and testing such code is notoriously hard, especially for shared-memory models of prog ...

2009

Programming language abstractions for mobile code

Stéphane Micheloud

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