Monotonicity Types for Distributed Dataflow

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.

Type systems are a device for verifying properties of programs without running them. Many programming languages used in the industry have always had a type system, while others were initially created without a type system and later adopted one, when the ad ...

Data races have long been a notorious problem in concurrent programming. They are subtle to detect, and lead to non-deterministic behaviours. There has been a lot of interest in type systems that statically guarantee data race freedom. Significant progress ...

Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CC

Writing and optimizing application software for heterogeneous platforms including GPU units is a very difficult task that requires designer efforts and resources to consider several key elements to obtain good performance. Dataflow programming has shown to ...

MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new development. However, its specification in terms of biunification is difficult to understand, relying on the new concepts of bi ...

Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. High-level languages tend to greatly improve safety, productivity, and code maintainability because they handle various impl ...

In the face of the increasing trend in application development to interact with more and more remote services, and cognizant of the fact that issues arising from data consistency and task coordination are core challenges in distributed programming, the sys ...

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

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

We present short programs that demonstrate the unsoundness of Java and Scala's current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down) casting. Fortunately, parame ...

We present qualified types for Scala, a form of refinement types adapted to the Scala language. Qualified types allow users to refine base types and classes using predicate expressions. We implemented a type checker for qualified types that is embedded in ...

The celebrated distributed computing approach for building systems and services using multiple machines continues to expand to new domains. Computation devices nowadays have additional sensing and communication capabilities, while becoming, at the same tim ...

The most successful systems for “big data” processing have all adopted functional APIs. We present a new programming model we call function passing designed to provide a more principled substrate on which to build data-centric distributed systems. A key id ...

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

To maximize run-time performance, programmers often specialize their code by hand, replacing library collections and containers by custom objects in which data is restructured for efficient access. However, changing the data representation is a tedious and ...

We present short programs that demonstrate the unsoundness of Java and Scala’s current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, paramet ...

High-level languages allow programmers to express data structures and algorithms that abstract over the type of data they handle. This improves code reuse and makes it possible to develop general-purpose libraries. Yet, data abstractions slow down program ...

Programming systems incorporating aspects of functional programming, e.g., higher-order func- tions, are becoming increasingly popular for large-scale distributed programming. New frameworks such as Apache Spark leverage functional techniques to provide hi ...

The actor model has been a model of choice for building reliable distributed systems. On one hand, it ensures that message-processing is serialized within each actor, preserving the familiar sequential programming model. On the other hand, programs written ...

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

Monotonicity Types for Distributed Dataflow

Chat with Graph Search

Formal Foundations of Capture Tracking

Degrees of Separation: A Flexible Type System for Safe Concurrency

Capturing Types

SIMD Parallel Execution on GPU from High-Level Dataflow Synthesis

The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy

Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages

Monotonicity Types

Type Soundness Proofs with Definitional Interpreters

Higher-Order Subtyping with Type Intervals

Java and Scala's Type Systems are Unsound The Existential Crisis of Null Pointers

SMT-Based Checking of Predicate-Qualified Types for Scala

Reliable and Real-Time Distributed Abstractions

Function Passing: A Model for Typed, Distributed Functional Programming

Language Support for Distributed Functional Programming

Automating Ad hoc Data Representation Transformations

Java and Scala's Type Systems are Unsound: The Existential Crisis of Null Pointers

Compile-Time Type-Driven Data Representation Transformations in Object-Oriented Languages

Distributed Programming via Safe Closure Passing

Isolates, channels, and event streams for composable distributed programming

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