Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programminglanguage features. While his calculus is type-safe, it is not coherent: different d...
详细信息
ISBN:
(纸本)9781450342193
Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programminglanguage features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programminglanguages, as the semantics of the programminglanguage becomes implementation-dependent. This paper presents lambda(i) : a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of lambda(i), with three variants of disjointness. In the simplest variant, which does not allow inverted perpendicular types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce inverted perpendicular types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with inverted perpendicular types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.
The proceedings contain 23 papers. The topics discussed include: parsing and reflective printing, bidirectionally;taming context-sensitive languages with principled stateful parsing;efficient development of consistent...
ISBN:
(纸本)9781450344470
The proceedings contain 23 papers. The topics discussed include: parsing and reflective printing, bidirectionally;taming context-sensitive languages with principled stateful parsing;efficient development of consistent projectional editors using grammar cells;experiences of Models@run-time with EMF and CDO;runtime support for rule-based access-control evaluation through model-transformation;object-oriented design pattern for DSL program monitoring;execution framework of the GEMOC studio;languagedesign and implementation for the domain of coding conventions;BSML-mbeddr: integrating semantically configurable state-machine models in a C programming environment;adding uncertainty and units to quantity types in software models;FRaMED: full-fledge role modeling editor;towards a universal code formatter through machine learning;the IDE portability problem and its solution in Monto;principled syntactic code completion using placeholders;automated testing support for reactive domain-specific modelling languages;symbolic execution of high-level transformations;and raincode assembler compiler.
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.
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.
The proceedings contain 11 papers. The topics discussed include: signal rate inference for multidimensional Faust;type directives and type graphs in elm;towards the layout of things;a portable VM-based implementation ...
ISBN:
(纸本)9781450347679
The proceedings contain 11 papers. The topics discussed include: signal rate inference for multidimensional Faust;type directives and type graphs in elm;towards the layout of things;a portable VM-based implementation platform for non-strict functional programminglanguages;contractive functions on infinite data structures;design and implementation of probabilistic programminglanguage Anglican;a lazy language needs a lazy type system: introducing polymorphic contexts;Eliom: tierless web programming from the ground up;synthesis of railway-signaling plans using reachability games;a lightweight hat: simple type-preserving instrumentation for self-tracing lazy functional programs;and identifying and introducing interfaces and callbacks using wrangler.
The proceedings contain 9 papers. The topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performanc...
ISBN:
(纸本)9781450329170
The proceedings contain 9 papers. The topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performance of Intel sandy bridge and AMD bulldozer;non-volatile memory is a broken time machine;O-structures: semantics for versioned memory;outlawing ghosts: avoiding out-of-thin-air results;and trash in cache: detecting eternally silent stores.
We present FLIX, a declarative programminglanguage for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone fu...
详细信息
We present FLIX, a declarative programminglanguage for specifying and solving least fixed point problems, particularly static program analyses. FLIX is inspired by Datalog and extends it with lattices and monotone functions. Using FLIX, implementors of static analyses can express a broader range of analyses than is currently possible in pure Datalog, while retaining its familiar rule-based syntax. We define a model-theoretic semantics of FLIX as a natural extension of the Datalog semantics. This semantics captures the declarative meaning of FLIX programs without imposing any specific evaluation strategy. An efficient strategy is semi-naive evaluation which we adapt for FLIX. We have implemented a compiler and runtime for FLIX, and used it to express several well-known static analyses, including the IFDS and IDE algorithms. The declarative nature of FLIX clearly exposes the similarity between these two algorithms.
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Often...
详细信息
Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.
This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees ...
详细信息
This paper presents a new approach for synthesizing transformations on tree-structured data, such as Unix directories and XML documents. We consider a general abstraction for such data, called hierarchical data trees (HDTs) and present a novel example-driven synthesis algorithm for HDT transformations. Our central insight is to reduce the problem of synthesizing tree transformers to the synthesis of list transformations that are applied to the paths of the tree. The synthesis problem over lists is solved using a new algorithm that combines SMT solving and decision tree learning. We have implemented our technique in a system called HADES and show that HADES can automatically synthesize a variety of interesting transformations collected from online forums.
The proceedings contain 46 papers. The topics discussed include: optimizing database-backed applications with query synthesis;automated feedback generation for introductory programming assignments;fast condensation of...
ISBN:
(纸本)9781450320146
The proceedings contain 46 papers. The topics discussed include: optimizing database-backed applications with query synthesis;automated feedback generation for introductory programming assignments;fast condensation of the program dependence graph;scalable variable and data type detection in a binary rewriter;rely-guarantee references for refinement types over aliased mutable data;harmonizing classes, functions, tuples, and type parameters in Virgil III;terra: a multi-stage language for high-performance computing;SMAT: an input adaptive auto-tuner for sparse matrix-vector multiplication;when polyhedral transformations meet SIMD code generation;CLAP: recording local executions to reproduce concurrency failures;CONCURRIT: a domain specific language for reproducing concurrency bugs;compiler testing via a theory of sound optimisations in the C11/C++11 memory model;and almost-correct specifications: a modular semantic framework for assigning confidence to warnings.
暂无评论