Publication

Decrypting Local Type Inference

Related publications (147)

Graph Chatbot

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.

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 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 Rigorous Numerical Computation as a Scala Library

Viktor Kuncak, Eva Darulova

Modern programming languages have adopted the floating point type as a way to describe computations with real numbers. Thanks to the hardware support, such computations are efficient on modern architectures. However, rigorous reasoning about the resulting ...

2010

Type Classes as Objects and Implicits

Martin Odersky

Type classes were originally developed in Haskell as a disciplined alternative to ad-hoc polymorphism. Type classes have been shown to provide a type-safe solution to important challenges in software engineering and programming languages such as, for examp ...

ACM2010

Improving API Documentation for Java-like Languages

Gilles Dubochet, Donna Malayeri

The Javadoc paradigm for displaying API documentation to users is quite popular, with similar variants existing for many mainstream languages. However, two user interface design properties of Javadoc may reduce its utility when displaying documentation for ...

2010

Phantm: PHP Analyzer for Type Mismatch

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

We present Phantm, a static analyzer that uses a flow-sensitive analysis to detect type errors in PHP applications. Phantm can infer types for nested arrays, and can leverage runtime information and procedure summaries for more precise results. Phantm foun ...

2010

Phantm: PHP analyzer for type mismatch

Viktor Kuncak, Etienne Kneuss, Philippe Paul Henri Suter

2010

Capabilities for Uniqueness and Borrowing

Martin Odersky, Philipp Haller

An important application of unique object references is safe and efficient message passing in concurrent object-oriented programming. However, to prevent the ill effects of aliasing, practical systems often severely restrict the shape of messages passed by ...

Springer2010

Precise static analysis of untrusted driver binaries

Johannes Kinder

Most closed source drivers installed on desktop systems today have never been exposed to formal analysis. Without vendor support, the only way to make these often hastily written, yet critical programs accessible to static analysis is to directly work at t ...

IEEE2010

Modelling the influence of human behaviour on the spread of infectious diseases: a review

Marcel Salathé

Human behaviour plays an important role in the spread of infectious diseases, and understanding the influence of behaviour on the spread of diseases can be key to improving control efforts. While behavioural responses to the spread of a disease have often ...

2010