检索结果-内蒙古大学图书馆

From dirt to shovels - Fully automatic tool generation from ad hoc data

acm SIGPLAN NOTICES 2008年第1期43卷 421-434页

作者： Fisher, Kathleen Walker, David Zhu, Kenny Q. White, Peter Princeton Univ Princeton NJ 08544 USA

An ad hoc data source is any semistructured data source for which useful data analysis and transformation tools are not readily available. Such data must be queried, transformed and displayed by systems administrators, computational biologists, financial analysts and hosts of others on a regular basis. In this paper, we demonstrate that it is possible to generate a suite of useful data processing tools, including a semi-structured query engine, several format converters, a statistical analyzer and data visualization routines directly from the ad hoc data itself, without any human intervention. The key technical contribution of the work is a multi-phase algorithm that automatically infers the structure of an ad hoc data source and produces a format specification in the PADS data description language. Programmers wishing to implement custom data analysis tools can use such descriptions to generate printing and parsing libraries for the data. Alternatively, our software infrastructure will push these descriptions through the PADS compiler, creating format-dependent modules that, when linked with format-independent algorithms for analysis and transformation, result in fully functional tools. We evaluate the performance of our inference algorithm, showing it scales linearly in the size of the training data - completing in seconds, as opposed to the hours or days it takes to write a description by hand. We also evaluate the correctness of the algorithm, demonstrating that generating accurate descriptions often requires less than 5% of the available data.

关键词： languages algorithms data description languages grammar induction tool generation ad hoc data

来源：评论

学校读者我要写书评

暂无评论

Boomerang: Resourceful lenses for string data

引用

acm SIGPLAN NOTICES 2008年第1期43卷 407-419页

作者： Bohannon, Aaron Foster, J. Nathan Pierce, Benjamin C. Pilkiewicz, Alexandre Schmitt, Alan Univ Penn Philadelphia PA 19104 USA Ecole Polytech F-91128 Palaiseau France

A lens is a bidirectional program. When read from left to right, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an "update translator" that takes an input together with an updated output and produces a new input that reflects the update. Many variants of this idea have been explored in the literature, but none deal fully with ordered data. If, for example, an update changes the order of a list in the output, the items in the output list and the chunks of the input that generated them can be misaligned, leading to lost or corrupted data. We attack this problem in the context of bidirectional transformations over strings, the primordial ordered data type. We first propose a collection of bidirectional string lens combinators, based on familiar operations on regular transducers (union, concatenation, Kleene-star) and with a type system based on regular expressions. We then design a new semantic space of dictionary lenses, enriching the lenses of Foster et al. (2007b) with support for two additional combinators for marking "reorderable chunks" and their keys. To demonstrate the effectiveness of these primitives, we describe the design and implementation of Boomerang, a full-blown bidirectional programming language with dictionary lenses at its core. We have used Boomerang to build transformers for complex real-world data formats including the SwissProt genomic database. We formalize the essential property of resourcefulness-the correct use of keys to associate chunks in the input and output-by defining a refined semantic space of quasi-oblivious lenses. Several previously studied properties of lenses turn out to have compact characterizations in this space.

关键词： languages design theory bidirectional languages lenses view update problem regular string transducers regular types

来源：评论

学校读者我要写书评

暂无评论

Imperative self-adjusting computation

引用

acm SIGPLAN NOTICES 2008年第1期43卷 309-322页

作者： Acar, Umut A. Ahmed, Amal Blume, Matthias Toyota Technol Inst Chicago IL USA

Self-adjusting computation enables writing programs that can automatically and efficiently respond to changes to their data (e. g., inputs). The idea behind the approach is to store all data that can change over time in modifiable references and to let computations construct traces that can drive change propagation. After changes have occurred, change propagation updates the result of the computation by re-evaluating only those expressions that depend on the changed data. Previous approaches to self-adjusting computation require that modifiable references be written at most once during execution-this makes the model applicable only in a purely functional setting. In this paper, we present techniques for imperative self-adjusting computation where modifiable references can be written multiple times. We define a language SAIL (Self-Adjusting Imperative Language) and prove consistency, i.e., that change propagation and from-scratch execution are observationally equivalent. Since SAIL programs are imperative, they can create cyclic data structures. To prove equivalence in the presence of cycles in the store, we formulate and use an untyped, step-indexed logical relation, where step indices are used to ensure well-foundedness. We show that SAIL accepts an asymptotically efficient implementation by presenting algorithms and data structures for its implementation. When the number of operations (reads and writes) per modifiable is bounded by a constant, we show that change propagation becomes as efficient as in the non-imperative case. The general case incurs a slowdown that is logarithmic in the maximum number of such operations. We describe a prototype implementation of SAIL as a Standard ML library.

关键词： languages design semantics algorithms self-adjusting computation incremental computation step-indexed logical relations imperative programming change propagation memoization mutable state

来源：评论

学校读者我要写书评

暂无评论

Separation logic, abstraction and inheritance

引用

acm SIGPLAN NOTICES 2008年第1期43卷 75-86页

作者： Parkinson, Matthew J. Bierman, Gavin M. Univ Cambridge Cambridge CB2 1TN England

Inheritance is a fundamental concept in object-oriented programming, allowing new classes to be defined in terms of old classes. When used with care, inheritance is an essential tool for object-oriented programmers. Thus, for those interested in developing formal verification techniques, the treatment of inheritance is of paramount importance. Unfortunately, inheritance comes in a number of guises, all requiring subtle techniques. To address these subtleties, most existing verification methodologies typically adopt one of two restrictions to handle inheritance: either (1) they prevent a derived class from restricting the behaviour of its base class (typically by syntactic means) to trivialize the proof obligations;or (2) they allow a derived class to restrict the behaviour of its base class, but require that every inherited method must be reverified. Unfortunately, this means that typical inheritance-rich code either cannot be verified or results in an unreasonable number of proof obligations. In this paper, we develop a separation logic for a core object-oriented language. It allows derived classes which override the behaviour of their base class, yet supports the inheritance of methods without reverification where this is safe. For each method, we require two specifications: a static specification that is used to verify the implementation and direct method calls (in Java this would be with a super call);and a dynamic specification that is used for calls that are dynamically dispatched;along with a simple relationship between the two specifications. Only the dynamic specification is involved with behavioural subtyping. This simple separation of concerns leads to a powerful system that supports all forms of inheritance with low proof-obligation overheads. We both formalize our methodology and demonstrate its power with a series of inheritance examples.

关键词： languages theory verification separation logic modularity classes

来源：评论

学校读者我要写书评

暂无评论

Clowns to the left of me, jokers to the right (pearl) -: Dissecting data structures

引用

acm SIGPLAN NOTICES 2008年第1期43卷 287-295页

作者： McBride, Conor Univ Nottingham Nottingham NG7 2RD England

This paper introduces a small but useful generalisation to the 'derivative' operation on datatypes underlying Huet's notion of 'zipper' (Huet 1997;McBride 2001;Abbott et al. 2005b), giving a concrete representation to one-hole contexts in data which is undergoing transformation. This operator, 'dissection', turns a container-like functor into a bifunctor representing a one-hole context in which elements to the left of the hole are distinguished in type from elements to its right. I present dissection here as a generic program, albeit for polynomial functors only. The notion is certainly applicable more widely, but here I prefer to concentrate on its diverse applications. For a start, map-like operations over the functor and fold-like operations over the recursive data structure it induces can be expressed by tail recursion alone. Further, the derivative is readily recovered from the dissection. Indeed, it is the dissection structure which delivers Huet's operations for navigating zippers. The original motivation for dissection was to define 'division', capturing the notion of leftmost hole, canonically distinguishing values with no elements from those with at least one. Division gives rise to an isomorphism corresponding to the remainder theorem in algebra. By way of a larger example, division and dissection are exploited to give a relatively efficient generic algorithm for abstracting all occurrences of one term from another in a first-order syntax. The source code for the paper is available online(1) and compiles with recent extensions to the Glasgow Haskell Compiler.

关键词： algorithms design languages theory datatype differentiation dissection division generic programming iteration polynomial stack tail recursion traversal zipper

来源：评论

学校读者我要写书评

暂无评论

Systems biology, models, and concurrency

引用

acm SIGPLAN NOTICES 2008年第1期43卷 1-2页

作者： Fontana, Walter Harvard Univ Sch Med Dept Syst Biol Boston MA 02115 USA

Models will play a central role in the representation, storage, manipulation, and communication of knowledge in systems biology. Models capable of fulfilling such a role will likely differ from the familiar styles deployed with great success in the physical sciences. Molecular systems at the basis of cellular decision processes are concurrent and combinatorial. Their behavior is as much constrained by relationships of causality between molecular interactions as it is by chemical kinetics. Understanding how such systems give rise to coherent behavior and designing effective interventions to fight disease will require a notion of model that is akin to the concept of program in computer science. I will discuss recent progress in implementing a platform and tools for formal analysis that bring us closer to this vision. Protein interactions are represented by means of rules expressed in a formal language that captures a very simple, yet effective and biologically meaningful level of abstraction. Models, then, are collections of rules operating on an initial set of agents, in complete analogy to rules of organic chemical reactions. I will describe tools for analyzing and navigating rule collections as well as exploring their dynamics. We draw on concepts familiar to computer science, especially event structures, and adapt them to biological needs with the goal of formalizing the notion of "pathway". The challenges are many, but a roadmap for the future is discernible. Computer science will play a central role in providing an additional foundational layer, both theoretical and practical, that neither physics nor chemistry can offer on their own in the future definition of the biological sciences.

关键词： experimentation languages systems biology models concurrency kappa

来源：评论

学校读者我要写书评

暂无评论

Conference Record of POPL 2007: The 34th acm SIGPLAN-sigact symposium on principles of programming languages - Papers Presented at the symposium

Conference Record of POPL 2007: The 34th ACM SIGPLAN-SIGACT ...

引用

34th acm SIGPLAN-sigact symposium on principles of programming languages, POPL'07

ISBN: (纸本)1595935754

The proceedings contain 39 papers. The topics discussed include: operational semantics for multi-language programs;a typed intermediate language for compiling multiple inheritance;dynamic heap type inference for program understanding and debugging;compositional dynamic test generation;locality approximation using time;modular type classes;first-class nonstandard interpretations by opening closures;generative unbinding of names;types, bytes, and separation logic;a very modal model of a modern, major, general type system;from implementation to theory in product synthesis;lightweight fusion by fixed point promotion;lazy multivariate higher-order forward-mode AD;towards a mechanized metatheory of standard ML;logic-flow analysis of higher-order programs;and extracting queries by static analysis of transparent persistence.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Automatic inference of stationary fields: a generalization of java's final fields

引用

acm SIGPLAN NOTICES 2008年第1期43卷 183-195页

作者： Unkel, Christopher Lam, Monica S. Stanford Univ Comp Syst Lab Stanford CA 94305 USA

Java programmers can document that the relationship between two objects is unchanging by declaring the field that encodes that relationship to be final. This information can be used in program understanding and detection of errors in new code additions. Unfortunately, few fields in programs are actually declared final. Programs often contain fields that could be final, but are not declared so. Moreover, the definition of final has restrictions on initialization that limit its applicability. We introduce stationary fields as a generalization of final. A field in a program is stationary if, for every object that contains it, all writes to the field occur before all the reads. Unlike the definition of final fields, there can be multiple writes during initialization, and initialization can span multiple methods. We have developed an efficient algorithm for inferring which fields are stationary in a program, based on the observation that many fields acquire their value very close to object creation. We presume that an object's initialization phase has concluded when its reference is saved in some heap object. We perform precise analysis only regarding recently created objects. Applying our algorithm to real-world Java programs demonstrates that stationary fields are more common than final fields: 44-59% vs. 11-17% respectively in our benchmarks. These surprising results have several significant implications. First, substantial portions of Java programs appear to be written in a functional style. Second, initialization of these fields occurs very close to object creation, when very good alias information is available. These results open the door for more accurate and efficient pointer alias analysis.

关键词： algorithms languages stationary Java final initialization

来源：评论

学校读者我要写书评

暂无评论

Cryptographically sound implementations for typed information-flow security

引用

acm SIGPLAN NOTICES 2008年第1期43卷 323-335页

作者： Fournet, Cedric Rezk, Tamara Microsoft Research MSR-INRIA Joint Centre France MSR-INRIA Joint Centre France

In language-based security, confidentiality and integrity policies conveniently specify the permitted flows of information between different parts of a program with diverse levels of trust. These policies enable a simple treatment of security, and they can often be verified by typing. However, their enforcement in concrete systems involves delicate compilation issues. We consider cryptographic enforcement mechanisms for imperative programs with untrusted components. Such programs may represent, for instance, distributed systems connected by some untrusted network. In source programs, security depends on an abstract access-control policy for reading and writing the shared memory. In their implementations, shared memory is unprotected and security depends instead on encryption and signing. We build a translation from well-typed source programs and policies to cryptographic implementations. To establish its correctness, we develop a type system for the target language. Our typing rules enforce a correct usage of cryptographic primitives against active adversaries;from an information-flow viewpoint, they capture controlled forms of robust declassification and endorsement. We show type soundness for a variant of the non-interference property, then show that our translation preserves typability. We rely on concrete primitives and hypotheses for cryptography, stated in terms of probabilistic polynomial-time algorithms and games. We model these primitives as commands in our target language. Thus, we develop a uniform language-based model of security, ranging from computational non-interference for probabilistic programs down to standard cryptographic hypotheses.

关键词： security verification design languages secure information flow confidentiality integrity non-interference type systems compilers probabilistic programs cryptography computational model

来源：评论

学校读者我要写书评

暂无评论

Conference Record of POPL [registered trademark] 2007: The 34th acm SIGPLAN-sigact symposium on principles of programming languages [registered trademark] : Foreword

引用

acm SIGPLAN Notices 2007年第1期42卷

作者： Felleisen, Matthias Northeastern University Boston MA United States

No abstract available

关键词：

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：