Publication

Scaling Language Features for Program Verification

Related publications (134)

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.

Functional BIP: Embedding connectors in functional programming languages

Romain Edelmann, Joseph Sifakis, Simon Bliudze

This paper presents a theoretical foundation for functional language implementations of Behaviour–Interaction–Priority (BIP). We introduce a set of connector combinators describing synchronisation, data transfer, priorities and dynamicity in a principled w ...

Elsevier Science Inc2017

Higher-Order Subtyping with Type Intervals

Sandro Stucki

Modern, statically typed programming languages provide various abstraction facilities at both the term- and type-level. Common abstraction mechanisms for types include parametric polymorphism -- a hallmark of functional languages -- and subtyping -- which ...

EPFL2017

Dotty Phantom Types

Martin Odersky, Nicolas Alexander Stucki

Phantom types are a well-known type-level, design pattern which is commonly used to express constraints encoded in types. We observe that in modern, multi-paradigm programming languages, these encodings are too restrictive or do not provide the guarantees ...

2017

Interactive Programming by Example

Mikaël Mayer

As of today, programming has never been so accessible. Yet, it remains a challenge for end-users: students, non-technical employees, experts in their domains outside of computer science, and so on. With its forecast potential for solving problems by only o ...

EPFL2017

LMS-Verify: Abstraction without Regret for Verified Systems Programming’

Tiark Rompf, Nada Amin

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because d ...

Assoc Computing Machinery2017

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

Python module for finite rate of innovation (FRI) sampling

Hanjie Pan

Level: BS/MS semester project Description: Sampling signals with finite rate of innovation plays a key in the sucess of continuous domain sparse reconstructions [1], including the direction of arrival estimation (DOA) with a microphone array [2], ...

2017

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

, ,

Implicit parameters are used pervasively in Scala and are also present in a number of other programming and theorem proving languages. This paper describes a generalization of implicit parameters as they are currently found in Scala to implicit function ty ...

2017

Digital technologies are transforming the film industry. Up until roughly a decade ago, the business model for film exhibition was based on theatrical release in combination with television sales and home cinema releases (video and DVD). Recently, many que ...

2017