the proceedings contain 12 papers. the topics discussed include: using many-core coprocessor to boost up Erlang VM;on the scalability of the Erlang term storage;Riak PG: distributed process groups on dynamo-style dist...
ISBN:
(纸本)9781450323857
the proceedings contain 12 papers. the topics discussed include: using many-core coprocessor to boost up Erlang VM;on the scalability of the Erlang term storage;Riak PG: distributed process groups on dynamo-style distributed storage;multicore profiling for Erlang programs using Percept2;software agents mobility using process migration mechanism in distributed Erlang;actor scheduling for multicore hierarchical memory platforms;extending Erlang by utilising RefactorErl;scalable persistent storage for Erlang: theory and practice;towards an abstraction for remote evaluation in Erlang;towards property-based testing of RESTful web services;turning web services descriptions into QuickCheck models for automatic testing;and testing blocking operations with QuickCheck's component library.
the proceedings contain 41 papers. the topics discussed include: C-SHORe: a collapsible approach to higher-order verification;exploiting vector instructions with generalized stream fusion;type-theory in color;Mtac: a ...
ISBN:
(纸本)9781450323260
the proceedings contain 41 papers. the topics discussed include: C-SHORe: a collapsible approach to higher-order verification;exploiting vector instructions with generalized stream fusion;type-theory in color;Mtac: a monad for typed tactic programming in Coq;fun with semirings: a functional pearl on the abuse of linear algebra;programming and reasoning with algebraic effects and dependent types;well-founded recursion with copatterns: a unified approach to termination and productivity;productive coprogramming with guarded recursion;higher-order functional reactive programming without spacetime leaks;simple and compositional reification of monadic embedded languages;structural recursion for querying ordered graphs;a nanopass framework for commercial compiler development;the bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier;and a practical theory of language-integrated query.
the proceedings contain 45 papers. the topics discussed include: cooperative empirical failure avoidance for multithreaded programs;parasol and GreenSwitch: managing datacenters powered by renewable energy;power conta...
ISBN:
(纸本)9781450318709
the proceedings contain 45 papers. the topics discussed include: cooperative empirical failure avoidance for multithreaded programs;parasol and GreenSwitch: managing datacenters powered by renewable energy;power containers: an OS facility for fine-grained power and energy management on multicore servers;ConAir: featherweight concurrency bug recovery via single-threaded idempotent execution;using likely invariants for automated software fault localization;the rise of the expert amateur: DIY culture and the evolution of computer science;DeAliaser: alias speculation using atomic region support;regularities considered harmful: forcing randomness to memory accesses to reduce row buffer conflicts for multi-core, multi-bank systems;a study of the scalability of stop-the-world garbage collectors on multicores;Iago attacks: why the system call API is a bad untrusted RPC interface;and InkTag: secure applications on an untrusted operating system.
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. the description of the small-step operational semantics ...
详细信息
ISBN:
(纸本)9781450323260
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. the description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. this implies that our implementation is a correct evaluator for an abstract specification equipped with a bigstep semantics.
this pearl presents a novel technique for constructing a first-order syntax tree directly from a higher-order interface. We exploit circular programming to generate names for new variables, resulting in a simple yet e...
详细信息
ISBN:
(纸本)9781450323260
this pearl presents a novel technique for constructing a first-order syntax tree directly from a higher-order interface. We exploit circular programming to generate names for new variables, resulting in a simple yet efficient method. Our motivating application is the design of embedded languages supporting variable binding, where it is convenient to use higher-order syntax when constructing programs, but first-order syntax when processing or transforming programs.
We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. this rules out certain mistak...
详细信息
ISBN:
(纸本)9781450323260
We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. this rules out certain mistakes, including representation exposure and data races, and enables new idioms, such as gradual initialization, memory re-use, and (type) state changes. Although the core static discipline disallows sharing a mutable data structure, Mezzo offers several ways of working around this restriction, including a novel dynamic ownership control mechanism which we dub "adoption and abandon".
We present a novel set of meta-programming primitives for use in a dependently-typed functional language. the types of our meta-programs provide strong and precise guarantees about their termination, correctness and c...
详细信息
ISBN:
(纸本)9781450323260
We present a novel set of meta-programming primitives for use in a dependently-typed functional language. the types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.
the bondi programming language is multi-polymorphic, in that it supports four polymorphic programming styles within a small core of computation, namely a typed pattern calculus. bondi's expressive power is illustr...
详细信息
functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource...
详细信息
ISBN:
(纸本)9781450323260
functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style. In this paper, we give a new language for higher-order reactive programming. Our language generalizes and simplifies prior type systems for reactive programming, by supporting the use of streams of streams, first-class functions, and higher-order operations. We also support many temporal operations beyond streams, such as terminatable streams, events, and even resumptions with first-class schedulers. Furthermore, our language supports an efficient implementation strategy permitting us to eagerly deallocate old values and statically rule out spacetime leaks, a notorious source of inefficiency in reactive programs. Furthermore, these memory guarantees are achieved without the use of a complex substructural type discipline. We also show that our implementation strategy of eager deallocation is safe, by showing the soundness of our type system with a novel step-indexed Kripke logical relation.
One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exception...
详细信息
ISBN:
(纸本)9781450323260
One often cited benefit of pure functionalprogramming is that pure code is easier to test and reason about, both formally and informally. However, real programs have side-effects including state management, exceptions and interactions withthe outside world. Haskell solves this problem using monads to capture details of possibly side-effecting computations - it provides monads for capturing state, I/O, exceptions, non-determinism, libraries for practical purposes such as CGI and parsing, and many others, as well as monad transformers for combining multiple effects. Unfortunately, useful as monads are, they do not compose very well. Monad transformers can quickly become unwieldy when there are lots of effects to manage, leading to a temptation in larger programs to combine everything into one coarse-grained state and exception monad. In this paper I describe an alternative approach based on handling algebraic effects, implemented in the IDRIS programming language. I show how to describe side effecting computations, how to write programs which compose multiple fine-grained effects, and how, using dependent types, we can use this approach to reason about states in effectful programs.
暂无评论