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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

800 篇 会议
131 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

823 篇 工学
- 807 篇 软件工程
- 547 篇 计算机科学与技术...
- 22 篇 控制科学与工程
- 11 篇 信息与通信工程
- 7 篇 电气工程
- 5 篇 电子科学与技术（可...
- 4 篇 化学工程与技术
- 3 篇 机械工程
- 2 篇 材料科学与工程（可...
- 2 篇 建筑学
- 2 篇 交通运输工程
- 2 篇 安全科学与工程
- 1 篇 光学工程
- 1 篇 冶金工程
- 1 篇 动力工程及工程热...
- 1 篇 土木工程
- 1 篇 纺织科学与工程
102 篇 理学
- 88 篇 数学
- 10 篇 系统科学
- 8 篇 统计学（可授理学、...
- 4 篇 化学
- 2 篇 物理学
- 2 篇 生物学
- 1 篇 地质学
53 篇 管理学
- 35 篇 管理科学与工程(可...
- 21 篇 工商管理
- 21 篇 图书情报与档案管...
5 篇 经济学
- 5 篇 应用经济学
4 篇 教育学
- 4 篇 教育学
3 篇 法学
- 3 篇 社会学

主题

166 篇 design
155 篇 languages
96 篇 performance
74 篇 computer program...
56 篇 algorithms
45 篇 experimentation
42 篇 computer program...
39 篇 verification
36 篇 reliability
34 篇 object oriented ...
27 篇 java programming...
26 篇 functional progr...
25 篇 program synthesi...
24 篇 probabilistic pr...
22 篇 java
19 篇 domain-specific ...
19 篇 theory
19 篇 concurrency
17 篇 compilers
17 篇 type systems

机构

15 篇 carnegie mellon ...
13 篇 princeton univ p...
11 篇 univ texas austi...
10 篇 univ michigan an...
10 篇 rice univ housto...
10 篇 purdue univ w la...
10 篇 univ washington ...
10 篇 univ calif berke...
9 篇 univ wisconsin m...
9 篇 harvard univ cam...
9 篇 univ penn philad...
9 篇 stanford univ st...
8 篇 yale univ new ha...
8 篇 cornell univ ith...
8 篇 univ chicago il ...
7 篇 mit cambridge ma...
7 篇 northeastern uni...
7 篇 microsoft resear...
6 篇 microsoft res re...
6 篇 microsoft res re...

作者

11 篇 walker david
10 篇 dillig isil
9 篇 chlipala adam
8 篇 solar-lezama arm...
8 篇 chaudhuri swarat
7 篇 august david i.
7 篇 shao zhong
7 篇 gulwani sumit
7 篇 sarkar vivek
6 篇 wang xinyu
6 篇 grossman dan
6 篇 adl-tabatabai al...
6 篇 aiken alex
6 篇 foster nate
6 篇 bacon david f.
6 篇 myers andrew c.
6 篇 mezini mira
6 篇 mahlke scott
6 篇 bodik rastislav
5 篇 mckinley kathryn...

语言

852 篇 英文
78 篇 其他
1 篇 中文

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

共 931 条记录，以下是281-290 订阅

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

详细简洁

排序：

Persistency for Synchronization-Free Regions 2018

Persistency for Synchronization-Free Regions

引用

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

作者： Gogte, Vaibhav Diestelhorst, Stephan Wang, William Narayanasamy, Satish Chen, Peter M. Wenisch, Thomas F. Univ Michigan Ann Arbor MI 48109 USA Arm Res Cambridge England

ISBN: (纸本)9781450356985

Nascent persistent memory (PM) technologies promise the performance of DRAM with the durability of disk, but how best to integrate them into programming systems remains an open question. Recent work extends language memory models with a persistency model prescribing semantics for updates to PM. These semantics enable programmers to design data structures in PM that are accessed like memory and yet are recoverable upon crash or failure. Alas, we find the semantics and performance of existing approaches unsatisfying. Existing approaches require high-overhead mechanisms, are restricted to certain synchronization constructs, provide incomplete semantics, and/or may recover to state that cannot arise in fault-free execution. We propose persistency semantics that guarantee failure atomicity of synchronization-free regions (SFRs) -program regions delimited by synchronization operations. Our approach provides clear semantics for the PM state recovery code may observe and extends C++11's "sequential consistency for data-race-free" guarantee to post-failure recovery code. We investigate two designs for failure-atomic SFRs that vary in performance and the degree to which commit of persistent state may lag execution. We demonstrate both approaches in LLVM v3.6.0 and compare to a state-of-the-art baseline to show performance improvement up to 87.5% (65.5% avg).

关键词： Persistent memories persistency models language memory models failure-atomicity synchronization-free regions

来源：评论

学校读者我要写书评

暂无评论

Spatial: A language and Compiler for Application Accelerators 2018

Spatial: A Language and Compiler for Application Accelerator...

引用

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

作者： Koeplinger, David Feldman, Matthew Prabhakar, Raghu Zhang, Yaqi Hadjis, Stefan Fiszel, Ruben Zhao, Tian Nardi, Luigi Pedram, Ardavan Kozyrakis, Christos Olukotun, Kunle Stanford Univ Stanford CA 94305 USA Ecole Polytech Fed Lausanne Lausanne Switzerland

ISBN: (纸本)9781450356985

Industry is increasingly turning to reconfigurable architectures like FPGAs and CGRAs for improved performance and energy efficiency. Unfortunately, adoption of these architectures has been limited by their programming models. HDLs lack abstractions for productivity and are difficult to target from higher level languages. HLS tools are more productive, but offer an ad-hoc mix of software and hardware abstractions which make performance optimizations difficult. In this work, we describe a new domain-specific language and compiler called Spatial for higher level descriptions of application accelerators. We describe Spatial's hardware-centric abstractions for both programmer productivity and design performance, and summarize the compiler passes required to support these abstractions, including pipeline scheduling, automatic memory banking, and automated design tuning driven by active machine learning. We demonstrate the language's ability to target FPGAs and CGRAs from common source code. We show that applications written in Spatial are, on average, 42% shorter and achieve a mean speedup of 2.9x over SDAccel HLS when targeting a Xilinx UltraScale+ VU9P FPGA on an Amazon EC2 F1 instance.

关键词： domain-specific languages compilers hardware accelerators high-level synthesis reconfigurable architectures FPGAs CGRAs

来源：评论

学校读者我要写书评

暂无评论

Fast breakpoints. design and implementation 90

Fast breakpoints. Design and implementation

引用

Proceedings of the acm sigplan '90 conference on programming language design and implementation

作者： Kessler, Peter B. Xerox PARC Palo Alto United States

ISBN: (纸本)0897913647

We have designed and implemented a fast breakpoint facility. Breakpoints are usually thought of as a feature of an interactive debugger, in which case the breakpoints need not be particularly fast. In our environment breakpoints are often used for non-interactive information gathering;for example, procedure call count and statement execution count profiling. When used non-interactively, breakpoints should be as fast as possible, so as to perturb the execution of the program as little as possible. Even in interactive debuggers, a conditional breakpoint facility would benefit from breakpoints that could transfer to the evaluation of the condition rapidly, and continue expeditiously if the condition were not satisfied. Such conditional breakpoints could be used to check assertions, etc. Program advising could also make use of fast breakpoints. Examples of advising include tracing, timing, and even animation, all of which should be part of an advanced programming environment.

关键词： Computer Operating Systems

来源：评论

学校读者我要写书评

暂无评论

Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic 11

Mostly-Automated Verification of Low-Level Programs in Compu...

引用

32nd acm sigplan conference on programming language design and implementation (PLDI 11)

作者： Chlipala, Adam Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781450306638

Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems. The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is computational, in the sense that function specifications are usually written in terms of reference implementations in a purely functional language. Logical quantifiers are the most challenging feature for most automated verifiers;by relying on functional programs (written in the expressive language of the Coq proof assistant), we are able to avoid quantifiers almost entirely. This leads to some dramatic improvements compared to both past work in classical verification, which we compare against with implementations of data structures like binary search trees and hash tables;and past work in verified programming with code pointers, which we compare against with examples like function memoization and a cooperative threading library.

关键词： interactive proof assistants separation logic low-level programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

Lightweight, Flexible Object-Oriented Generics 15

Lightweight, Flexible Object-Oriented Generics

引用

36th acm sigplan conference on programming language design and implementation

作者： Zhang, Yizhou Loring, Matthew C. Salvaneschi, Guido Liskov, Barbara Myers, Andrew C. Cornell Univ Ithaca NY 14853 USA Tech Univ Darmstadt Darmstadt Germany MIT Cambridge MA 02139 USA

ISBN: (纸本)9781450334686

The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens static checking, while remaining lightweight and simple in common use cases. Like type classes and concepts, the mechanism allows existing types to model type constraints retroactively. For expressive power, we expose models as named constructs that can be defined and selected explicitly to witness constraints;in common uses of genericity, however, types implicitly witness constraints without additional programmer effort. Models are integrated into the object-oriented style, with features like model generics, model-dependent types, model enrichment, model multimethods, constraint entailment, model inheritance, and existential quantification further extending expressive power in an object-oriented setting. We introduce the new genericity features and show that common generic programming idioms, including current generic libraries, can be expressed more precisely and concisely. The static semantics of the mechanism and a proof of a key decidability property can be found in an associated technical report.

关键词： Genus generic programming constraints models

来源：评论

学校读者我要写书评

暂无评论

Gillian, Part I: A Multi-language Platform for Symbolic Execution 2020

Gillian, Part I: A Multi-language Platform for Symbolic Exec...

引用

41st acm sigplan conference on programming language design and implementation (PLDI)

作者： Santos, Jose Fragoso Maksimovic, Petar Ayoun, Sacha-Elie Gardner, Philippa Univ Lisbon INESC ID Inst Super Tecn Lisbon Portugal Imperial Coll London London England

ISBN: (纸本)9781450376136

We introduce Gillian, a platform for developing symbolic analysis tools for programming languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is parametric on the memory model of the target language. We give a formal description of the symbolic analysis and a modular implementation that closely follows this description. We prove a parametric soundness result, introducing restriction on abstract states, which generalises path conditions used in classical symbolic execution. We instantiate Gillian to obtain trusted symbolic testing tools for JavaScript and C, and use these tools to find bugs in real-world code, thus demonstrating the viability of our parametric approach.

关键词： Symbolic execution parametric semantics bug-finding bounded verification JavaScript C

来源：评论

学校读者我要写书评

暂无评论

Example-Guided Synthesis of Relational Queries 2021

Example-Guided Synthesis of Relational Queries

引用

42nd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Thakkar, Aalok Naik, Aaditya Sands, Nathaniel Alur, Rajeev Naik, Mayur Raghothaman, Mukund Univ Penn Philadelphia PA 19104 USA Univ Southern Calif Los Angeles CA 90007 USA

ISBN: (纸本)9781450383912

Program synthesis tasks are commonly specified via input-output examples. Existing enumerative techniques for such tasks are primarily guided by program syntax and only make indirect use of the examples. We identify a class of synthesis algorithms for programming-by-examples, which we call Example-Guided Synthesis (EGS), that exploits latent structure in the provided examples while generating candidate programs. We present an instance of EGS for the synthesis of relational queries and evaluate it on 86 tasks from three application domains: knowledge discovery, program analysis, and database querying. Our evaluation shows that EGS outperforms state-of-the-art synthesizers based on enumerative search, constraint solving, and hybrid techniques in terms of synthesis time, quality of synthesized programs, and ability to prove unrealizability.

关键词： programming by example Example-Guided Synthesis

来源：评论

学校读者我要写书评

暂无评论

Latte: A language, Compiler, and Runtime for Elegant and Efficient Deep Neural Networks 16

Latte: A Language, Compiler, and Runtime for Elegant and Eff...

引用

37th acm sigplan conference on programming language design and implementation

作者： Truong, Leonard Barik, Rajkishore Totoni, Ehsan Liu, Hai Markley, Chick Fox, Armando Shpeisman, Tatiana Univ Calif Berkeley Intel Labs Berkeley CA USA Intel Labs Berkeley CA USA Univ Calif Berkeley Berkeley CA USA

ISBN: (纸本)9781450342612

Deep neural networks (DNNs) have undergone a surge in popularity with consistent advances in the state of the art for tasks including image recognition, natural language processing, and speech recognition. The computationally expensive nature of these networks has led to the proliferation of implementations that sacrifice abstraction for high performance. In this paper, we present Latte, a domain-specific language for DNNs that provides a natural abstraction for specifying new layers without sacrificing performance. Users of Latte express DNNs as ensembles of neurons with connections between them. The Latte compiler synthesizes a program based on the user specification, applies a suite of domain-specific and general optimizations, and emits efficient machine code for heterogeneous architectures. Latte also includes a communication runtime for distributed memory data-parallelism. Using networks described using Latte, we demonstrate 3-6x speedup over Caffe (C++/MKL) on the three state-of-the-art ImageNet models executing on an Intel Xeon E5-2699 v3 x86 CPU.

关键词： Deep Learning Neural Networks Domain Specific language Compiler Optimization

来源：评论

学校读者我要写书评

暂无评论

Synthesizing Racy Tests 15

Synthesizing Racy Tests

引用

36th acm sigplan conference on programming language design and implementation

作者： Samak, Malavika Ramanathan, Murali Krishna Jagannathan, Suresh Indian Inst Sci Bangalore 560012 Karnataka India Purdue Univ W Lafayette IN 47907 USA

ISBN: (纸本)9781450334686

Subtle concurrency errors in multithreaded libraries that arise because of incorrect or inadequate synchronization are often difficult to pinpoint precisely using only static techniques. On the other hand, the effectiveness of dynamic race detectors is critically dependent on multithreaded test suites whose execution can be used to identify and trigger races. Usually, such multithreaded tests need to invoke a specific combination of methods with objects involved in the invocations being shared appropriately to expose a race. Without a priori knowledge of the race, construction of such tests can be challenging. In this paper, we present a lightweight and scalable technique for synthesizing precisely these kinds of tests. Given a multithreaded library and a sequential test suite, we describe a fully automated analysis that examines sequential execution traces, and produces as its output a concurrent client program that drives shared objects via library method calls to states conducive for triggering a race. Experimental results on a variety of well-tested Java libraries yield 101 synthesized multithreaded tests in less than four minutes. Analyzing the execution of these tests using an off-the-shelf race detector reveals 187 harmful races, including several previously unreported ones.

关键词： design Reliability Verification Race detection dynamic analysis concurrency

来源：评论

学校读者我要写书评

暂无评论

Extensible algebraic datatypes with defaults 01

Extensible algebraic datatypes with defaults

引用

6th International conference on Functional programming (ICFP 2001)

作者： Zenger, M Odersky, M Swiss Fed Inst Technol INR Ecublens CH-1015 Lausanne Switzerland

ISBN: (纸本)9781581134155

A major problem for writing extensible software arises when recursively defined datatypes and operations on these types have to be extended simultaneously without modifying existing code. This paper introduces Extensible Algebraic Datatypes with Defaults which promote a simple programming pattern to solve this well known problem. We show that it is possible to encode extensible algebraic datatypes in an object-oriented language, using a new design pattern for extensible visitors. Extensible algebraic datatypes have been successfully applied in the implementation of an extensible Java compiler. Our technique allows for the reuse of existing components in compiler extensions without the need for any adaptations.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共94页 << < 25 26 27 28 29 30 31 32 33 34 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：