This paper presents the design and implementation of Juniper: a functional reactive programminglanguage (FRP) targeting the Arduino and related microcontroller systems. Juniper provides a number of high level feature...
详细信息
The proceedings contain 20 papers. The topics discussed include: Recaf: Java dialects as libraries;classless Java;extensible modeling with managed data in Java;actor profiling in virtual execution environments;bootstr...
ISBN:
(纸本)9781450344463
The proceedings contain 20 papers. The topics discussed include: Recaf: Java dialects as libraries;classless Java;extensible modeling with managed data in Java;actor profiling in virtual execution environments;bootstrapping domain-specific meta-languages in language workbenches;dependence-driven delimited CPS transformation for JavaScript;synthesizing regular expressions from examples for introductory automata assignments;programmable semantic fragments: the design and implementation of typy;delaying decisions in variable concern hierarchies;automatic code generation in practice: experiences with embedded robot controllers;a change-centric approach to compile configurable systems with #ifdefs;a feature-based personalized recommender system for product-line configuration;IncLing: efficient product-line testing using incremental pairwise sampling;towards a software product line of trie-based collections;tool demo: testing configurable systems with FeatureIDE;automated regression testing of BPMN 2.0 processes: a capture and replay framework for continuous delivery;a vision for online verification-validation;and automatic non-functional testing of code generators families.
The majority of modern programminglanguages provide concurrency and object-orientation in some form. However, object-oriented concurrency remains cumbersome in many situations. We introduce the language OrcO, Orc wit...
详细信息
Java provides security and robustness by building a high-level security model atop the foundation of memory protection. Unfortunately, any native code linked into a Java program-including the million lines used to imp...
详细信息
We present a new, completely redesigned, version of F-star, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programminglanguage. In support of these comp...
详细信息
ISBN:
(纸本)9781450335492
We present a new, completely redesigned, version of F-star, a language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programminglanguage. In support of these complementary roles, F-star is a dependently typed, higher-order, call-by-value language with primitive effects including state, exceptions, divergence and IO. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F-star uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of SMT solving and manual proofs. Isolated from the effects, the core of F-star is a language of pure functions used to write specifications and proof terms its consistency is maintained by a semantic termination check based on a well-founded order. We evaluate our design on more than 55,000 lines of F-star we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programminglanguage, F-star is programmed (but not verified) in F-star, and bootstraps in both OCaml and F#. Our experience confirms F-star's pay-as-you-go cost model: writing idiomatic ML-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F-star is in verifying several key modules in an implementation of the TLS-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F-star than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F-star in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even mu F-star, a sizeable fragment of F-star itself these proofs make essential use of F-star's flexible combination of SMT automation and constructiv
We present an embedded language in Haskell for programming pipelined computations. The language is a combination of Feldspar (a functional language for array computations) and a new implementation of Ziria (a language...
详细信息
ISBN:
(纸本)9781450344333
We present an embedded language in Haskell for programming pipelined computations. The language is a combination of Feldspar (a functional language for array computations) and a new implementation of Ziria (a language for describing streaming computations originally designed for programming software defined radio). The resulting language makes heavy use of fusion: as in Feldspar, computations over arrays are fused to eliminate intermediate arrays, but Ziria processes can also be fused, eliminating the message passing between them, which in turn can give rise to more fusion at the Feldspar level. The result is a language in which we can first describe pipelined computations at a very fine-grained level, and only afterwards map computations onto the details of a specific parallel architecture, where the fusion helps us to generate efficient code. This flexible design method enables late design decisions cheaply, which in turn can lead to more efficient produced code. In the paper, we present two examples of pipelined computations in our language that can be run on Adapteva's Epiphany many-core coprocessor and on other back-ends.
The paper contains a summary of a focus group discussion concerning a possibility to design a programminglanguage so that implementation of the known design patterns would be easier than in the existing languages. We...
详细信息
This paper discusses the design and implementation of a domain-specific language for modelling energy optimal pumping systems (realizing specific flows and pressures). The domain model is transformed into a correspond...
详细信息
ISBN:
(纸本)9781450346467
This paper discusses the design and implementation of a domain-specific language for modelling energy optimal pumping systems (realizing specific flows and pressures). The domain model is transformed into a corresponding mixed-integer linear program which can be solved by standard solvers. The solution together with the original model are transformed into executable simulation models (e.g. MODELICA or MATLAB SIMULINK).
Even if multicore architectures are nowadays extremely wide- spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in ou...
详细信息
ISBN:
(纸本)9783319390833;9783319390826
Even if multicore architectures are nowadays extremely wide- spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine- tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.
Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired ad...
详细信息
ISBN:
(纸本)9781450335492
Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.
暂无评论