Publication

A Flow-Insensitive, Modular Effect System for Purity

Related publications (34)

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.

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

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

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

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

Type Soundness for Dependent Object Types (DOT)

Tiark Rompf, Nada Amin

Scala's type system unifies aspects of ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar expressive languages. Unfortunately, ty ...

Assoc Computing Machinery2016

Language Support for Distributed Functional Programming

Software development has taken a fundamental turn. Software today has gone from simple, closed programs running on a single machine, to massively open programs, patching together user experiences byway of responses received via hundreds of network requests ...

EPFL2015

On Counter-Example Complete Verification for Higher-Order Functions

Viktor Kuncak, Etienne Kneuss, Nicolas Charles Yves Voirol

We present a verification procedure for pure higher-order functional Scala programs with parametric types. We show that our procedure is sound for proofs, as well as sound and complete for counter-examples. The procedure reduces the analysis of higher-orde ...

2015

Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution

Martin Odersky, Philipp Haller

Functional programming (FP) is regularly touted as the way forward for bringing parallel, concurrent, and distributed programming to the mainstream. The popularity of the rationale behind this viewpoint (immutable data transformed by function application) ...

2014

Spores, Formally

Philipp Haller

2013

Termination Analysis in a Higher-Order Functional Context

Nicolas Charles Yves Voirol

We start by describing how higher-order function support can be added to a (first order) functional verification framework. We cover both the higher-order construct management and framework extensions necessary for constraint specification. Next, we outlin ...

2013