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

35th acm-SIGPLAN-sigact symposium on principles of programming languages

作者： Neamtiu, Iulian Hicks, Michael Foster, Jeffrey S. Pratikakis, Polyvios Univ Maryland Dept Comp Sci College Pk MD 20742 USA

ISBN: (纸本)9781595936899

This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we compute the effect of the computation that has already occurred (the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency (TVC), a novel correctness property for dynamic software updates. TVC ensures that program mer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.

关键词： Contextual effects computation effects type and effect systems version consistency dynamic software updating data race detection

来源：评论

学校读者我要写书评

暂无评论

Foundations for Structured programming with GADTs

Foundations for Structured Programming with GADTs

引用

35th acm-SIGPLAN-sigact symposium on principles of programming languages

作者： Johann, Patricia Ghani, Neil Rutgers State Univ Camden NJ 08102 USA

ISBN: (纸本)9781595936899

GADTs are at the cutting edge of functional programming and becomemore widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derivean initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools - analogous to the well-known and widely-used ones for algebraic and nested data types - for reasoning about, programming with, and improving the performance of programs involving, GADTs;we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can bederived. © 2008 acm.

关键词： GADTs initial algebra semantics program fusion

来源：评论

学校读者我要写书评

暂无评论

Imperative Self-Adjusting Computation

Imperative Self-Adjusting Computation

引用

35th acm-SIGPLAN-sigact symposium on principles of programming languages

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

ISBN: (纸本)9781595936899

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. © 2008 acm.

关键词： Self-adjusting computation incremental computation step-indexed logical relations imperative programming change propagation memoization mutable state

来源：评论

学校读者我要写书评

暂无评论

Boomerang: Resourceful Lenses for String Data

Boomerang: Resourceful Lenses for String Data

引用

35th acm-SIGPLAN-sigact symposium on principles of programming languages

作者： Bohannon, Aaron Foster, J. Nathan Pierce, Benjamin C. Pilkiewicz, Alexandre Schmitt, Alan Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781595936899

A lens is a bidirectional program. When read from left toright, 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 theoutput, 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 anew semantic space of dictionary lenses, enriching the lenses of Foster et al. (2007) with support for two additional combinators for marking "reorderable chunks" andtheir 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 format sincluding 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. © 2008 acm.

关键词： Bidirectional languages lenses view update problem regular string transducers regular types

来源：评论

学校读者我要写书评

暂无评论

Clowns to the Left of me, Jokers to the Right (Pearl) Dissecting Data Structures

Clowns to the Left of me, Jokers to the Right (<i>Pearl</i>)...

引用

35th acm-SIGPLAN-sigact symposium on principles of programming languages

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

ISBN: (纸本)9781595936899

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.

关键词： Datatype Differentiation Dissection Division Generic programming Iteration Polynomial Stack Tail Recursion Traversal Zipper

来源：评论

学校读者我要写书评

暂无评论

Conference Record of the Annual acm symposium on principles of programming languages: Foreword

Conference Record of the Annual ACM Symposium on Principles ...

引用

Conference Record of the Annual acm symposium on principles of programming languages 2008年 iii页

作者： Wadler, Philip University of Edinburgh United Kingdom

来源：评论

学校读者我要写书评

暂无评论

The design and implementation of typed scheme

引用

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

作者： Tobin-Hochstadt, Sam Felleisen, Matthias Northeastern Univ PLT Boston MA 02115 USA

When scripts in untyped languages grow into large programs, maintaining them becomes difficult. A lack of types in typical scripting languages means that programmers must (re) discover critical pieces of design information every time they wish to change a program. This analysis step both slows down the maintenance process and may even introduce mistakes due to the violation of undiscovered invariants. This paper presents Typed Scheme, an explicitly typed extension of an untyped scripting language. Its type system is based on the novel notion of occurrence typing, which we formalize and mechanically prove sound. The implementation of Typed Scheme additionally borrows elements from a range of approaches, including recursive types, true unions and subtyping, plus polymorphism combined with a modicum of local inference. Initial experiments with the implementation suggest that Typed Scheme naturally accommodates the programming style of the underlying scripting language, at least for the first few thousand lines of ported code.

关键词： languages design type systems Scheme

来源：评论

学校读者我要写书评

暂无评论

Much ado about two (pearl) -: A pearl on parallel prefix computation

引用

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

作者： Voigtlaender, Janis Tech Univ Dresden Inst Theoret Informat D-01062 Dresden Germany

This pearl develops a statement about parallel prefix computation in the spirit of Knuth's 0-1-Principle for oblivious sorting algorithms. It turns out that 0- 1 is not quite enough here. The perfect hammer for th... 详细信息

关键词： algorithms languages verification 0-1-principle free theorems parallel prefix computation relational parametricity

来源：评论

学校读者我要写书评

暂无评论

Subcubic algorithms for recursive state machines

引用

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

作者： Chaudhuri, Swarat Penn State Univ University Pk PA 16802 USA

We show that the reachability problem for recursive state machines (or equivalently, pushdown systems), believed for long to have cubic worst-case complexity, can be solved in slightly subcubic time. All that is necessary for the new bound is a simple adaptation of a known technique. We also show that a better algorithm exists if the input machine does not have infinite recursive loops.

关键词： algorithms theory verification recursive state machines pushdown systems CFL-reachability context-free languages interprocedural analysis transitive closure cubic bottleneck

来源：评论

学校读者我要写书评

暂无评论

Relevance heuristics for program analysis

引用

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

作者： McMillan, K. L. Cadence Res Labs Berkeley CA USA

Relevance heuristics allow us to tailor a program analysis to a particular property to be verified. This in turn makes it possible to improve the precision of the analysis where needed, while maintaining scalability. In this talk I will discuss the principles by which SAT solvers and other decision procedures decide what information is relevant to a given proof. Then we will see how these ideas can be exploited in program verification using the method of Craig interpolation. The result is an analysis that is finely tuned to prove a given property of a program. At the end of the talk, I will cover some recent research in this area, including the use of interpolants for verifying heap-manipulating programs.

关键词： languages theory verification abstract interpretation model checking Craig interpolation

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：