Publication

On Proving and Disproving Equivalence of Functional Programming Assignments

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

Constraints as Control

Viktor Kuncak, Philippe Paul Henri Suter

We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates con ...

ACM Order Department, P O Box 64145, Baltimore, MD 21264 Usa2012

Verification of Imperative Programs in Scala

Régis William Blanc

Safety-critical software systems can only support a limited number of failures. Extensive testing is good at catching errors, however that will never certify their absence. Formal verification is an alternative to testing that can (automatically) provide a ...

2012

Software Synthesis Procedures

Viktor Kuncak, Mikaël Mayer, Philippe Paul Henri Suter, Ruzica Piskac

Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succ ...

2012

Deprecating the Observer Pattern with Scala.React

Martin Odersky, Ingo Maier

Programming interactive systems by means of the observer pattern is hard and error-prone yet is still the implementation standard in many production environments. We show how to integrate different reactive programming abstractions into a single framework ...

2012

A Programming Workshop using the Robot "Thymio II": The Effect on the Understanding by Children

Francesco Mondada, Michael Bonani, Stéphane Magnenat, Fanny Riedo

Robots are both fascinating objects for the general public and devices whose conception, understanding and pro- gramming involve many fields. This unique combination makes them an ideal tool for introducing science and technology to children. This paper pr ...

IEEE2012

On Interactive Synthesis of Code Snippets

Viktor Kuncak, Tihomir Gvero, Ruzica Piskac

We describe a tool that applies theorem proving technology to synthesize code fragments that use given library functions. Our approach takes into account polymorphic type constraints as well as code behavior. We have found our system to be useful for synth ...

2011

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

Deprecating the Observer Pattern

Martin Odersky, Tiark Rompf, Ingo Maier

Programming interactive systems by means of the observer pattern is hard and error-prone yet is still the implementation standard in many production environments. We present an approach to gradually deprecate observers in favor of reactive programming abst ...

2010

Programming with Undo

Ersoy Bayramoglu

This thesis is about objects that can undo their state changes. Based on an earlier work on data structure persistence, we propose generating undo methods for classes from annotated classes automatically. As opposed to ephemeral data structures, persistent ...

2009

A Probabilistic Programming by Demonstration Framework Handling Constraints in Joint Space and Task Space

Aude Billard, Sylvain Calinon

We present a probabilistic architecture for solving generically the problem of extracting the task constraints through a Programming by Demonstration (PbD) framework and for generalizing the acquired knowledge to various situations. We propose an approach ...

2008