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

Proceedings of the 36th annual acm SIGPLAN-sigact symposium on principles of programming languages

作者： Patricia Johann University of Strathclyde

No abstract available.

ISBN: (纸本)9781605583792

No abstract available.

关键词：

来源：评论

学校读者我要写书评

暂无评论

POPL'08 - Proceedings of the 35th Annual acm SIGPLAN-sigact symposium on principles of programming languages

POPL'08 - Proceedings of the 35th Annual ACM SIGPLAN-SIGACT ...

引用

35th Annual acm SIGPLAN-sigact symposium on principles of programming languages, POPL'08

ISBN: (纸本)9781595936899

The proceedings contain 37 papers. The topics discussed include: proving non-termination;subcubic algorithms for recursive state machines;back to the future: revisiting precise program verification using SMT solvers;automatic inference of stationary fields: a generalization of Java's final fields;demand-driven alias analysis for C;A theory of platform-dependent low-level software;generating precise and concise procedure summaries;lifting abstract interpreters to quantified logical domains;relational inductive shape analysis;a theory of contracts for web services;multiparty asynchronous session types;clowns to the left of me, jokers to the right (pearl): dissecting data structures;foundations for structured programming with GADTs;imperative self-adjusting computation;cryptographically sound implementations for typed information-flow security;and on the computational soundness of cryptographically masked flows.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Classical BI (A Logic for Reasoning about Dualising Resources)

引用

acm SIGPLAN NOTICES 2009年第1期44卷 328-339页

作者： Brotherston, James Calcagno, Cristiano Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England

We show how to extend O'Hearn and Pym's logic of bunched implications, BI, to classical BI ( CBI), in which both the additive and the multiplicative connectives behave classically. Specifically, CBI is a non-conservative extension of (propositional) Boolean BI that includes multiplicative versions of falsity, negation and disjunction. We give an algebraic semantics for CBI that leads us naturally to consider resource models of CBI in which every resource has a unique dual. We then give a cut-eliminating proof system for CBI, based on Belnap's display logic, and demonstrate soundness and completeness of this proof system with respect to our semantics.

关键词： Theory verification languages Classical BI display logic semantics resource models completeness cut-elimination bunched implications

来源：评论

学校读者我要写书评

暂无评论

Subcubic Algorithms for Recursive State Machines

Subcubic Algorithms for Recursive State Machines

引用

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

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

ISBN: (纸本)9781595936899

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.

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

来源：评论

学校读者我要写书评

暂无评论

Semantics of Transactional Memory and Automatic Mutual Exclusion

Semantics of Transactional Memory and Automatic Mutual Exclu...

引用

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

作者： Abadi, Martin Birrell, Andrew Harris, Tim Isard, Michael Microsoft Research Silicon Valley United States University of California Santa Cruz CA United States Microsoft Research Cambridge United Kingdom

ISBN: (纸本)9781595936899

Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming, However, the semantics of these features can be delicate and problematic. In this paper we explore the tradeoffs between semantic simplicity, the viability of efficient implementation strategies, and the flexibility of language constructs. Specifically, we develop semantics and type systems for the constructs of the Automatic Mutual Exclusion (AME) programming model;our results apply also to other constructs, such as atomic blocks. With this semantics as a point of reference, we study several implementation strategies. We model STM systems that use in-place update, optimistic concurrency, lazy conflict detection, and roll-back. These strategies are correct only under non-trivial assumptions that we identify and analyze. One important source of errors is that some efficient implementations create dangerous "zombie" computations where a transaction keeps running after experiencing a conflict;the assumptions confine the effects of these computations.

关键词： languages Theory

来源：评论

学校读者我要写书评

暂无评论

Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures

Lightweight Semiformal Time Complexity Analysis for Purely F...

引用

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

作者： Danielsson, Nils Anders Chalmers Univ Technol Gothenburg Sweden

ISBN: (纸本)9781595936899

Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.

关键词： languages performance theory verification

来源：评论

学校读者我要写书评

暂无评论

A Type-theoretic Foundation for programming with Higher-order Abstract Syntax and First-class Substitutions

A Type-theoretic Foundation for Programming with Higher-orde...

引用

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

作者： Pientka, Brigitte McGill Univ Montreal PQ H3A 2T5 Canada

ISBN: (纸本)9781595936899

Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by representing binders in the object-language via binders in the meta-language. However, enriching functional programming languages with direct support for HOAS has been a major challenge, because recursion over HOAS encodings requires one to traverse lambda-abstractions and necessitates programming with open objects. We present a novel type-theoretic foundation based on contextual modal types which allows us to recursively analyze open terms via higher-order pattern matching. By design, variables occurring in open terms can never escape their scope. Using several examples, we demonstrate that our framework provides a name-safe foundation to operations typically found in nominal systems. In contrast to nominal systems however, we also support capture-avoiding substitution operations and even provide first-class substitutions to the programmer. The main contribution of this paper is a syntax-directed bi-directional type system where we distinguish between the data language and the computation language together with the progress and preservation proof for our language. © 2008 acm.

关键词： Type theory logical frameworks

来源：评论

学校读者我要写书评

暂无评论

High-Level Small-Step Operational Semantics for Transactions

High-Level Small-Step Operational Semantics for Transactions

引用

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

作者： Moore, Katherine F. Grossman, Dan Univ Washington Seattle WA 98195 USA

ISBN: (纸本)9781595936899

Software transactions have received significant attention as a way to simplify shared-memory concurrent programming, but insufficient focus has been given to the precise meaning of software transactions or their interaction with other language features. This work begins to rectify that situation by presenting a family of formal languages that model a wide variety of behaviors for software transactions. These languages abstract away implementation details of transactional memory, providing high-level definitions suitable for programming languages. We use small-step semantics in order to represent explicitly the interleaved execution of threads that is necessary to investigate pertinent issues. We demonstrate the value of our core approach to modeling transactions by investigating two issues in depth. First, we consider parallel nesting, in which parallelism and transactions can nest arbitrarily. Second, we present multiple models for weak isolation, in which nontransactional code can violate the isolation of a transaction. For both, type-and-effect systems let us soundly and statically restrict what computation can occur inside or outside a transaction. We prove some key language-equi valence theorems to confirm that under sufficient static restrictions, in particular that each mutable memory location is used outside transactions or inside transactions (but not both), no program can determine whether the language implementation uses weak isolation or strong isolation.

关键词： languages

来源：评论

学校读者我要写书评

暂无评论

Multiparty Asynchronous Session Types

Multiparty Asynchronous Session Types

引用

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

作者： Honda, Kohei Yoshida, Nobuko Carbone, Marco Univ London London WC1E 7HU England

ISBN: (纸本)9781595936899

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and programming languages, focussing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centred applications. Presented as a typed calculus for mobile processes. the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain a friendly type syntax of binary session types while capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety, progress and session fidelity are established for general n-party asynchronous interactions.

关键词： communications multiparty structured programming session types mobile processes causality choreography

来源：评论

学校读者我要写书评

暂无评论

A Theory of Platform-Dependent Low-Level Software

A Theory of Platform-Dependent Low-Level Software

引用

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

作者： Nita, Marius Grossman, Dan Chambers, Craig Univ Washington Dept Comp Sci & Engn Seattle WA 98195 USA

ISBN: (纸本)9781595936899

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions hold. Previous work on formalizing C-like languages has ignored this issue, either by assuming that programs do not make such assumptions or by assuming that all valid programs target only one platform. In the latter case, the platform's choices are hard-wired in the language semantics. In this paper, we present a practically-motivated model for a C-like language in which the memory layouts of types are left largely unspecified. The dynamic semantics is parameterized by a platform's layout policy and makes manifest the consequence of platform-dependent (i.e., unspecified) steps. A type-and-effect system produces a layout constraint: a logic formula encoding layout conditions under which the program is memory-safe. We prove that if a program type-checks, it is memory-safe on all platforms satisfying its constraint. Based on our theory, we have implemented a tool that discovers unportable layout assumptions in C programs. Our approach should generalize to other kinds of platform-dependent assumptions.

关键词： languages Verification Theory

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：