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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

26 篇 会议

馆藏范围

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

日期分布

学科分类号

21 篇 工学
- 21 篇 软件工程
- 1 篇 计算机科学与技术...

主题

11 篇 design
10 篇 languages
6 篇 performance
4 篇 algorithms
3 篇 experimentation
3 篇 reliability
2 篇 scripting langua...
2 篇 program synthesi...
2 篇 type systems
2 篇 probabilistic pr...
2 篇 end-user program...
2 篇 measurement
2 篇 programming lang...
2 篇 concurrency
1 篇 deterministic mu...
1 篇 separation
1 篇 macros
1 篇 precise exceptio...
1 篇 symbolic virtual...
1 篇 fast

机构

2 篇 univ wisconsin m...
2 篇 stanford univ st...
2 篇 univ washington ...
1 篇 epfl
1 篇 natl taipei univ...
1 篇 univ massachuset...
1 篇 technion haifa
1 篇 university of co...
1 篇 ufrj rio de jane...
1 篇 acad sinica taiw...
1 篇 univ calif davis...
1 篇 swiss fed inst t...
1 篇 beijing inst tec...
1 篇 puc-rio rio de j...
1 篇 microsoft corp m...
1 篇 chinese acad sci...
1 篇 univ calif berke...
1 篇 microsoft resear...
1 篇 rice univ dept c...
1 篇 cornell univ ith...

作者

2 篇 gupta gagan
2 篇 grossman dan
2 篇 gulwani sumit
2 篇 sohi gurindar s.
2 篇 sridharan srinat...
1 篇 mascarenhas fabi...
1 篇 mckinley kathryn...
1 篇 shull thomas
1 篇 yahav eran
1 篇 garzaran maria j...
1 篇 vilk john
1 篇 maidl andré murb...
1 篇 sujeeth arvind k...
1 篇 choi jiho
1 篇 devito zachary
1 篇 li yong
1 篇 ceze luis
1 篇 rajamani sriram ...
1 篇 paulo marques
1 篇 aiken alex

语言

26 篇 英文

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

共 26 条记录，以下是1-10 订阅

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

详细简洁

排序：

Memory Systems Performance and Correctness, MSPC 2014 - In Conjunction with the 35th acm sigplan conference on programming language design and implementation, pldi 2014

Memory Systems Performance and Correctness, MSPC 2014 - In C...

引用

2014 Workshop on Memory Systems Performance and Correctness, MSPC 2014 - In Conjunction with the 35th acm sigplan conference on programming language design and implementation, pldi 2014

ISBN: (纸本)9781450329170

the proceedings contain 9 papers. the topics discussed include: a study of connected object locality in NUMA heaps;affinity-based hash tables;feedback directed optimization of TCMalloc;main memory and cache performance of Intel sandy bridge and AMD bulldozer;non-volatile memory is a broken time machine;O-structures: semantics for versioned memory;outlawing ghosts: avoiding out-of-thin-air results;and trash in cache: detecting eternally silent stores.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Advanced Automata-Based Algorithms for Program Termination Checking 2018

Advanced Automata-Based Algorithms for Program Termination C...

引用

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

作者： Chen, Yu-Fang Heizmann, Matthias Lengal, Ondrej Li, Yong Tsai, Ming-Hsien Turrini, Andrea Zhang, Lijun Acad Sinica Taipei Taiwan Natl Taipei Univ New Taipei Taiwan Univ Freiburg Freiburg Germany Brno Univ Technol FIT IT4Innovat Ctr Excellence Brno Czech Republic Chinese Acad Sci Univ Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China Chinese Acad Sci Inst Software State Key Lab Comp Sci Beijing Peoples R China

ISBN: (纸本)9781450356985

In 2014, Heizmann et al. proposed a novel framework for program termination analysis. the analysis starts with a termination proof of a sample path. the path is generalized to a Buchi automaton (BA) whose language (by construction) represents a set of terminating paths. All these paths can be safely removed from the program. the removal of paths is done using automata difference, implemented via BA complementation and intersection. the analysis constructs in this way a set of BAs that jointly "cover" the behavior of the program, thus proving its termination. An implementation of the approach in Ultimate Automizer won the 1st place in the Termination category of SV-Comp 2017. In this paper, we exploit advanced automata-based algorithms and propose several non-trivial improvements of the framework. To alleviate the complementation computation for BAs-one of the most expensive operations in the framework-, we propose a multi-stage generalization construction. We start with generalizations producing subclasses of BAs (such as deterministic BAs) for which efficient complementation algorithms are known, and proceed to more general classes only if necessary. Particularly, we focus on the quite expressive subclass of semideterministic BAs and provide an improved complementation algorithm for this class. Our experimental evaluation shows that the proposed approach significantly improves the power of termination checking within the Ultimate Automizer framework.

关键词： Program Termination Buchi Automata Complementation and language Difference

来源：评论

学校读者我要写书评

暂无评论

pldi 2014 - Proceedings of the 2014 acm sigplan conference on programming language design and implementation

PLDI 2014 - Proceedings of the 2014 ACM SIGPLAN Conference o...

引用

35th acm sigplan conference on programming language design and implementation, pldi 2014

ISBN: (纸本)9781450327848

the proceedings contain 56 papers. the topics discussed include: test-driven repair of data races in structured parallel programs;atomicity refinement for verified compilation;herding cats: modeling, simulation, testing, and data-mining for weak memory;stochastic optimization of floating-point programs using tunable precision;a framework for enhancing data reuse via associative reordering;first-class runtime generation of high-performance types using exotypes;optimal inference of fields in row-polymorphic records;expressing and verifying probabilistic assertions;compositional solution space quantification for probabilistic software analysis;slicing probabilistic programs;adaptive, efficient parallel execution of parallel programs differentiation;globally precise-restartable execution of parallel programs;and accurate application progress analysis for large-scale parallel debugging.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Getting F-Bounded Polymorphism into Shape 14

Getting F-Bounded Polymorphism into Shape

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Greenman, Ben Muehlboeck, Fabian Tate, Ross Cornell Univ Ithaca NY 14853 USA

ISBN: (纸本)9781450327848

We present a way to restrict recursive inheritance without sacrificing the benefits of F-bounded polymorphism. In particular, we distinguish two new concepts, materials and shapes, and demonstrate through a survey of 13.5 million lines of open-source generic-Java code that these two concepts never actually overlap in practice. With this Material-Shape Separation, we prove that even naive type-checking algorithms are sound and complete, some of which address problems that were unsolvable even under the existing proposals for restricting inheritance. We illustrate how the simplicity of our design reflects the design intuitions employed by programmers and potentially enables new features coming into demand for upcoming programming languages.

关键词： Algorithms design languages Materials Shapes Separation Subtyping F-Bounded Polymorphism Variance Decidability Joins Higher-Kinded Types

来源：评论

学校读者我要写书评

暂无评论

Resugaring: Lifting Evaluation Sequences through Syntactic Sugar 14

Resugaring: Lifting Evaluation Sequences through Syntactic S...

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Pombrio, Justin Krishnamurthi, Shriram Brown Univ Providence RI 02912 USA

ISBN: (纸本)9781450327848

Syntactic sugar is pervasive in language technology. It is used to shrink the size of a core language;to define domain-specific languages;and even to let programmers extend their language. Unfortunately, syntactic sugar is eliminated by transformation, so the resulting programs become unfamiliar to authors. thus, it comes at a price: it obscures the relationship between the user's source program and the program being evaluated. We address this problem by showing how to compute reduction steps in terms of the surface syntax. Each step in the surface language emulates one or more steps in the core language. the computed steps hide the transformation, thus maintaining the abstraction provided by the surface language. We make these statements about emulation and abstraction precise, prove that they hold in our formalism, and verify part of the system in Coq. We have implemented this work and applied it to three very different languages.

关键词： programming languages Syntactic Sugar Macros Evaluation Debugging Resugaring

来源：评论

学校读者我要写书评

暂无评论

Code Completion with Statistical language Models 14

Code Completion with Statistical Language Models

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Raychev, Veselin Vechev, Martin Yahav, Eran Swiss Fed Inst Technol Zurich Switzerland Technion Haifa Israel

ISBN: (纸本)9781450327848

We address the problem of synthesizing code completions for programs using APIs. Given a program with holes, we synthesize completions for holes with the most likely sequences of method calls. Our main idea is to reduce the problem of code completion to a natural-language processing problem of predicting probabilities of sentences. We design a simple and scalable static analysis that extracts sequences of method calls from a large codebase, and index these into a statistical language model. We then employ the language model to find the highest ranked sentences, and use them to synthesize a code completion. Our approach is able to synthesize sequences of calls across multiple objects together with their arguments. Experiments show that our approach is fast and effective. Virtually all computed completions typecheck, and the desired completion appears in the top 3 results in 90% of the cases.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

FAST: a Transducer-Based language for Tree Manipulation 14

FAST: a Transducer-Based Language for Tree Manipulation

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： D'Antoni, Loris Veanes, Margus Livshits, Benjamin Molnar, David Univ Penn Philadelphia PA 19104 USA

ISBN: (纸本)9781450327848

Tree automata and tree transducers are used in a wide range of applications in software engineering, from XML processing to language type-checking. While these formalisms are of immense practical use, they can only model finite alphabets, and since many real-world applications operate over in finite domains such as integers, this is often a limitation. To overcome this problem we augment tree automata and transducers with symbolic alphabets represented as parametric theories. Admitting in finite alphabets makes these models more general and succinct than their classical counterparts. Despite this, we show how the main operations, such as composition and language equivalence, remain computable given a decision procedure for the alphabet theory. We introduce a high-level language called Fast that acts as a front-end for the above formalisms. Fast supports symbolic alphabets through tight integration with state-of-the art satisfiability modulo theory (SMT) solvers. We demonstrate our techniques on practical case studies, covering a wide range of applications.

关键词： Symbolic Tree Transducers FAST

来源：评论

学校读者我要写书评

暂无评论

Dynamic Enforcement of Determinism in a Parallel Scripting language 14

Dynamic Enforcement of Determinism in a Parallel Scripting L...

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Lu, Li Ji, Weixing Scott, Michael L. Univ Rochester Rochester NY 14627 USA Beijing Inst Technol Beijing Peoples R China

ISBN: (纸本)9781450327848

Determinism is an appealing property for parallel programs, as it simplifies understanding, reasoning and debugging. It is particularly appealing in dynamic (scripting) languages, where ease of programming is a dominant design goal. Some existing parallel languages use the type system to enforce determinism statically, but this is not generally practical for dynamic languages. In this paper, we describe how determinism can be obtained-and dynamically enforced/verified-for appropriate extensions to a parallel scripting language. Specifically, we introduce the constructs of Deterministic Parallel Ruby (DPR), together with a run-time system (TARDIS) that verifies properties required for determinism, including correct usage of reductions and commutative operators, and the mutual independence (data-race freedom) of concurrent tasks. Experimental results confirm that DPR can provide scalable performance on multicore machines and that the overhead of TARDIS is low enough for practical testing. In particular, TARDIS significantly outperforms alternative data-race detectors with comparable functionality. We conclude with a discussion of future directions in the dynamic enforcement of determinism.

关键词： design languages Reliability Determinism deterministic parallelism data races scripting language

来源：评论

学校读者我要写书评

暂无评论

First-class Runtime Generation of High-performance Types using Exotypes 14

First-class Runtime Generation of High-performance Types usi...

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： DeVito, Zachary Ritchie, Daniel Fisher, Matt Aiken, Alex Hanrahan, Pat Stanford Univ Stanford CA 94305 USA

ISBN: (纸本)9781450327848

We introduce exotypes, user-defined types that combine the flexibility of meta-object protocols in dynamically-typed languages with the performance control of low-level languages. Like objects in dynamic languages, exotypes are defined programmatically at runtime, allowing behavior based on external data such as a database schema. To achieve high performance, we use staged programming to define the behavior of an exotype during a runtime compilation step and implement exotypes in Terra, a low-level staged programming language. We show how exotype constructors compose, and use exotypes to implement high-performance libraries for serialization, dynamic assembly, automatic differentiation, and probabilistic programming. Each exotype achieves expressiveness similar to libraries written in dynamically-typed languages but implements optimizations that exceed the performance of existing libraries written in low-level statically-typed languages. though each implementation is significantly shorter, our serialization library is 11 times faster than Kryo, and our dynamic assembler is 3-20 times faster than Google's Chrome assembler.

关键词： design Performance Lua Staged computation DSL

来源：评论

学校读者我要写书评

暂无评论

FlashExtract: A Framework for Data Extraction by Examples 14

FlashExtract: A Framework for Data Extraction by Examples

引用

35th acm sigplan conference on programming language design and implementation (pldi)

作者： Le, Vu Gulwani, Sumit Univ Calif Davis Davis CA 95616 USA Microsoft Res Redmond Redmond WA USA

ISBN: (纸本)9781450327848

Various document types that combine model and view (e. g., text files, webpages, spreadsheets) make it easy to organize (possibly hierarchical) data, but make it difficult to extract raw data for any further manipulation or querying. We present a general framework FlashExtract to extract relevant data from semi-structured documents using examples. It includes: (a) an interaction model that allows end-users to give examples to extract various fields and to relate them in a hierarchical organization using structure and sequence constructs. (b) an inductive synthesis algorithm to synthesize the intended program from few examples in any underlying domain-specific language for data extraction that has been built using our specified algebra of few core operators (map, filter, merge, and pair). We describe instantiation of our framework to three different domains: text files, webpages, and spreadsheets. On our benchmark comprising 75 documents, FlashExtract is able to extract intended data using an average of 2.36 examples in 0.84 seconds per field.

关键词： languages Algorithms Human Factors Program Synthesis End-user programming programming by Examples

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共3页 << < 1 2 3 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：