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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

256 篇 会议
26 篇 期刊文献
2 册 图书

馆藏范围

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

日期分布

学科分类号

225 篇 工学
- 215 篇 软件工程
- 164 篇 计算机科学与技术...
- 2 篇 信息与通信工程
- 2 篇 控制科学与工程
- 1 篇 材料科学与工程（可...
- 1 篇 电气工程
41 篇 理学
- 38 篇 数学
- 4 篇 系统科学
- 3 篇 统计学（可授理学、...
13 篇 管理学
- 7 篇 图书情报与档案管...
- 6 篇 管理科学与工程(可...
- 4 篇 工商管理
1 篇 经济学
- 1 篇 应用经济学

主题

83 篇 languages
43 篇 performance
29 篇 computer program...
24 篇 algorithms
24 篇 verification
23 篇 design
19 篇 theory
18 篇 parallel program...
10 篇 functional progr...
8 篇 logic programmin...
7 篇 experimentation
7 篇 semantics
6 篇 reliability
6 篇 mpi
6 篇 dependent types
6 篇 transactional me...
5 篇 abstract interpr...
4 篇 object oriented ...
4 篇 static analysis
4 篇 atomicity

机构

4 篇 carnegie mellon ...
3 篇 univ texas austi...
3 篇 univ of tokyo
3 篇 tohoku univ send...
3 篇 imdea software i...
3 篇 microsoft resear...
3 篇 univ texas austi...
2 篇 epfl
2 篇 univ wisconsin d...
2 篇 univ wisconsin m...
2 篇 xerox parc
2 篇 univ illinois ur...
2 篇 department of co...
2 篇 swiss fed inst t...
2 篇 univ lugano usi ...
2 篇 natl inst inform...
2 篇 mcgill univ mont...
2 篇 northeastern uni...
2 篇 univ calif santa...
2 篇 microsoft resear...

作者

4 篇 pingali keshav
4 篇 burtscher martin
3 篇 taura kenjiro
3 篇 yonezawa akinori
3 篇 flanagan cormac
3 篇 walker david
3 篇 abadi martin
3 篇 kobayashi naoki
2 篇 hoefler torsten
2 篇 saraswat vijay
2 篇 wand mitchell
2 篇 huelsbergen lore...
2 篇 grossman dan
2 篇 stulova nataliia
2 篇 palsberg jens
2 篇 donaldson alasta...
2 篇 yoshida nobuko
2 篇 kim jungwon
2 篇 gay simon j.
2 篇 welc adam

语言

282 篇 英文
2 篇 其他

检索条件"任意字段=Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"

共 284 条记录，以下是31-40 订阅

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

详细简洁

排序：

Context-sensitive data-dependence analysis via linear conjunctive language reachability 17

Context-sensitive data-dependence analysis via linear conjun...

引用

44th acm sigplan symposium on principles of programming languages, POPL 2017

作者： Zhang, Qirun Su, Zhendong University of California Davis United States

ISBN: (纸本)9781450346603

Many program analysis problems can be formulated as graph reachability problems. In the literature, context-free language (CFL) reachability has been the most popular formulation and can be computed in subcubic time. the context-sensitive data-dependence analysis is a fundamental abstraction that can express a broad range of program analysis problems. It essentially describes an interleaved matched-parenthesis language reachability problem. the language is not context-free, and the problem is well-known to be undecidable. In practice, many program analyses adopt CFL-reachability to exactly model the matched parentheses for either context-sensitivity or structure-transmitted data-dependence, but not both. thus, the CFL-reachability formulation for context-sensitive data-dependence analysis is inherently an approximation. To support more precise and scalable analyses, this paper introduces linear conjunctive language (LCL) reachability, a new, expressive class of graph reachability. LCL not only contains the interleaved matched-parenthesis language, but is also closed under all set-theoretic operations. Given a graph with n nodes and m edges, we propose an O(mn) time approximation algorithm for solving all-pairs LCL-reachability, which is asymptotically better than known CFL-reachability algorithms. Our formulation and algorithm offer a new perspective on attacking the aforementioned undecidable problem-the LCL-reachability formulation is exact, while the LCL-reachability algorithm yields a sound approximation. We have applied the LCL-reachability framework to two existing client analyses. the experimental results show that the LCL-reachability framework is both more precise and scalable than the traditional CFL-reachability framework. this paper opens up the opportunity to exploit LCL-reachability in program analysis. © 2017 acm.

关键词： Context free languages

来源：评论

学校读者我要写书评

暂无评论

Aggressive Pipelining of Irregular Applications on Reconfigurable Hardware 17

Aggressive Pipelining of Irregular Applications on Reconfigu...

引用

44th Annual International symposium on Computer Architecture (ISCA)

作者： Li, Zhaoshi Liu, Leibo Deng, Yangdong Yin, Shouyi Wang, Yao Wei, Shaojun Tsinghua Univ Natl Lab Informat Sci & Technol Beijing Peoples R China Tsinghua Univ Sch Software Beijing Peoples R China

ISBN: (纸本)9781450348928

CPU-FPGA heterogeneous platforms offer a promising solution for high-performance and energy-efficient computing systems by providing specialized accelerators with post-silicon reconfigurability. To unleash the power of FPGA, however, the programmability gap has to be filled so that applications specified in high-level programming languages can be efficiently mapped and scheduled on FPGA. the above problem is even more challenging for irregular applications, in which the execution dependency can only be determined at run time. thus over-serialized accelerators are generated from existing works that rely on compile time analysis to schedule the computation. In this work, we propose a comprehensive software-hardware co-design framework, which captures parallelism in irregular applications and aggressively schedules pipelined execution on reconfigurable platform. Based on an inherently parallel abstraction packaging parallelism for runtime schedule, our framework significantly differs from existing works that tend to schedule executions at compile time. An irregular application is formulated as a set of tasks with their dependencies specified as rules describing the conditions under which a subset of tasks can be executed concurrently. then datapaths on FPGA will be generated by transforming applications in the formulation into task pipelines orchestrated by evaluating rules at runtime, which could exploit fine-grained pipeline parallelism as handcrafted accelerators do. An evaluation shows that this framework is able to produce datapath with its quality close to handcrafted designs. Experiments show that generated accelerators are dramatically more efficient than those created by current high-level synthesis tools. Meanwhile, accelerators generated for a set of irregular applications attain 0.5x similar to 1.9x performance compared to equivalent software implementations we selected on a server-grade 10-core processor, with the memory subsystem remaining as the bottlene

关键词： FPGA Hardware Accelerator Parallel programming

来源：评论

学校读者我要写书评

暂无评论

JParEnt: Parallel entropy decoding for JPEG decompression on heterogeneous multicore architectures 7

JParEnt: Parallel entropy decoding for JPEG decompression on...

引用

Euro-Par Conference / 7th International Workshop on programming Models and Applications for Multicores and Manycores (PMAM) held in conjunction with the 21st sigplan symposium on principles and Practice of Parallel programming (PPoPP)

作者： Sodsong, Wasuwee Jung, Minyoung Park, Jinwoo Burgstaller, Bernd Yonsei Univ Dept Comp Sci Seoul South Korea

ISBN: (纸本)9781450341967

the JPEG format employs Huffman codes to compress the entropy data of an image. Huffman codewords are of variable length, which makes parallel entropy decoding a difficult problem. To determine the start position of a codeword in the bitstream, the previous codeword must be decoded first. We present JParEnt, a new approach to parallel entropy decoding for JPEG decompression on heterogeneous multicores. JParEnt conducts JPEG decompression in two steps: (1)an efficient sequential scan of the entropy data on the CPU to determine the start-positions (boundaries) of coefficient blocks in the bitstream, followed by (2)a parallel entropy decoding step on the graphics processing unit (GPU). the block boundary scan constitutes a reinterpretation of the Huffman-coded entropy data to determine codeword boundaries in the bitstream. We introduce a dynamic workload partitioning scheme to account for GPUs of low compute power relative to the CPU. this configuration has become common with the advent of SoCs with integrated graphics processors (IGPs). We leverage additional parallelism through pipelined execution across CPU and GPU. For systems providing a unified address space between CPU and GPU, we employ zero-copy to completely eliminate the data transfer overhead. Our experimental evaluation of JParEnt was conducted on six heterogeneous multicore systems: one server and two desktops with dedicated GPUs, one desktop with an IGP, and two embedded systems. For a selection of more than 1000JPEG images, JParEnt outperforms the SIMD-implementation of the libjpeg-turbo library by up to a factor of 4.3x, and the previously fastest JPEG decompression method for heterogeneous multicores by up to a factor of 2.2x. JParEnt's entropy data scan consumes 45% of the entropy decoding time of libjpeg-turbo on average. Given this new ratio for the sequential part of JPEG decompression, JParEnt achieves up to97% of the maximum attainable speedup (95% on average). On the IGP-based desktop platform,

关键词： JPEG decoding entropy decoding prefix codes heterogeneous multicores GPU programming

来源：评论

学校读者我要写书评

暂无评论

Language-integrated Provenance 16

Language-integrated Provenance

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Fehrenbach, Stefan Cheney, James Univ Edinburgh Edinburgh Midlothian Scotland

ISBN: (纸本)9781450341486

Provenance, or information about the origin or derivation of data, is important for assessing the trustworthiness of data and identifying and correcting mistakes. Most prior implementations of data provenance have involved heavyweight modifications to database systems and little attention has been paid to how the provenance data can be used outside such a system. We present extensions to the Links programming language that build on its support for language-integrated query to support provenance queries by rewriting and normalizing monadic comprehensions and extending the type system to distinguish provenance metadata from normal data. the main contribution of this paper is to show that the two most common forms of provenance can be implemented efficiently and used safely as a programming language feature with no changes to the database system.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

proceedings of the 18th International symposium on principles and Practice of Declarative programming, PPDP 2016

Proceedings of the 18th International Symposium on Principle...

引用

18th International symposium on principles and Practice of Declarative programming, PPDP 2016

ISBN: (纸本)9781450341486

the proceedings contain 16 papers. the topics discussed include: description and evaluation of a generic design to integrate CLP and tabled execution;higher-order logic programming: an expressive language for representing qualitative preferences;a framework for easing the development of applications embedding answer set programming;proving inductive validity of constrained inequalities;analysis of access control policy updates through narrowing;strand spaces with choice via a process algebra semantics;reducing the overhead of assertion run-time checks via static analysis;and iterated process analysis over lattice-valued regular expressions.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Higher-Order Logic programming: an Expressive Language for Representing Qualitative Preferences 16

Higher-Order Logic Programming: an Expressive Language for R...

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Charalambidis, Angelos Rondogiannis, Panos Troumpoukis, Antonis Univ Athens Dept Informat & Telecommun Athens Greece NCSR Demokritos Inst Informat & Telecommun Aghia Paraskevi Greece

ISBN: (纸本)9781450341486

We consider the problem of concisely representing and handling preferences in logic programming and relational data-bases. Our starting point is a well-known proposal [8] which advocates the embedding of first-order preference formulas into relational algebra through a single winnow operator that is parameterized by a database relation and a preference formula. We argue that despite its elegance, the framework of [8] has a number of shortcomings: only intrinsic preference formulas are supported, the preference relations and preference queries are expressed in two different languages, and there is no direct way to define alternative operators beyond winnow. We propose the use of higher-order logic programming as a logical framework that remedies all the above deficiencies. In particular, the proposed framework supports both intrinsic and extrinsic preference formulas, it can represent both preference relations as-well-as queries, and it can be used to define a variety of interesting alternative operators beyond winnow. We demonstrate the feasibility of our approach by presenting an implementation of all the proposed concepts in the higher-order logic programming language Hilog.

关键词： Preferences Higher-Order Logic programming Hilog

来源：评论

学校读者我要写书评

暂无评论

Typechecking Protocols with Mungo and StMungo 16

Typechecking Protocols with Mungo and StMungo

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Kouzapas, Dimitrios Dardha, Ornela Perera, Roly Gay, Simon J. Univ Glasgow Sch Comp Sci Glasgow Lanark Scotland

ISBN: (纸本)9781450341486

We report on two tools that extend Java with support for static type-checking of communication protocols. Our Mungo tool extends Java with typestate definitions, which allow classes to be associated with state machines defining permitted sequences of method calls. A complementary tool, StMungo, takes a communication protocol specified in the Scribble protocol description language, and generates a typestate specification for each endpoint, capturing the permitted sequences of messages along that channel. Endpoint implementations can be validated by Mungo against their typestate definitions and then compiled as usual with j avac. We formalise Mungo's typestate inference system and demonstrate the Scribble, Mungo and StMungo toolchain via a typechecked SMTP client that can communicate with a real-world SMTP server.

关键词： Session types object-oriented programming typestate protocols typestate inference

来源：评论

学校读者我要写书评

暂无评论

Exploration of Language Specifications by Compilation to First-Order Logic 16

Exploration of Language Specifications by Compilation to Fir...

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Grewe, Sylvia Erdweg, Sebastian Raulf, Michael Mezini, Mira Tech Univ Darmstadt Darmstadt Germany Delft Univ Technol Delft Netherlands Univ Lancaster Lancaster England

ISBN: (纸本)9781450341486

Exploration of language specifications helps to discover errors and inconsistencies early during the development of a programming language. We propose exploration of language specifications via application of existing automated first-order theorem provers (ATPs). To this end, we translate language specifications and exploration tasks to first-order logic, which many ATPs accept as input. However, there are several different strategies for compiling a language specification to first-order logic, and even small variations in the translation may have a large impact on the time it takes ATPs to find proofs. In this paper, we present a systematic empirical study on how to best compile language specifications to first-order logic such that existing ATPs can solve typical exploration tasks efficiently. We have developed a compiler product line that implements 36 different compilation strategies and used it to feed language specifications to 4 existing first-order theorem provers. As a benchmark, we developed a language specification for typed SQL with 50 exploration goals. Our study empirically confirms that the choice of a compilation strategy in general greatly influences prover performance and shows which strategies are advantageous for prover performance.

关键词： Type systems Formal specification Declarative languages First-order theorem proving Domain-specific languages

来源：评论

学校读者我要写书评

暂无评论

A Framework for Easing the Development of Applications Embedding Answer Set programming 16

A Framework for Easing the Development of Applications Embed...

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Fusca, Davide Germano, Stefano Zangari, Jessica Anastasio, Marco Calimeri, Francesco Perri, Simona Univ Calabria Dept Math & Comp Sci Via BucciCubo 30B I-87036 Arcavacata Di Rende Italy DLVSystem Srl Arcavacata Di Rende Italy

ISBN: (纸本)9781450341486

Answer Set programming (ASP) is a well-established declarative problem solving paradigm which became widely used in AI and recognized as a powerful tool for knowledge representation and reasoning (KRR), especially for its high expressiveness and the ability to deal also with incomplete knowledge. Recently, thanks to the availability of a number of robust and efficient implementations, ASP has been increasingly employed in a number of different domains, and used for the development of industrial-level and enterprise applications. this made clear the need for proper development tools and interoperability mechanisms for easing interaction and integration with external systems in the widest range of real-world scenarios, including mobile applications and educational contexts. In this work we present a framework for integrating the KRR capabilities of ASP into generic applications. We show the use of the framework by illustrating proper specializations for some relevant ASP systems over different platforms, including the mobile setting;furthermore, the potential of the framework for educational purposes is illustrated by means of the development of several ASP-based applications.

关键词： Answer Set programming Logic Programs Education Industrial Applications Knowledge Representation and Reasoning Object-Oriented programming Software Development Complex Systems Embedded Systems Artificial Intelligence

来源：评论

学校读者我要写书评

暂无评论

Reducing the Overhead of Assertion Run-time Checks via Static Analysis 16

Reducing the Overhead of Assertion Run-time Checks via Stati...

引用

18th International symposium on principles and Practice of Declarative programming (PPDP)

作者： Stulova, Nataliia Morales, Jose F. Hermenegildo, Manuel V. IMDEA Software Inst Madrid Spain Tech Univ Madrid UPM Sch Comp Sci Madrid Spain

ISBN: (纸本)9781450341486

In order to aid in the process of detecting incorrect program behaviors, a number of approaches have been proposed which include a combination of language-level constructs (such as procedure-level assertions/contracts, program-point assertions, gradual types, etc.) and associated tools (such as code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and/or limited expressiveness. Verification frameworks that combine static and dynamic techniques offer the potential to bridge this gap. In this paper we explore the effectiveness of abstract interpretation in detecting parts of program specifications that can be statically simplified to true or false, as well as the impact of such analysis in reducing the cost of the run-time checks required for the remaining parts of these specifications. Starting with a semantics for programs with assertion checking, and for assertion simplification based on static analysis information, we propose and study a number of practical assertion checking modes, each of which represents a trade-off between code annotation depth, execution time slowdown, and program safety. We also propose techniques for taking advantage of the run-time checking semantics to improve the precision of the analysis. Finally, we study experimentally the performance of these techniques. Our experiments illustrate the benefits and costs of each of the assertion checking modes proposed as well as the benefit of analysis for these scenarios.

关键词： Abstract Interpretation Assertions Run-time Checking Verification Logic programming Horn Clauses

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共29页 << < 1 2 3 4 5 6 7 8 9 10 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：