Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately sea...
详细信息
ISBN:
(纸本)9781450342193
Contracts feel misunderstood, especially those with a higher-order soul. While software engineers appreciate contracts as tools for articulating the interface between components, functional programmers desperately search for their types and meaning, completely forgetting about their pragmatics. This gem presents a novel analysis of contract systems. Applied to the higher-order kind, this analysis reveals their large and clearly unappreciated software engineering potential. Three sample applications illustrate where this kind of exploration may lead.
We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programminglanguages suc...
详细信息
ISBN:
(纸本)9781450342193
We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, and both hard and soft constraints, as a foundation for universal probabilistic programminglanguages such as CHURCH, ANGLICAN, and VENTURE. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integration over the space of traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language, or for a language with soft constraints.
Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressions. Formulas are succinct, expressive, ...
详细信息
ISBN:
(纸本)9781450335492
Regression formulas are a domain-specific language adopted by several R packages for describing an important and useful class of statistical models: hierarchical linear regressions. Formulas are succinct, expressive, and clearly popular, so are they a useful addition to probabilistic programminglanguages? And what do they mean? We propose a core calculus of hierarchical linear regression, in which regression coefficients are themselves defined by nested regressions (unlike in R). We explain how our calculus captures the essence of the formula DSL found in R. We describe the design and implementation of Fabular, a version of the Tabular schema-driven probabilistic programminglanguage, enriched with formulas based on our regression calculus. To the best of our knowledge, this is the first formal description of the core ideas of R's formula notation, the first development of a calculus of regression formulas, and the first demonstration of the benefits of composing regression formulas and latent variables in a probabilistic programminglanguage.
Declarative programming has been hailed as a promising approach to parallel programming since it makes it easier to reason about programs while hiding the implementation details of parallelism from the programmer. How...
详细信息
ISBN:
(纸本)9781450340922
Declarative programming has been hailed as a promising approach to parallel programming since it makes it easier to reason about programs while hiding the implementation details of parallelism from the programmer. However, its advantage is also its disadvantage as it leaves the programmer with no straightforward way to optimize programs for performance. In this paper, we introduce Coordinated Linear Meld (CLM), a concurrent forward-chaining linear logic programminglanguage, with a declarative way to coordinate the execution of parallel programs allowing the programmer to specify arbitrary scheduling and data partitioning policies. Our approach allows the programmer to write graph-based declarative programs and then optionally to use coordination to fine-tune parallel performance. In this paper we specify the set of coordination facts, discuss their implementation in a parallel virtual machine, and show-through example-how they can be used to optimize parallel execution. We compare the performance of CLM programs against the original uncoordinated Linear Meld and several other frameworks.
To ease domain-specific language (DSL) development, a range of language workbenches have been created, which provide languagedesign facilities and programming tools, like editors and validators. In spite of these dev...
详细信息
ISBN:
(纸本)9781450344470
To ease domain-specific language (DSL) development, a range of language workbenches have been created, which provide languagedesign facilities and programming tools, like editors and validators. In spite of these developments, there is a perceived lack of tool support for execution monitoring, which is the basic block for program validation and maintenance. To partially address this issue some language workbenches offer ad-hoc solutions for DSL debugging, but lack support for other monitoring features. In the literature, a number of domain-specific monitoring tools have been proposed. However, there is no clear way for integrating these developments in existing language workbenches. This paper presents ten requirements needed for creating a modular and composable DSL monitoring infrastructure and proposes an object-oriented design pattern for DSL program monitoring. This pattern provides a practical answer to the problem of interfacing the runtime of a DSL with concrete domain-specific monitoring tools. To show the practicability of our approach, we add monitoring support to a simple lambda calculus, without changing the standard interpreter. The ease of integrating monitoring tools is shown through the development of a tracer and the integration of an off-the-shelf domain-specific profiler.
The proceedings contain 41 papers. The topics discussed include: safe programmable speculative parallelism;supporting speculative parallelization in the presence of dynamic data structures;cache topology aware computa...
ISBN:
(纸本)9781450300193
The proceedings contain 41 papers. The topics discussed include: safe programmable speculative parallelism;supporting speculative parallelization in the presence of dynamic data structures;cache topology aware computation mapping for multicores;a GPGPU compiler for memory optimization and parallelism management;safe to the last instruction: automated verification of a type-safe operating system;bringing extensibility to verified compilers;parameterized verification of transactional memories;detecting inefficiently-used containers to avoid bloat;finding low-utility data structures;evaluating the accuracy of java profilers;a context-free markup language for semi-structured text;printing floating-point numbers quickly and accurately with integers;adversarial memory for detecting destructive races;smooth interpretation;the reachability-bound problem;resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis;complete functional synthesis;and composing parallel software efficiently with lithe.
Metaprogramming techniques to generate code at runtime in a general-purpose meta-language have seen a surge of interest in recent years, driven by the widening performance gap between high-level languages and emerging...
详细信息
ISBN:
(纸本)9781450346481
Metaprogramming techniques to generate code at runtime in a general-purpose meta-language have seen a surge of interest in recent years, driven by the widening performance gap between high-level languages and emerging hardware platforms. In the context of Scala, the LMS (Lightweight Modular Staging) framework has contributed to "abstraction without regret"-high-level programming without performance penalty-in a number of challenging domains, through runtime code generation and embedded compiler pipelines based on stacks of DSLs. Based on this experience, this paper crystallizes some of the design decisions of LMS and discusses potential alternatives, which maintain the underlying spirit but differ in implementation choices: specifically, strategies for realizing more flexible front-end embeddings using type classes instead of higher-kinded types, and strategies for type-safe metaprogramming with untyped intermediate representations.
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and th...
详细信息
ISBN:
(纸本)9781450335492
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing. We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification. We have implemented an embedding of PSYNC in the SCALA programminglanguage with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.
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.
Principled syntactic code completion enables developers to change source code by inserting code templates, thus increasing developer efficiency and supporting language exploration. However, existing code completion sy...
详细信息
ISBN:
(纸本)9781450344470
Principled syntactic code completion enables developers to change source code by inserting code templates, thus increasing developer efficiency and supporting language exploration. However, existing code completion systems are ad-hoc and neither complete nor sound. They are not complete and only provide few code templates for selected programminglanguages. They also are not sound and propose code templates that yield invalid programs when inserted. This paper presents a generic framework that automatically derives complete and sound syntactic code completion from the syntax definition of arbitrary languages. A key insight of our work is to provide an explicit syntactic representation for incomplete programs using placeholders. This enables us to address the following challenges for code completion separately: (i) completing incomplete programs by replacing placeholders with code templates, (ii) injecting placeholders into complete programs to make them incomplete, and (iii) introducing lexemes and placeholders into incorrect programs through error-recovery parsing to make them correct so we can apply one of the previous strategies. We formalize our framework and provide an implementation in Spoofax.
暂无评论