Latest in

total 2367took 0.24s
Putting in All the Stops: Execution Control for JavaScriptFeb 08 2018Scores of compilers produce JavaScript, enabling programmers to use many languages on the Web, reuse existing code, and even use Web IDEs. Unfortunately, most compilers expose the browser's compromised execution model, so long-running programs freeze ... More
A Separation Logic for Concurrent Randomized ProgramsFeb 08 2018We present a concurrent separation logic with support for probabilistic reasoning. As part of our logic, we extend the idea of coupling, which underlies recent work on probabilistic relational logics, to the setting of programs with both probabilistic ... More
Classical Higher-Order ProcessesFeb 08 2018Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session types ... More
Recent Advances in Neural Program SynthesisFeb 07 2018In recent years, deep learning has made tremendous progress in a number of fields that were previously out of reach for artificial intelligence. The successes in these problems has led researchers to consider the possibilities for intelligent systems ... More
Axiomatic Foundations and Algorithms for Deciding Semantic Equivalences of SQL QueriesFeb 06 2018Deciding the equivalence of SQL queries is a fundamental problem in data management. As prior work has mainly focused on studying the theoretical limitations of the problem, very few implementations for checking such equivalences exist. In this paper, ... More
Code Reuse With Transformation ObjectsFeb 06 2018We present an approach for a lightweight datatype-generic programming in Objective Caml programming language aimed at better code reuse. We show, that a large class of transformations usually expressed via recursive functions with pattern matching can ... More
Causal Linearizability: Compositionality for Partially Ordered ExecutionsFeb 06 2018In the interleaving model of concurrency, where events are totally ordered, linearizability is compositional: the composition of two linearizable objects is guaranteed to be linearizable. However, linearizability is not compositional when events are only ... More
Demand-driven Alias Analysis : Formalizing Bidirectional Analyses for Soundness and PrecisionFeb 03 2018A demand-driven approach to program analysis have been viewed as efficient algorithms to compute only the information required to serve a target demand. In contrast, an exhaustive approach computes all information in anticipation of it being used later. ... More
When Good Components Go Bad: Formally Secure Compilation Despite Dynamic CompromiseFeb 02 2018We propose a new formal criterion for secure compilation, giving strong end-to-end security guarantees for software components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model_dynamic_ compromise ... More
Generalized Points-to Graphs: A New Abstraction of Memory in the Presence of PointersJan 28 2018Flow- and context-sensitive points-to analysis is difficult to scale; for top-down approaches, the problem centers on repeated analysis of the same procedure; for bottom-up approaches, the abstractions used to represent procedure summaries have not scaled ... More
Modeling of languages for tensor manipulationJan 26 2018Numerical applications and, more recently, machine learning applications rely on high-dimensional data that is typically organized into multi-dimensional tensors. Many existing frameworks, libraries, and domain-specific languages support the development ... More
Reasoning about effects: from lists to cyber-physical agentsJan 24 2018Theories for reasoning about programs with effects initially focused on basic manipulation of lists and other mutable data. The next challenge was to consider higher-order programming, adding functions as first class objects to mutable data. Reasoning ... More
Finitary-based Domain Theory in Coq: An Early ReportJan 17 2018In domain theory every finite computable object can be represented by a single mathematical object instead of a set of objects, using the notion of finitary-basis. In this article we report on our effort to formalize domain theory in Coq in terms of finitary-basis. ... More
Introspection for C and its Applications to Library RobustnessDec 04 2017Context: In C, low-level errors, such as buffer overflow and use-after-free, are a major problem, as they cause security vulnerabilities and hard-to-find bugs. C lacks automatic checks, and programmers cannot apply defensive programming techniques because ... More
Declarativeness: the work done by something elseNov 25 2017Being declarative means that we do computer programming on higher levels of abstraction. This vague definition identifies declarativeness with the act of ignoring details, but it is a special case of abstraction. The unspecified part is some computational ... More
Real-time Stream-based MonitoringNov 10 2017We introduce RTLola, a new stream-based specification language for the description of real-time properties of reactive systems. In real-time applications, data arrives at varying rates and in most cases it is hard to predict the input rate. The integration ... More
Linear Haskell: practical linearity in a higher-order polymorphic languageOct 26 2017Nov 08 2017Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind: backwards-compatibility ... More
MatchPy: A Pattern Matching LibraryOct 16 2017Pattern matching is a powerful tool for symbolic computations, based on the well-defined theory of term rewriting systems. Application domains include algebraic expressions, abstract syntax trees, and XML and JSON data. Unfortunately, no lightweight implementation ... More
Causality-based Model CheckingOct 10 2017Model checking is usually based on a comprehensive traversal of the state space. Causality-based model checking is a radically different approach that instead analyzes the cause-effect relationships in a program. We give an overview on a new class of ... More
Efficient Pattern Matching in PythonSep 29 2017Pattern matching is a powerful tool for symbolic computations. Applications include term rewriting systems, as well as the manipulation of symbolic expressions, abstract syntax trees, and XML and JSON data. It also allows for an intuitive description ... More
Variant-Based Decidable Satisfiability in Initial Algebras with PredicatesSep 15 2017Decision procedures can be either theory-specific, e.g., Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the ... More
Abstractness, specificity, and complexity in software designSep 05 2017Abstraction is one of the fundamental concepts of software design. Consequently, the determination of an appropriate abstraction level for the multitude of artefacts that form a software system is an integral part of software engineering. However, the ... More
A Verified Compiler for Probability Density FunctionsJul 21 2017Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language ... More
Exploiting Term Hiding to Reduce Run-time Checking OverheadMay 18 2017Oct 16 2017One of the most attractive features of untyped languages is the flexibility in term creation and manipulation. However, with such power comes the responsibility of ensuring the correctness of these operations. A solution is adding run-time checks to the ... More
Microservices: a Language-based ApproachApr 26 2017Microservices is an emerging development paradigm where software is obtained by composing autonomous entities, called (micro)services. However, microservice systems are currently developed using general-purpose programming languages that do not provide ... More
Scaling Reliably: Improving the Scalability of the Erlang Distributed Actor PlatformApr 24 2017May 08 2017Distributed actor languages are an effective means of constructing scalable reliable systems, and the Erlang programming language has a well-established and influential model. While Erlang model conceptually provides reliable scalability, it has some ... More
The pragmatics of clone detection and eliminationMar 31 2017The occurrence of similar code, or `code clones', can make program code difficult to read, modify and maintain. This paper describes industrial case studies of clone detection and elimination using a refactoring and clone detection tool. We discuss how ... More
Verified type checker for Jolie programming languageMar 15 2017Mar 23 2017Jolie is a service-oriented programming language which comes with the formal specification of its type system. However, there is no tool to ensure that programs in Jolie are well-typed. In this paper we provide the results of building a type checker for ... More
Designing a pi-based Programming Language in the .NET framework: CLR interoperability from the Programmer's point of viewMar 15 2017Interoperability is the ability of a programming language to work with systems based on different languages and paradigms. These days, many widely used high-level language impementations provide access to external functionalities. In this paper, we present ... More
Jolie Static Type Checker: a prototypeFeb 23 2017Oct 18 2017Static verification of a program source code correctness is an important element of software reliability. Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Many languages use both ... More
Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all ModelsFeb 22 2017Apr 28 2017We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ... More
Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural CodeJan 25 2017The current trends in next-generation exascale systems go towards integrating a wide range of specialized (co-)processors into traditional supercomputers. Due to the efficiency of heterogeneous systems in terms of Watts and FLOPS per surface unit, opening ... More
Towards a Semantics-Aware Code Transformation Toolchain for Heterogeneous SystemsJan 12 2017Obtaining good performance when programming heterogeneous computing platforms poses significant challenges. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code with semantic annotations ... More
Self-composable ProgrammingDec 08 2016Increasing scale and complexity of modern software, we have found programming problem with techniques like Aspect-oriented Programming(AOP) while constructing features of the software. We capture its key property as behavioral similarity, a set of tangled ... More
Type Annotation for Adaptive SystemsDec 06 2016We introduce type annotations as a flexible typing mechanism for graph systems and discuss their advantages with respect to classical typing based on graph morphisms. In this approach the type system is incorporated with the graph and elements can adapt ... More
Building Code with Dynamic StagingDec 05 2016When creating a new domain-specific language (DSL) it is common to embed it as a part of a flexible host language, rather than creating it entirely from scratch. The semantics of an embedded DSL (EDSL) is either given directly as a set of functions (shallow ... More
From signatures to monads in UniMathDec 02 2016The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The system is kept ... More
How Are Programs Found? Speculating About Language Ergonomics With Curry-HowardDec 02 2016Functional languages with strong static type systems have beneficial properties to help ensure program correctness and reliability. Surprisingly, their practical significance in applications is low relative to other languages lacking in those dimensions. ... More
Transaction-based Sandboxing for JavaScriptDec 02 2016Today's JavaScript applications are composed of scripts from different origins that are loaded at run time. As not all of these origins are equally trusted, the execution of these scripts should be isolated from one another. However, some scripts must ... More
Dynamic Structural Operational SemanticsDec 02 2016We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The ... More
Sparsity Preserving Algorithms for OctagonsDec 01 2016Known algorithms for manipulating octagons do not preserve their sparsity, leading typically to quadratic or cubic time and space complexities even if no relation among variables is known when they are all bounded. In this paper, we present new algorithms, ... More
Revisiting the Futamura Projections: A Visual TutorialNov 29 2016Partial evaluation, while powerful, is not widely studied or used by the pragmatic programmer. To address this, we revisit the Futamura Projections from a visual perspective by introducing a diagramming scheme that helps the reader navigate the complexity ... More
Formal Languages, Formally and CoinductivelyNov 29 2016Traditionally, formal languages are defined as sets of words. More recently, the alternative coalgebraic or coinductive representation as infinite tries, i.e., prefix trees branching over the alphabet, has been used to obtain compact and elegant proofs ... More
Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt GenerationNov 29 2016We present sound and complete environmental bisimilarities for a variant of Dybvig et al.'s calculus of multi-prompted delimited-control operators with dynamic prompt generation. The reasoning principles that we obtain generalize and advance the existing ... More
An Inductive Proof Method for Simulation-based Compiler CorrectnessNov 29 2016We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The proof method relies ... More
Domain-Specific Languages of Mathematics: Presenting Mathematical Analysis Using Functional ProgrammingNov 29 2016We present the approach underlying a course on "Domain-Specific Languages of Mathematics", currently being developed at Chalmers in response to difficulties faced by third-year students in learning and applying classical mathematics (mainly real and complex ... More
Proust: A Nano Proof AssistantNov 29 2016Proust is a small Racket program offering rudimentary interactive assistance in the development of verified proofs for propositional and predicate logic. It is constructed in stages, some of which are done by students before using it to complete proof ... More
The Bricklayer Ecosystem - Art, Math, and CodeNov 29 2016This paper describes the Bricklayer Ecosystem - a freely-available online educational ecosystem created for people of all ages and coding backgrounds. Bricklayer is designed in accordance with a "low-threshold infinite ceiling" philosophy and has been ... More
Learn Quantum Mechanics with HaskellNov 29 2016To learn quantum mechanics, one must become adept in the use of various mathematical structures that make up the theory; one must also become familiar with some basic laboratory experiments that the theory is designed to explain. The laboratory ideas ... More
Teaching Functional Patterns through Robotic ApplicationsNov 29 2016We present our approach to teaching functional programming to First Year Computer Science students at Middlesex University through projects in robotics. A holistic approach is taken to the curriculum, emphasising the connections between different subject ... More
Do be do be doNov 28 2016We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar's effect handler abstraction. Effect handlers ... More
Dynamic Choreographies: Theory And ImplementationNov 28 2016Dec 01 2016Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, ... More
Dynamic Choreographies: Theory And ImplementationNov 28 2016Programming distributed applications free from communication deadlocks and race conditions is complex. Preserving these properties when applications are updated at runtime is even harder. We present a choreographic approach for programming updatable, ... More
Propositions in Linear Multirole Logic as Multiparty Session TypesNov 27 2016We identify multirole logic as a new form of logic and formalize linear multirole logic (LMRL) as a natural generalization of classical linear logic (CLL). Among various meta-properties established for LMRL, we obtain one named multi-cut elimination stating ... More
Proceedings of the 4th and 5th International Workshop on Trends in Functional Programming in EducationNov 26 2016This volume contains the proceedings of the Fourth and Fifth International Workshops on Trends in Functional Programming in Education, TFPIE 2015 and TFPIE 2016, which were held on June 2, 2015 in Sophia-Antipolis, France, and on June 7, 2016 at the University ... More
On the Relationship of Inconsistent Software Clones and Faults: An Empirical StudyNov 23 2016Background: Code cloning - copying and reusing pieces of source code - is a common phenomenon in software development in practice. There have been several empirical studies on the effects of cloning, but there are contradictory results regarding the connection ... More
At Ease with Your Warnings: The Principles of the Salutogenesis Model Applied to Automatic Static AnalysisNov 23 2016The results of an automatic static analysis run can be overwhelming, especially for beginners. The overflow of information and the resulting need for many decisions is mentally tiring and can cause stress symptoms. There are several models in health care ... More
Browsix: Bridging the Gap Between Unix and the BrowserNov 23 2016Applications written to run on conventional operating systems typically depend on OS abstractions like processes, pipes, signals, sockets, and a shared file system. Porting these applications to the web currently requires extensive rewriting or hosting ... More
Approaching Symbolic Parallelization by Synthesis of Recurrence DecompositionsNov 23 2016We present GraSSP, a novel approach to perform automated parallelization relying on recent advances in formal verification and synthesis. GraSSP augments an existing sequential program with an additional functionality to decompose data dependencies in ... More
Developing a Practical Reactive Synthesis Tool: Experience and Lessons LearnedNov 23 2016We summarise our experience developing and using Termite, the first reactive synthesis tool intended for use by software development practitioners. We identify the main barriers to making reactive synthesis accessible to software developers and describe ... More
Leveraging Parallel Data Processing Frameworks with Verified LiftingNov 23 2016Many parallel data frameworks have been proposed in recent years that let sequential programs access parallel processing. To capitalize on the benefits of such frameworks, existing code must often be rewritten to the domain-specific languages that each ... More
Using SyGuS to Synthesize Reactive Motion PlansNov 23 2016We present an approach for synthesizing reactive robot motion plans, based on compilation to Syntax-Guided Synthesis (SyGuS) specifications. Our method reduces the motion planning problem to the problem of synthesizing a function that can choose the next ... More
Mutable WadlerFest DOTNov 23 2016The Dependent Object Types (DOT) calculus aims to model the essence of Scala, with a focus on abstract type members, path-dependent types, and subtyping. Other Scala features could be defined by translation to DOT. Mutation is a fundamental feature of ... More
Component-based Synthesis of Table Consolidation and Transformation Tasks from ExamplesNov 22 2016This paper presents an example-driven synthesis technique for automating a large class of data preparation tasks that arise in data science. Given a set of input tables and an out- put table, our approach synthesizes a table transformation program that ... More
Mixing Metaphors: Actors as Channels and Channels as ActorsNov 18 2016Nov 22 2016Channel- and actor-based programming languages are both used in practice, but the two are often confused. Languages such as Go provide anonymous processes which communicate using typed buffers---known as channels---while languages such as Erlang provide ... More
Precondition Inference for Peephole Optimizations in LLVMNov 18 2016Peephole optimizations are a common source of compiler bugs. Compiler developers typically transform an incorrect peephole optimization into a valid one by strengthening the precondition. This process is challenging and tedious. This paper proposes PInfer, ... More
A Theory of Available-by-Design Communicating SystemsNov 17 2016Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of ... More
Well-Typed Languages are SoundNov 16 2016Type soundness is an important property of modern programming languages. In this paper we explore the idea that "well-typed languages are sound": the idea that the appropriate typing discipline over language specifications guarantees that the language ... More
Undecidability of Asynchronous Session SubtypingNov 15 2016The most prominent proposals of subtyping for asynchronous session types are by Mostrous and Yoshida for binary sessions, by Chen et al. for binary sessions under the assumption that every message emitted is eventually consumed, and by Mostrous et al. ... More
Evolving the Incremental λ Calculus into a Model of Forward Automatic Differentiation (AD)Nov 10 2016Formal transformations somehow resembling the usual derivative are surprisingly common in computer science, with two notable examples being derivatives of regular expressions and derivatives of types. A newcomer to this list is the incremental $\lambda$-calculus, ... More
Efficient Implementation of a Higher-Order Language with Built-In ADNov 10 2016We show that Automatic Differentiation (AD) operators can be provided in a dynamic language without sacrificing numeric performance. To achieve this, general forward and reverse AD functions are added to a simple high-level dynamic language, and support ... More
Binomial Checkpointing for Arbitrary Programs with No User AnnotationNov 10 2016Heretofore, automatic checkpointing at procedure-call boundaries, to reduce the space complexity of reverse mode, has been provided by systems like Tapenade. However, binomial checkpointing, or treeverse, has only been provided in Automatic Differentiation ... More
Language Support for Reliable Memory RegionsNov 09 2016The path to exascale computational capabilities in high-performance computing (HPC) systems is challenged by the inadequacy of present software technologies to adapt to the rapid evolution of architectures of supercomputing systems. The constraints of ... More
Language Support for Reliable Memory RegionsNov 09 2016Nov 23 2016The path to exascale computational capabilities in high-performance computing (HPC) systems is challenged by the inadequacy of present software technologies to adapt to the rapid evolution of architectures of supercomputing systems. The constraints of ... More
Network-wide Configuration SynthesisNov 08 2016Computer networks are hard to manage. Given a set of high-level requirements (e.g., reachability, security), operators have to manually figure out the individual configuration of potentially hundreds of devices running complex distributed protocols so ... More
Sums of Uncertainty: Refinements Go GradualNov 08 2016A long-standing shortcoming of statically typed functional languages is that type checking does not rule out pattern-matching failures (run-time match exceptions). Refinement types distinguish different values of datatypes; if a program annotated with ... More
Neural Functional ProgrammingNov 07 2016We discuss a range of modeling choices that arise when constructing an end-to-end differentiable programming language suitable for learning programs from input-output examples. Taking cues from programming languages research, we study the effect of memory ... More
Neuro-Symbolic Program SynthesisNov 06 2016Recent years have seen the proposal of a number of neural architectures for the problem of Program Induction. Given a set of input-output examples, these architectures are able to learn mappings that generalize to new test inputs. While achieving impressive ... More
Learning a Static Analyzer from DataNov 06 2016To be practically useful, modern static analyzers must precisely model the effect of both, statements in the programming language as well as frameworks used by the program under analysis. While important, manually addressing these challenges is difficult ... More
A Traversable Fixed Size Small Object Allocator in C++Nov 05 2016Nov 08 2016At the allocation and deallocation of small objects with fixed size, the standard allocator of the runtime system has commonly a worse time performance compared to allocators adapted for a special application field. We propose a memory allocator, originally ... More
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler MappingsNov 04 2016The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get mapped down to individual instructions or combinations of instructions by ... More
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler MappingsNov 04 2016Nov 17 2016The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get mapped down to individual instructions or combinations of instructions by ... More
Stochastic Invariants for Probabilistic TerminationNov 03 2016Nov 16 2016Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 ... More
Stochastic Invariants for Probabilistic TerminationNov 03 2016Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 ... More
HPVM: A Portable Virtual Instruction Set for Heterogeneous Parallel SystemsNov 03 2016We describe a programming abstraction for heterogeneous parallel hardware, designed to capture a wide range of popular parallel hardware, including GPUs, vector instruction sets and multicore CPUs. Our abstraction, which we call HPVM, is a hierarchical ... More
Towards Automatic Resource Bound Analysis for OCamlNov 02 2016This article presents a resource analysis system for OCaml programs. This system automatically derives worst-case resource bounds for higher-order polymorphic programs with user-defined inductive types. The technique is parametric in the resource and ... More
Scala-gopher: CSP-style programming techniques with idiomatic ScalaNov 02 2016Cala-gopher is a library-level Scala implementation of communication sequence process constructs: channels, selectors (similar to analogical constructs in Limbo or Go) transputers (similar to Occam proc) and a set of high-level operations on top of akka ... More
A Performance Survey on Stack-based and Register-based Virtual MachinesNov 02 2016Virtual machines have been widely adapted for high-level programming language implementations and for providing a degree of platform neutrality. As the overall use and adaptation of virtual machines grow, the overall performance of virtual machines has ... More
Application of Case-Based Teaching and Learning in Compiler Design CourseNov 01 2016Compiler design is a course that discusses ideas used in construction of programming language compilers. Students learn how a program written in high level programming language and designed for humans understanding is systematically converted into low ... More
The Paths to Choreography ExtractionOct 31 2016Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They ... More
Edward: A library for probabilistic modeling, inference, and criticismOct 31 2016Probabilistic modeling is a powerful approach for analyzing empirical information. We describe Edward, a library for probabilistic modeling. Edward's design reflects an iterative process pioneered by George Box: build a model of a phenomenon, make inferences ... More
Edward: A library for probabilistic modeling, inference, and criticismOct 31 2016Nov 17 2016Probabilistic modeling is a powerful approach for analyzing empirical information. We describe Edward, a library for probabilistic modeling. Edward's design reflects an iterative process pioneered by George Box: build a model of a phenomenon, make inferences ... More
FEAST: An Automated Feature Selection Framework for Compilation TasksOct 29 2016The success of the application of machine-learning techniques to compilation tasks can be largely attributed to the recent development and advancement of program characterization, a process that numerically or structurally quantifies a target program. ... More
Multiactive objects and their applicationsOct 28 2016In order to tackle the development of concurrent and distributed systems, the active object programming model provides a high-level abstraction to program concurrent behaviours. There exists already a variety of active object frameworks targeted at a ... More
Push vs. Pull-Based Loop Fusion in Query EnginesOct 28 2016Database query engines use pull-based or push-based approaches to avoid the materialization of data across query operators. In this paper, we study these two types of query engines in depth and present the limitations and advantages of each engine. Similarly, ... More
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited ControlOct 28 2016We compare the expressive power of three programming abstractions for user-defined computational effects: Bauer and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control. This comparison allows a precise discussion about the ... More
Fencing off Go: Liveness and Safety for Channel-based Programming (extended version)Oct 27 2016Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication ... More
Type oriented parallel programming for ExascaleOct 27 2016Whilst there have been great advances in HPC hardware and software in recent years, the languages and models that we use to program these machines have remained much more static. This is not from a lack of effort, but instead by virtue of the fact that ... More
Gradual Typing in an Open WorldOct 26 2016Gradual typing combines static and dynamic typing in the same language, offering the benefits of both to programmers. Static typing provides error detection and strong guarantees while dynamic typing enables rapid prototyping and flexible programming ... More
Tracing where IoT data are collected and aggregatedOct 26 2016The Internet of Things (IoT) offers the infrastructure of the information society. It hosts smart objects that automatically collect and exchange data of various kinds, directly gathered from sensors or generated by aggregations. Suitable coordination ... More