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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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

分类表

所选分类

>> <<

限定检索结果

文献类型

278 篇 会议
40 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

274 篇 工学
- 267 篇 软件工程
- 140 篇 计算机科学与技术...
- 7 篇 电气工程
- 3 篇 生物工程
- 2 篇 信息与通信工程
- 2 篇 控制科学与工程
- 1 篇 动力工程及工程热...
- 1 篇 电子科学与技术（可...
- 1 篇 化学工程与技术
- 1 篇 纺织科学与工程
- 1 篇 生物医学工程（可授...
10 篇 理学
- 8 篇 数学
- 1 篇 化学
- 1 篇 地质学
- 1 篇 生物学
6 篇 管理学
- 3 篇 管理科学与工程(可...
- 3 篇 图书情报与档案管...
2 篇 农学
- 2 篇 作物学
1 篇 教育学
- 1 篇 教育学

主题

80 篇 design
73 篇 languages
32 篇 performance
17 篇 verification
16 篇 algorithms
14 篇 reliability
14 篇 probabilistic pr...
13 篇 object oriented ...
13 篇 program synthesi...
13 篇 domain-specific ...
13 篇 functional progr...
11 篇 java
10 篇 experimentation
10 篇 programming lang...
9 篇 type systems
9 篇 theory
9 篇 concurrency
7 篇 compilers
7 篇 optimization
6 篇 modules

机构

9 篇 carnegie mellon ...
8 篇 purdue univ w la...
6 篇 princeton univ p...
5 篇 northeastern uni...
5 篇 yale univ new ha...
5 篇 harvard univ cam...
5 篇 cornell univ ith...
5 篇 univ washington ...
5 篇 univ calif berke...
4 篇 univ wisconsin m...
4 篇 univ calif davis...
4 篇 univ utah salt l...
4 篇 univ penn philad...
4 篇 rice univ housto...
4 篇 univ chicago il ...
4 篇 stanford univ st...
4 篇 univ texas austi...
3 篇 mit csail cambri...
3 篇 univ cambridge c...
3 篇 microsoft res re...

作者

7 篇 walker david
6 篇 foster nate
5 篇 shao zhong
5 篇 gulwani sumit
5 篇 dillig isil
4 篇 rainey mike
4 篇 gu ronghui
4 篇 rompf tiark
4 篇 solar-lezama arm...
4 篇 chaudhuri swarat
4 篇 myers andrew c.
4 篇 wansbrough keith
3 篇 hirschfeld rober...
3 篇 flatt matthew
3 篇 rajamani sriram
3 篇 seshia sanjit a.
3 篇 rajan hridesh
3 篇 huang jeff
3 篇 liu yu david
3 篇 vechev martin

语言

283 篇 英文
34 篇 其他
1 篇 中文

检索条件"任意字段=37th ACM SIGPLAN Conference on Programming Language Design and Implementation"

共 318 条记录，以下是111-120 订阅

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

详细简洁

排序：

Incremental Inference for Probabilistic Programs 2018

Incremental Inference for Probabilistic Programs

引用

39th acm sigplan conference on programming language design and implementation (PLDI)

作者： Cusumano-Towner, Marco Bichsel, Benjamin Gehr, Timon Vechev, Martin Mansinghka, Vikash K. MIT 77 Massachusetts Ave Cambridge MA 02139 USA Swiss Fed Inst Technol Zurich Switzerland

ISBN: (纸本)9781450356985

We present a novel approach for approximate sampling in probabilistic programs based on incremental inference. the key idea is to adapt the samples for a program P into samples for a program Q, thereby avoiding the expensive sampling computation for program Q. To enable incremental inference in probabilistic programming, our work: (i) introduces the concept of a trace translator which adapts samples from P into samples of Q, (ii) phrases this translation approach in the context of sequential Monte Carlo (SMC), which gives theoretical guarantees that the adapted samples converge to the distribution induced by Q, and (iii) shows how to obtain a concrete trace translator by establishing a correspondence between the random choices of the two probabilistic programs. We implemented our approach in two different probabilistic programming systems and showed that, compared to methods that sample the program Q from scratch, incremental inference can lead to orders of magnitude increase in efficiency, depending on how closely related P and Q are.

关键词： Probabilistic programming sequential Monte Carlo incremental computation

来源：评论

学校读者我要写书评

暂无评论

Halide: A language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines

Halide: A Language and Compiler for Optimizing Parallelism, ...

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Ragan-Kelley, Jonathan Barnes, Connelly Adams, Andrew Paris, Sylvain Durand, Fredo Amarasinghe, Saman MIT CSAIL United States Adobe United States

ISBN: (纸本)9781450320146

Image processing pipelines combine the challenges of stencil computations and stream programs. they are composed of large graphs of different stencil stages, as well as complex reductions, and stages with global or data-dependent access patterns. Because of their complex structure, the performance difference between a naive implementation of a pipeline and an optimized one is often an order of magnitude. Efficient implementations require optimization of both parallelism and locality, but due to the nature of stencils, there is a fundamental tension between parallelism, locality, and introducing redundant recomputation of shared values. We present a systematic model of the tradeoff space fundamental to stencil pipelines, a schedule representation which describes concrete points in this space for each stage in an image processing pipeline, and an optimizing compiler for the Halide image processing language that synthesizes high performance implementations from a Halide algorithm and a schedule. Combining this compiler with stochastic search over the space of schedules enables terse, composable programs to achieve state-of-the-art performance on a wide range of real image processing pipelines, and across different hardware architectures, including multicores with SIMD, and heterogeneous CPU+GPU execution. From simple Halide programs written in a few hours, we demonstrate performance up to 5x faster than hand-tuned C, intrinsics, and CUDA implementations optimized by experts over weeks or months, for image processing applications beyond the reach of past automatic compilers.

关键词： domain specific language compiler image processing locality parallelism redundant computation optimization GPU vectorization

来源：评论

学校读者我要写书评

暂无评论

Symbolic Reasoning for Automatic Signal Placement 2018

Symbolic Reasoning for Automatic Signal Placement

引用

39th acm sigplan conference on programming language design and implementation (PLDI)

作者： Ferles, Kostas Van Geffen, Jacob Dillig, Isil Smaragdakis, Yannis Univ Texas Austin Austin TX 78712 USA Univ Athens Athens Greece

ISBN: (纸本)9781450356985

Explicit signaling between threads is a perennial cause of bugs in concurrent programs. While there are several runtime techniques to automatically notify threads upon the availability of some shared resource, such techniques are not widely-adopted due to their run-time overhead. this paper proposes a new solution based on static analysis for automatically generating a performant explicit-signal program from its corresponding implicit-signal implementation. the key idea is to generate verification conditions that allow us to minimize the number of required signals and unnecessary context switches, while guaranteeing semantic equivalence between the source and target programs. We have implemented our method in a tool called Expresso and evaluate it on challenging benchmarks from prior papers and open-source software. Expresso-generated code significantly outperforms past automatic signaling mechanisms (avg. 1.56x speedup) and closely matches the performance of hand-optimized explicit-signal code.

关键词： Implicit signal monitors concurrent programming symbolic reasoning verification conditions abductive reasoning monitor invariant

来源：评论

学校读者我要写书评

暂无评论

A new perspective on processing-in-memory architecture design 13

A new perspective on processing-in-memory architecture desig...

引用

acm sigplan Workshop on Memory Systems Performance and Correctness, MSPC 2013, co-located with the 34th annual acm sigplan conference on programming language design and implementation, PLDI

作者： Zhang, Dong Ping Jayasena, Nuwan Lyashevsky, Alexander Greathouse, Joseph Meswani, Mitesh Nutter, Mark Ignatowski, Mike Research Group AMD CA United States

ISBN: (纸本)9781450321037

As computation becomes increasingly limited by data movement and energy consumption, exploiting locality throughout the memory hierarchy becomes critical for maintaining the performance scaling that many have come to expect from the computing industry. Moving computation closer to main memory presents an opportunity to reduce the overheads associated with data movement. We explore the potential of using 3D die stacking to move memory-intensive computations closer to memory. this approach to processing-in-memory addresses some drawbacks of prior research on in-memory computing and appears commercially viable in the foreseeable future. We show promising early results from this approach and identify areas that are in need of research to unlock its full potential. © 2013 acm.

关键词： Memory architecture

来源：评论

学校读者我要写书评

暂无评论

programming with Binders and Indexed Data-Types 12

Programming with Binders and Indexed Data-Types

引用

39th Annual acm sigplan-SIGACT Symposium on Principles of programming languages

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

ISBN: (纸本)9781450310833

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. this allows the user to specify formal systems within the logical framework LF and index ML types with contextual LF objects. Our language design keeps the index language generic only requiring decidability of equality of the index language providing a modular design. To illustrate the elegance and effectiveness of our language, we give programs for closure conversion and normalization by evaluation. Our three key technical contribution are: 1) We give a bidirectional type system for our core language which is centered around refinement substitutions instead of constraint solving. As a consequence, type checking is decidable and easy to trust, although constraint solving may be undecidable. 2) We give a big-step environment based operational semantics with environments which lends itself to efficient implementation. 3) We prove our language to be type safe and have mechanized our theoretical development in the proof assistant Coq using the fresh approach to binding.

关键词： Logical frameworks higher-order abstract syntax dependent types recursive types

来源：评论

学校读者我要写书评

暂无评论

Bounded Expectations: Resource Analysis for Probabilistic Programs 2018

Bounded Expectations: Resource Analysis for Probabilistic Pr...

引用

39th acm sigplan conference on programming language design and implementation (PLDI)

作者： Van Chan Ngo Carbonneaux, Quentin Hoffmann, Jan Carnegie Mellon Univ Pittsburgh PA 15213 USA Yale Univ New Haven CT 06520 USA

ISBN: (纸本)9781450356985

this paper presents a new static analysis for deriving upper bounds on the expected resource consumption of probabilistic programs. the analysis is fully automatic and derives symbolic bounds that are multivariate polynomials in the inputs. the new technique combines manual state-of-the-art reasoning techniques for probabilistic programs with an effective method for automatic resource-bound analysis of deterministic programs. It can be seen as both, an extension of automatic amortized resource analysis (AARA) to probabilistic programs and an automation of manual reasoning for probabilistic programs that is based on weakest preconditions. An advantage of the technique is that it combines the clarity and compositionality of a weakest-precondition calculus with the efficient automation of AARA. As a result, bound inference can be reduced to off-the-shelf LP solving in many cases and automatically-derived bounds can be interactively extended with standard program logics if the automation fails. Building on existing work, the soundness of the analysis is proved with respect to an operational semantics that is based on Markov decision processes. the effectiveness of the technique is demonstrated with a prototype implementation that is used to automatically analyze 39 challenging probabilistic programs and randomized algorithms. Experiments indicate that the derived constant factors in the bounds are very precise and even optimal for some programs.

关键词： probabilistic programming resource bound analysis static analysis

来源：评论

学校读者我要写书评

暂无评论

Heartbeat Scheduling: Provable Efficiency for Nested Parallelism 2018

Heartbeat Scheduling: Provable Efficiency for Nested Paralle...

引用

39th acm sigplan conference on programming language design and implementation (PLDI)

作者： Acar, Umut A. Chargueraud, Arthur Guatto, Adrien Rainey, Mike Sieczkowski, Filip Carnegie Mellon Univ Pittsburgh PA 15213 USA INRIA Rocquencourt France Univ Strasbourg ICube Strasbourg France CREST Bloomington IN USA

ISBN: (纸本)9781450356985

A classic problem in parallel computing is to take a high-level parallel program written, for example, in nested-parallel style with fork-join constructs and run it efficiently on a real machine. the problem could be considered solved in theory, but not in practice, because the overheads of creating and managing parallel threads can overwhelm their benefits. Developing efficient parallel codes therefore usually requires extensive tuning and optimizations to reduce parallelism just to a point where the overheads become acceptable. In this paper, we present a scheduling technique that delivers provably efficient results for arbitrary nested-parallel programs, without the tuning needed for controlling parallelism overheads. the basic idea behind our technique is to create threads only at a beat (which we refer to as the "heartbeat") and make sure to do useful work in between. We specify our heartbeat scheduler using an abstract-machine semantics and provide mechanized proofs that the scheduler guarantees low overheads for all nested parallel programs. We present a prototype C++ implementation and an evaluation that shows that Heartbeat competes well with manually optimized Cilk Plus codes, without requiring manual tuning.

关键词： parallel programming languages granularity control

来源：评论

学校读者我要写书评

暂无评论

LoCal: A language for Programs Operating on Serialized Data 2019

LoCal: A Language for Programs Operating on Serialized Data

引用

40th acm sigplan conference on programming language design and implementation (PLDI) part of acm's Federated Computing Research conference (FCRC)

作者： Vollmer, Michael Koparkar, Chaitanya Rainey, Mike Sakka, Laith Kulkarni, Milind Newton, Ryan R. Indiana Univ Comp Sci Bloomington IN 47405 USA Purdue Univ Elect & Comp Engn W Lafayette IN 47907 USA

ISBN: (纸本)9781450367127

In a typical data-processing program, the representation of data in memory is distinct from its representation in a serialized form on disk. the former has pointers and arbitrary, sparse layout, facilitating easy manipulation by a program, while the latter is packed contiguously, facilitating easy I/O. We propose a language, LoCal, to unify in-memory and serialized formats. LoCal extends a region calculus into a location calculus, employing a type system that tracks the byte-addressed layout of all heap values. We formalize LoCal and prove type safety, and show how LoCal programs can be inferred from unannotated source terms. We transform the existing Gibbon compiler to use LoCal as an intermediate language, with the goal of achieving a balance between code speed and data compactness by introducing just enough indirection into heap layouts, preserving the asymptotic complexity of traditional representations, but working with mostly or completely serialized data. We show that our approach yields significant performance improvement over prior approaches to operating on packed data, without abandoning idiomatic programming with recursive functions.

关键词： Region Calculus Compiler Optimization Data Encoding Tree Traversal

来源：评论

学校读者我要写书评

暂无评论

Concurrency Debugging with Differential Schedule Projections 15

Concurrency Debugging with Differential Schedule Projections

引用

36th acm sigplan conference on programming language design and implementation

作者： Machado, Nuno Lucia, Brandon Rodrigues, Luis Univ Lisbon Inst Super Tecn INESC ID P-1699 Lisbon Portugal Carnegie Mellon Univ Pittsburgh PA 15213 USA

ISBN: (纸本)9781450334686

We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% fewer data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events, DSPs reduce the amount of time required to find a valid fix.

关键词： Algorithms design Reliability Concurrency Debugging Symbolic Execution Constraint Solving Differential Schedule Projection

来源：评论

学校读者我要写书评

暂无评论

TRANSIT: Specifying Protocols with Concolic Snippets

TRANSIT: Specifying Protocols with Concolic Snippets

引用

34th acm sigplan conference on programming language design and implementation (PLDI)

作者： Udupa, Abhishek Raghavan, Arun Deshmukh, Jyotirmoy V. Mador-Haim, Sela Martin, Milo M. K. Alur, Rajeev Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781450320146

With the maturing of technology for model checking and constraint solving, there is an emerging opportunity to develop programming tools that can transform the way systems are specified. In this paper, we propose a new way to program distributed protocols using concolic snippets. Concolic snippets are sample execution fragments that contain both concrete and symbolic values. the proposed approach allows the programmer to describe the desired system partially using the traditional model of communicating extended finite-state-machines (EFSM), along with high-level invariants and concrete execution fragments. Our synthesis engine completes an EFSM skeleton by inferring guards and updates from the given fragments which is then automatically analyzed using a model checker with respect to the desired invariants. the counterexamples produced by the model checker can then be used by the programmer to add new concrete execution fragments that describe the correct behavior in the specific scenario corresponding to the counterexample. We describe TRANSIT, a language and prototype implementation of the proposed specification methodology for distributed protocols. Experimental evaluations of TRANSIT to specify cache coherence protocols show that (1) the algorithm for expression inference from concolic snippets can synthesize expressions of size 15 involving typical operators over commonly occurring types, (2) for a classical directory-based protocol, TRANSIT automatically generates, in a few seconds, a complete implementation from a specification consisting of the EFSM structure and a few concrete examples for every transition, and (3) a published partial description of the SGI Origin cache coherence protocol maps directly to symbolic examples and leads to a complete implementation in a few iterations, with the programmer correcting counterexamples resulting from underspecified transitions by adding concrete examples in each iteration.

关键词： Program Synthesis Distributed Protocol Synthesis Cache Coherence Protocols programming by Example

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共32页 << < 8 9 10 11 12 13 14 15 16 17 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：