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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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 条记录，以下是331-340 订阅

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

详细简洁

排序：

Connecting effect and uniqueness with adoption

Connecting effect and uniqueness with adoption

引用

POPL 2005: The 32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Boyland, John Tang Retert, William University of Wisconsin - Milwaukee Department of EECS P O Box 784 Milwaukee WI 53201 United States

"Adoption" is when one piece of state is logically embedded in another piece of state. Adoption provides information hiding (the adopter can be used as a proxy for the adoptee) and with linear existentials, provides a way to store unique pointers in shared state. In this paper, we give an operational semantics of adoption in a simple procedural language with pointers to records. We define a "permission" type-system that uses adoption to model both effects and uniqueness. We prove type soundness (well-typed programs don't go wrong) and state separation (separately-typed statements cannot access the same state). Then we show how high-level effects and uniqueness annotations can be expressed in the type-system. The distinction between read and write effects is ignored in the body of this paper. Copyright 2005 acm.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Associated types with class 05

Associated types with class

引用

POPL 2005: The 32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Chakravarty, Manuel M.T. Keller, Gabriele Jones, Simon Peyton Marlow, Simon Programming Languages and Compilers University of New South Wales Australia Microsoft Research Ltd. Cambridge United Kingdom

ISBN: (纸本)9781581138306

Haskell's type classes allow ad-hoc overloading, or type-indexing, of functions. A natural generalisation is to allow type-indexing of data types as well. It turns out that this idea directly supports a powerful form of abstraction called associated types, which are available in C++ using traits classes. Associated types are useful in many applications, especially for self-optimising libraries that adapt their data representations and algorithms in a type-directed manner. In this paper, we introduce and motivate associated types as a rather natural generalisation of Haskell's existing type classes. Formally, we present a type system that includes a type-directed translation into an explicitly typed target language akin to System F;the existence of this translation ensures that the addition of associated data types to an existing Haskell compiler only requires changes to the front end. Copyright 2005 acm.

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

A bisimulation for type abstraction and recursion

A bisimulation for type abstraction and recursion

引用

32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Sumii, E Pierce, BC Univ Penn Philadelphia PA 19104 USA

We present a sound;complete;and elementary proof method, based on bisimulation, for contextual equivalence in a lambda-calculus with full universal;existential;and recursive types. Unlike logical relations (either semantic or syntactic), our development is elementary;using only sets and relations and avoiding advanced machinery such as domain theory;admissibility;and TT-closure. Unlike other bisimulations;ours is complete even for existential types. The key idea is to consider sets of relations-instead of just relations-as bisimulations.

关键词： theory languages lambda-calculus contextual equivalence bisimulations logical relations existential types recursive types

来源：评论

学校读者我要写书评

暂无评论

A syntactic approach to eta equality in type theory 05

A syntactic approach to eta equality in type theory

引用

32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Goguen, H AT&T Labs Florham Pk NJ 07932 USA

ISBN: (纸本)9781581138306

This paper outlines an elementary approach for showing the decidability of type checking for type theories with beta eta-equality;relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic translation trapping terms in the beta eta presentation into their full eta-expansions in the beta presentation. Decidability of type checking is lifted from the target beta presentation to the beta eta presentation. The approach extends to other inductive kinds with a single constructor, and is demonstrated for singletons and dependent pairs.

关键词： theory languages logical frameworks type checking decidability beta-eta equality

来源：评论

学校读者我要写书评

暂无评论

Automated soundness proofs for dataflow analyses and transformations via local rules 05

Automated soundness proofs for dataflow analyses and transfo...

引用

POPL 2005: The 32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Lerner, Sorin Rice, Erika Millstein, Todd Chambers, Craig Univ. of Washington United States UCLA United States

ISBN: (纸本)9781581138306

We present Rhodium, a new language for writing compiler optimizations that can be automatically proved sound. Unlike our previous work on Cobalt, Rhodium expresses optimizations using explicit dataflow facts manipulated by local propagation and transformation rules. This new style allows Rhodium optimizations to be mutually recursively defined, to be automatically composed, to be interpreted in both flow-sensitive and -insensitive ways, and to be applied interprocedurally given a separate context-sensitivity strategy, all while retaining soundness. Rhodium also supports infinite analysis domains while guaranteeing termination of analysis. We have implemented a soundness checker for Rhodium and have specified and automatically proven the soundness of all of Cobalt's optimizations plus a variety of optimizations not expressible in Cobalt, including Andersen's points-to analysis, arithmetic-invariant detection, loop-induction-variable strength reduction, and redundant array load elimination. Copyright 2005 acm.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Associated types with class

Associated types with class

引用

32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Chakravarty, MMT Keller, G Jones, SP Marlow, S Univ New S Wales Kensington NSW 2033 Australia Microsoft Res Ltd Cambridge England

Haskell's type classes allow ad-hoc overloading, or type-indexing;of functions. A natural generalisation is to allow type-indexing of data types as well. It turns out that this idea directly supports a powerful form of abstraction called associated types;which are available in C++ using traits classes. Associated types are useful in many applications, especially for self-optimising libraries that adapt their data representations and algorithms in a type-directed manner.

关键词： design languages theory type classes type-indexed types associated types type-directed translation self-optimising libraries

来源：评论

学校读者我要写书评

暂无评论

Theoretical foundations for compensations in flow composition languages 05

Theoretical foundations for compensations in flow compositio...

引用

32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Bruni, R Melgratti, H Montanari, U Univ Pisa Dipartimento Informat I-56100 Pisa Italy

ISBN: (纸本)9781581138306

A key aspect when aggregating business processes and web services is to assure transactional properties of process executions. Since transactions in this context may require long periods of time to complete;traditional mechanisms for guaranteeing atomicity are not always appropriate. Generally the concept of long running transactions relies on a weaker notion of atomicity based on compensations. For this reason;programming languages for service composition cannot leave out two key aspects: compensations, i.e. ad hoc activities that can undo the effects of a process that fails to complete, and transactional boundaries to delimit the scope of a transactional flow. This paper presents a hierarchy of transactional calculi with increasing expressiveness. We start from a very small language in which activities can only be composed sequentially. Then;we progressively introduce parallel composition;nesting;programmable compensations and exception handling. A running example illustrates the main features of each calculus in the hierarchy.

关键词： languages theory transactions compensations process description languages

来源：评论

学校读者我要写书评

暂无评论

Transactors: A programming model for maintaining globally consistent distributed in unreliable environments

Transactors: A programming model for maintaining globally co...

引用

POPL 2005: The 32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Field, John Varela, Carlos A. IBM T.J. Watson Research Center Department of Computer Science Rensselaer Polytechnic Institute

We introduce transactors, a fault-tolerant programming model for composing loosely-coupled distributed components running in an unreliable environment such as the internet into systems that reliably maintain globally consistent distributed state. The transactor model incorporates certain elements of traditional transaction processing, but allows these elements to be composed in different ways without the need for central coordination, thus facilitating the study of distributed fault-tolerance from a semantic point of view. We formalize our approach via the τ-calculus, an extended lambda-calculus based on the actor model, and illustrate its usage through a number of examples. The τ-calculus incorporates constructs which distributed processes can use to create globally-consistent check-points. We provide an operational semantics for the τ-calculus, and formalize the following safety and liveness properties: first, we show that globally-consistent checkpoints have equivalent execution traces without any node failures or application-level failures, and second, we show that it is possible to reach globally-consistent checkpoints provided that there is some bounded failure-free interval during which checkpointing can occur. Copyright 2005 acm.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Transition predicate abstraction and fair termination 05

Transition predicate abstraction and fair termination

引用

32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Podelski, A Rybalchenko, A Max Planck Inst Informat Saarbrucken Germany

ISBN: (纸本)9781581138306

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to transition predicate abstraction. Transition predicate abstraction goes beyond the idea of finite abstract-state programs (and checking the absence of loops). Instead, our abstraction algorithm transforms a program into a finite abstract-transition program. Then, a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (justice and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties.

关键词： languages theory verification software model checking transition predicate abstraction fair termination liveness

来源：评论

学校读者我要写书评

暂无评论

Communicating quantum processes 05

Communicating quantum processes

引用

POPL 2005: The 32nd acm SIGPLAN-sigact symposium on principles of programming languages

作者： Gay, Simon J. J. Nagarajan, Rajagopal Department of Computing Science University of Glasgow United Kingdom Department of Computer Science University of Warwick United Kingdom

ISBN: (纸本)9781581138306

We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state;in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems. Copyright 2005 acm.

关键词： Formal languages

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共76页 << < 30 31 32 33 34 35 36 37 38 39 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：