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

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

660 篇 会议
97 篇 期刊文献

馆藏范围

757 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

666 篇 工学
- 648 篇 软件工程
- 434 篇 计算机科学与技术...
- 20 篇 控制科学与工程
- 7 篇 信息与通信工程
- 3 篇 材料科学与工程（可...
- 3 篇 电子科学与技术（可...
- 2 篇 光学工程
- 1 篇 机械工程
- 1 篇 仪器科学与技术
- 1 篇 电气工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 化学工程与技术
- 1 篇 农业工程
170 篇 理学
- 167 篇 数学
- 8 篇 统计学（可授理学、...
- 2 篇 物理学
- 2 篇 系统科学
- 1 篇 化学
75 篇 管理学
- 55 篇 管理科学与工程(可...
- 22 篇 图书情报与档案管...
- 4 篇 工商管理
4 篇 法学
- 2 篇 法学
- 2 篇 社会学
1 篇 农学
- 1 篇 作物学

主题

234 篇 languages
153 篇 theory
121 篇 computer program...
106 篇 verification
53 篇 algorithms
48 篇 design
30 篇 computer program...
28 篇 object oriented ...
26 篇 reliability
23 篇 functional progr...
22 篇 high level langu...
22 篇 security
21 篇 performance
19 篇 programming theo...
19 篇 logic programmin...
18 篇 semantics
14 篇 computer systems...
14 篇 type systems
14 篇 concurrency
13 篇 separation logic

机构

15 篇 univ penn philad...
12 篇 carnegie mellon ...
11 篇 univ cambridge c...
11 篇 carnegie mellon ...
8 篇 princeton univ p...
7 篇 microsoft res re...
6 篇 inria rocquencou...
5 篇 inria
5 篇 univ of glasgow ...
5 篇 univ london impe...
5 篇 indiana univ blo...
5 篇 microsoft resear...
5 篇 microsoft resear...
5 篇 tel aviv univ il...
5 篇 university of pe...
5 篇 stanford univ st...
5 篇 univ london impe...
5 篇 cornell univ ith...
5 篇 univ edinburgh e...
4 篇 univ wisconsin m...

作者

11 篇 jones simon peyt...
11 篇 walker david
10 篇 leroy xavier
9 篇 pierce benjamin ...
9 篇 felleisen matthi...
9 篇 harper robert
9 篇 gordon andrew d.
9 篇 abadi martin
8 篇 cardelli luca
7 篇 palsberg jens
7 篇 sagiv mooly
7 篇 calcagno cristia...
7 篇 wadler philip
7 篇 morrisett greg
6 篇 riecke jon g.
6 篇 odersky martin
6 篇 hicks michael
6 篇 fournet cedric
6 篇 kobayashi naoki
5 篇 strub pierre-yve...

语言

690 篇 英文
61 篇 其他
6 篇 中文

检索条件"任意字段=ACM Singplan-sigact Symposium on Principles of Programming Languages"

共 757 条记录，以下是201-210 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

A Cost Semantics for Self-Adjusting Computation 09

A Cost Semantics for Self-Adjusting Computation

引用

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

作者： Ley-Wild, Ruy Acar, Umut A. Fluet, Matthew Carnegie Mellon Univ Pittsburgh PA 15213 USA Toyota Technol Inst Chicago IL USA

ISBN: (纸本)9781605583792

Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data by using a change-propagation mechanism that updates computation by re-building only the parts affected by changes. Previous work has proposed language techniques for self-adjusting computation and showed the approach to be effective in a number of application areas. However, due to the complex semantics of change propagation and the indirect nature of previously proposed language techniques, it remains difficult to reason about the efficiency of self-adjusting programs and change propagation. In this paper, we propose a cost semantics for self-adjusting computation that enables reasoning about its effectiveness. As our source language, we consider a direct-style lambda-calculus with first-class mutable references and develop a notion of trace distance for source programs. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concrete distances via trace contexts (traces with holes). We then show how to translate the source language into a self-adjusting target language such that the translation (1) preserves the extensional semantics of the source programs and the cost of from-scratch runs, and (2) ensures that change propagation between two evaluations takes time bounded by their relative distance. We consider several examples and analyze their effectiveness by considering upper and lower bounds.

关键词： languages Self-adjusting computation cost semantics

来源：评论

学校读者我要写书评

暂无评论

Compositional Shape Analysis by means of Bi-Abduction 09

Compositional Shape Analysis by means of Bi-Abduction

引用

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

作者： Calcagno, Cristiano Distefano, Dino O'Hearn, Peter Yang, Hongseok Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England Univ London London WC1E 7HU England

ISBN: (纸本)9781605583792

This paper describes a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure;the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits - increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision - to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger programs (e. g., an entire Linux distribution) to test scalability and graceful imprecision.

关键词： Verification Reliability languages Theory Program Analysis Proof Theory Abduction

来源：评论

学校读者我要写书评

暂无评论

Verifying Liveness for Asynchronous Programs 09

Verifying Liveness for Asynchronous Programs

引用

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

作者： Ganty, Pierre Majumdar, Rupak Rybalchenko, Andrey Univ Calif Los Angeles CS Dept Los Angeles CA 90024 USA

ISBN: (纸本)9781605583792

Asynchronous or "event-driven" programming is a popular technique to efficiently and flexibly manage concurrent interactions. In these programs, the programmer can post tasks that get stored in a task buffer and get executed atomically by a non-preemptive scheduler at a future point. We give a decision procedure for the fair termination property of asynchronous programs. The fair termination problem asks, given an asynchronous program and a fairness condition on its executions, does the program always terminate on fair executions? The fairness assumptions rule out certain undesired bad behaviors, such as where the scheduler ignores a set of posted tasks forever, or where a non-deterministic branch is always chosen in one direction. Since every liveness property reduces to a fair termination property, our decision procedure extends to liveness properties of asynchronous programs. Our decision procedure for the fair termination of asynchronous programs assumes all variables are finite-state. Even though variables are finite-state, asynchronous programs can have an unbounded stack from recursive calls made by tasks, as well as an unbounded task buffer of pending tasks. We show a reduction from the fair termination problem for asynchronous programs to fair termination problems on Petri Nets, and our main technical result is a reduction of the latter problem to Presburger satisfiability. Our decidability result is in contrast to multi-threaded recursive programs, for which liveness properties are undecidable. While we focus on fair termination, we show our reduction to Petri Nets can be used to prove related properties such as fair non-starvation (every posted task is eventually executed) and safety properties such as boundedness (find a bound on the maximum number of posted tasks that can be in the task buffer at any point).

关键词： languages Verification Reliability asynchronous (event-driven) programming liveness fair termination Petri Nets

来源：评论

学校读者我要写书评

暂无评论

Equality Saturation: a New Approach to Optimization 09

Equality Saturation: a New Approach to Optimization

引用

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

作者： Tate, Ross Stepp, Michael Tatlock, Zachary Lerner, Sorin Univ Calif San Diego Dept Comp Sci & Engn San Diego CA 92103 USA

ISBN: (纸本)9781605583792

Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to the next optimization. We present a new approach for structuring the optimization phase of a compiler. In our approach, optimizations take the form of equality analyses that add equality information to a common intermediate representation. The optimizer works by repeatedly applying these analyses to infer equivalences between program fragments, thus saturating the intermediate representation with equalities. Once saturated, the intermediate representation encodes multiple optimized versions of the input program. At this point, a profitability heuristic picks the final optimized program from the various programs represented in the saturated representation. Our proposed way of structuring optimizers has a variety of benefits over previous approaches: our approach obviates the need to worry about optimization ordering, enables the use of a global optimization heuristic that selects among fully optimized programs, and can be used to perform translation validation, even on compilers other than our own. We present our approach, formalize it, and describe our choice of intermediate representation. We also present experimental results showing that our approach is practical in terms of time and space overhead, is effective at discovering intricate optimization opportunities, and is effective at performing translation validation for a realistic optimizer.

关键词： languages Performance Compiler Optimization Equality Reasoning Intermediate Representation

来源：评论

学校读者我要写书评

暂无评论

Masked Types for Sound Object Initialization 09

Masked Types for Sound Object Initialization

引用

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

作者： Qi, Xin Myers, Andrew C. Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

ISBN: (纸本)9781605583792

This paper presents a type-based solution to the long-standing problem of object initialization. Constructors, the conventional mechanism for object initialization, have semantics that are surprising to programmers and that lead to bugs. They also contribute to the problem of null-pointer exceptions, which make software less reliable. Masked types are a new type-state mechanism that explicitly tracks the initialization state of objects and prevents reading from uninitialized fields. In the resulting language, constructors are ordinary methods that operate on uninitialized objects, and no special default value (null) is needed in the language. Initialization of cyclic data structures is achieved with the use of conditionally masked types. Masked types are modular and compatible with data abstraction. The type system is presented in a simplified object calculus and is proved to soundly prevent reading from uninitialized fields. Masked types have been implemented as an extension to Java, in which compilation simply erases extra type information. Experience using the extended language suggests that masked types work well on real code.

关键词： languages Reliability invariants null pointer exceptions conditional masks cyclic data structures data abstraction

来源：评论

学校读者我要写书评

暂无评论

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 2009年 iii页

作者： Pierce, Benjamin C. University of Pennsylvania

来源：评论

学校读者我要写书评

暂无评论

Feedback-Directed Barrier Optimization in a Strongly Isolated STM 09

Feedback-Directed Barrier Optimization in a Strongly Isolate...

引用

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

作者： Bronson, Nathan G. Kozyrakis, Christos Olukotun, Kunle Stanford Univ Comp Syst Lab Stanford CA 94305 USA

ISBN: (纸本)9781605583792

Speed improvements in today's processors have largely been delivered in the form of multiple cores, increasing the importance of abstractions that ease parallel programming. Software transactional memory (STM) addresses many of the complications of concurrency by providing a simple and composable model for safe access to shared data structures. Software transactions extend a language with an atomic primitive that declares that the effects of a block of code should not be interleaved with actions executing concurrently on other threads. Adding barriers to shared memory accesses provides atomicity, consistency and isolation. Strongly isolated STMs preserve the safety properties of transactions for all memory operations in a program, not just those inside an atomic block. Isolation barriers are added to non-transactional loads and stores in such a system to prevent those accesses from observing or corrupting a partially completed transaction. Strong isolation is especially important when integrating transactions into an existing language and memory model. Isolation barriers have a prohibitive performance overhead, however, so most STM proposals have chosen not to provide strong isolation. In this paper we reduce the costs of strong isolation by customizing isolation barriers for their observed usage. The customized barriers provide accelerated execution by blocking threads whose accesses do not follow the expected pattern. We use hot swap to tighten or loosen the hypothesized pattern, while preserving strong isolation. We introduce a family of optimization hypotheses that balance verification cost against generality. We demonstrate the feasibility of dynamic barrier optimization by implementing it in a bytecode-rewriting Java STM. Feedback-directed customization reduces the overhead of strong isolation from 505% to 38% across 11 non-transactional benchmarks;persistent feedback data further reduces the overhead to 16%. Dynamic optimization accelerates a multi-threaded t

关键词： Algorithms Design Experimentation languages Measurement Performance Transactional Memory Strong Isolation Weak Isolation Hot Swap Bytecode Rewriting Deoptimization

来源：评论

学校读者我要写书评

暂无评论

Modular Code Generation from Synchronous Block Diagrams Modularity vs. Code Size 09

Modular Code Generation from Synchronous Block Diagrams Modu...

引用

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

作者： Lublinerman, Roberto Szegedy, Christian Tripakis, Stavros Penn State Univ University Pk PA 16802 USA CNRS Verimag Lab F-75700 Paris France

ISBN: (纸本)9781605583792

We study modular, automatic code generation from hierarchical block diagrams with synchronous semantics. Such diagrams are the fundamental model behind widespread tools in the embedded software domain, such as Simulink and SCADE. Code is modular in the sense that it is generated for a given composite block independently from context (i.e., without knowing in which diagrams the block is to be used) and using minimal information about the internals of the block. In previous work, we have shown how modular code can be generated by computing a set of interface functions for each block and a set of dependencies between these functions that is exported along with the interface. We have also introduced a quantified notion of modularity in terms of the number of interface functions generated per block, and showed how to minimize this number, which is essential for scalability. Finally, we have exposed the fundamental trade-off between modularity and reusability (set of diagrams the block can be used in). In this paper we explore another trade-off: modularity vs. code size. We show that our previous technique, although it achieves maximal reusability and is optimal in terms of modularity, may result in code replication and therefore large code sizes, something often unacceptable in an embedded system context. We propose to remedy this by generating code with no replication, and show that this generally results in some loss of modularity. We show that optimizing modularity while maintaining maximal reusability and zero replication is an intractable problem (NP-complete). We also show that this problem can be solved using a simple iterative procedure that checks satisfiability of a sequence of propositional formulas. We report on a new prototype implementation and experimental results. The latter demonstrate the practical interest in our methods.

关键词： Algorithms Design languages Embedded software Block diagrams Synchronous languages Code generation Clustering NP-complete

来源：评论

学校读者我要写书评

暂无评论

A Foundation for Flow-Based Program Matching Using Temporal Logic and Model Checking 09

A Foundation for Flow-Based Program Matching Using Temporal ...

引用

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

作者： Brunel, Julien Doligez, Damien Hansen, Rene Rydhof Lawall, Julia L. Muller, Gilles Univ Copenhagen DIKU DK-1168 Copenhagen Denmark Aalborg Univ Dept Comp Sci Aalborg Denmark Ecole Mines Nantes Nantes France

ISBN: (纸本)9781605583792

Reasoning about program control-flow paths is an important functionality of a number of recent program matching languages and associated searching and transformation tools. Temporal logic provides a well-defined means of expressing properties of control-flow paths in programs, and indeed an extension of the temporal logic CTL has been applied to the problem of specifying and verifying the transformations commonly performed by optimizing compilers. Nevertheless, in developing the Coccinelle program transformation tool for performing Linux collateral evolutions in systems code, we have found that existing variants of CTL do not adequately support rules that transform subterms other than the ones matching an entire formula. Being able to transform any of the subterms of a matched term seems essential in the domain targeted by Coccinelle. In this paper, we propose an extension to CTL named CTL-VW (CTL with variables and witnesses) that is a suitable basis for the semantics and implementation of the Coccinelle's program matching language. Our extension to CTL includes existential quantification over program fragments, which allows metavariables in the program matching language to range over different values within different control-flow paths, and a notion of witnesses that record such existential bindings for use in the subsequent program transformation process. We formalize CTL-VW and describe its use in the context of Coccinelle. We then assess the performance of the approach in practice, using a transformation rule that fixes several reference count bugs in Linux code.

关键词： Algorithms languages Theory Program transformation bug finding program matching CTL model checking

来源：评论

学校读者我要写书评

暂无评论

State-Dependent Representation Independence 09

State-Dependent Representation Independence

引用

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

作者： Ahmed, Amal Dreyer, Derek Rossberg, Andreas TTI-C Chicago IL USA MPI-SWS Saarbrücken Germany

ISBN: (纸本)9781605583792

Mitchell's notion of representation independence is a particularly useful application of Reynolds' relational parametricity - two different implementations of an abstract data type can be shown contextually equivalent so long as there exists a relation between their type representations that is preserved by their operations. There have been a number of methods proposed for proving representation independence in various pure extensions of System F (where data abstraction is achieved through existential typing), as well as in Algol-or Java-like languages (where data abstraction is achieved through the use of local mutable state). However, none of these approaches addresses the interaction of existential type abstraction and local state. In particular, none allows one to prove representation independence results for generative ADTs - i.e., ADTs that both maintain some local state and define abstract types whose internal representations are dependent on that local state. In this paper, we present a syntactic, logical-relations-based method for proving representation independence of generative ADTs in a language supporting polymorphic types, existential types, general recursive types, and unrestricted ML-style mutable references. We demonstrate the effectiveness of our method by using it to prove several interesting contextual equivalences that involve a close interaction between existential typing and local state, as well as some well-known equivalences from the literature (such as Pitts and Stark's "awkward" example) that have caused trouble for previous logical-relations-based methods. The success of our method relies on two key technical innovations. First, in order to handle generative ADTs, we develop a possible-worlds model in which relational interpretations of types are allowed to grow over time in a manner that is tightly coupled with changes to some local state. Second, we employ a step-indexed stratification of possible worlds, which facilitates a simplified

关键词： languages Theory Verification Abstract data types representation independence existential types local state step-indexed logical relations

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共76页 << < 17 18 19 20 21 22 23 24 25 26 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：