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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

1,152 篇 会议
135 篇 期刊文献

馆藏范围

1,287 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

1,112 篇 工学
- 1,037 篇 软件工程
- 800 篇 计算机科学与技术...
- 48 篇 控制科学与工程
- 43 篇 电气工程
- 36 篇 信息与通信工程
- 9 篇 电子科学与技术（可...
- 8 篇 机械工程
- 6 篇 安全科学与工程
- 5 篇 建筑学
- 5 篇 土木工程
- 5 篇 航空宇航科学与技...
- 5 篇 生物工程
- 4 篇 材料科学与工程（可...
- 4 篇 化学工程与技术
- 2 篇 力学（可授工学、理...
- 2 篇 光学工程
- 2 篇 农业工程
141 篇 理学
- 117 篇 数学
- 13 篇 系统科学
- 9 篇 统计学（可授理学、...
- 7 篇 生物学
- 5 篇 物理学
- 4 篇 化学
89 篇 管理学
- 53 篇 管理科学与工程(可...
- 41 篇 图书情报与档案管...
- 28 篇 工商管理
15 篇 教育学
- 15 篇 教育学
6 篇 经济学
- 6 篇 应用经济学
5 篇 法学
- 4 篇 社会学
2 篇 农学
- 2 篇 作物学

主题

180 篇 design
167 篇 languages
103 篇 computer program...
99 篇 performance
59 篇 algorithms
49 篇 object oriented ...
49 篇 computer program...
45 篇 experimentation
45 篇 java programming...
39 篇 verification
35 篇 reliability
34 篇 java
32 篇 functional progr...
26 篇 program synthesi...
24 篇 probabilistic pr...
22 篇 software design
21 篇 theory
20 篇 concurrency
19 篇 domain-specific ...
18 篇 type systems

机构

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

作者

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

语言

1,205 篇 英文
81 篇 其他
1 篇 中文

检索条件"任意字段=Proceedings of the ACM Sigplan 2003 Conference on Programming Language Design and Implementation"

共 1287 条记录，以下是481-490 订阅

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

详细简洁

排序：

Type analysis of Prolog using type graphs 94

Type analysis of Prolog using type graphs

引用

proceedings of the acm sigplan'94 conference on programming language design and implementation (PLDI)

作者： Van Hentenryck, P. Cortesi, A. Le Charlier, B. Brown Univ Providence United States

ISBN: (纸本)089791662X

Type analysis of Prolog is of primary importance for high-performance compilers, since type information may lead to better indexing and to sophisticated specializations of unification and built-in predicates to name a few. However, these optimizations often require a sophisticated type inference system capable of inferring disjunctive and recursive types and hence expensive in computation time. The purpose of this paper is to describe a type analysis system for Prolog based on abstract interpretation and type graphs (i.e. disjunctive rational trees) with this functionality. The system (about 15,000 lines of C) consists of the combination of a generic fixpoint algorithm, a generic pattern domain, and a type graph domain. The main contribution of the paper is to show that this approach can be engineered to be practical for medium-sized programs without sacrificing accuracy. The main technical contributions to achieve this result are (1) a novel widening operator for type graphs which appears to be accurate and effective in keeping the sizes of the graphs, and hence the computation time, reasonably small;(2) the use of the generic pattern domain to obtain a compact representation of equality constraints between subterms and to factor out sure structural information.

关键词： PROLOG (programming language)

来源：评论

学校读者我要写书评

暂无评论

Multi-language static code analysis on the LARA framework 10

Multi-language static code analysis on the LARA framework

引用

10th acm sigplan International Workshop on the State Of the Art in Program Analysis, SOAP 2021, co-located with the 42nd acm sigplan International conference on programming language design and implementation, PLDI 2021

作者： Teixeira, Gil Bispo, João Correia, Filipe F. Faculty of Engineering University of Porto Porto Portugal Faculty of Engineering University of Porto Inesc Tec Porto Portugal

ISBN: (纸本)9781450384681

We propose a mechanism to raise the abstraction level of source-code analysis and robustly support multiple languages. Built on top of the LARA framework, it allows sharing language specifications between LARA source-to-source compilers, and enables the mapping of a virtual AST over the nodes of ASTs provided by different, unrelated parsers. We use this approach to create a language specification for Object-Oriented (OO) languages and add support for three different LARA compilers. We evaluate it by implementing a library of 18 software metrics using this language specification and apply the metrics to source code in four programming languages (C, C++, Java, and JavaScript). We compare the results with other tools to evaluate the approach. © 2021 Owner/Author.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Parametric analysis for adaptive computation offloading

Parametric analysis for adaptive computation offloading

引用

conference on programming language design and implementation

作者： Wang, C Li, ZY Purdue Univ Dept Comp Sci W Lafayette IN 47907 USA

Many programs can be invoked under different execution options;input parameters and data files. Such different execution contexts may lead to strikingly different execution instances. The optimal code generation may be sensitive to the execution instances. In this paper, we show how to use parametric program analysis to deal with this issue for the optimization problem of computation offloading. Computation offloading has been shown to be an effective way to improve performance and energy saving on mobile devices. Optimal program partitioning for computation offloading depends on the tradeoff between the computation workload and the communication cost. The computation workload and communication requirement may change with different execution instances. Optimal decisions on program partitioning must be made at run time when sufficient information about workload and communication requirement becomes available. Our cost analysis obtains program computation workload and communication cost expressed as functions of run-time parameters, and our parametric partitioning algorithm finds the optimal program partitioning corresponding to different ranges of run-time parameters. At run time, the transformed program self-schedules its tasks on either the mobile device or the server, based on the optimal program partitioning that corresponds to the current values of run-time parameters. Experimental results on an HP IPAQ handheld device show that different run-time parameters can lead to quite different program partitioning decisions.

关键词： algorithms design experimentation measurement performance program partitioning program analysis program transformation computation offloading program profiling handheld devices adaptive optimization distributed system

来源：评论

学校读者我要写书评

暂无评论

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers 16

Toward Compositional Verification of Interruptible OS Kernel...

引用

37th acm sigplan conference on programming language design and implementation

作者： Chen, Hao Wu, Xiongnan (Newman) Shao, Zhong Lockerman, Joshua Gu, Ronghui Univ Elect Sci & Technol China UESTC Chengdu Peoples R China Yale Univ New Haven CT 06520 USA

ISBN: (纸本)9781450342612

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.

关键词： Verification Reliability Security languages design Program Verification Certified OS Kernels Interrupts Device Drivers Abstraction Layer Modularity

来源：评论

学校读者我要写书评

暂无评论

From Clarity to Efficiency for Distributed Algorithms 12

From Clarity to Efficiency for Distributed Algorithms

引用

acm International conference on Object Oriented programming Systems languages and Applications

作者： Liu, Yanhong A. Stoller, Scott D. Lin, Bo Gorbovitski, Michael SUNY Stony Brook Dept Comp Sci Stony Brook NY 11794 USA

ISBN: (纸本)9781450315616

This paper describes a very high-level language for clear description of distributed algorithms and optimizations necessary for generating efficient implementations. The language supports high-level control flows where complex synchronization conditions can be expressed using high-level queries, especially logic quantifications, over message history sequences. Unfortunately, the programs would be extremely inefficient, including consuming unbounded memory, if executed straightforwardly. We present new optimizations that automatically transform complex synchronization conditions into incremental updates of necessary auxiliary values as messages are sent and received. The core of the optimizations is the first general method for efficient implementation of logic quantifications. We have developed an operational semantics of the language, implemented a prototype of the compiler and the optimizations, and successfully used the language and implementation on a variety of important distributed algorithms.

关键词： Algorithms design languages Performance distributed algorithms incrementalization logic quantifications program optimization very high-level languages

来源：评论

学校读者我要写书评

暂无评论

EXPLORER : Query- and Demand-Driven Exploration of Interprocedural Control Flow Properties 2015

EXPLORER : Query- and Demand-Driven Exploration of Interproc...

引用

acm sigplan International conference on Object-Oriented programming, Systems, languages, and Applications (OOPSLA)

作者： Feng, Yu Wang, Xinyu Dillig, Isil Lin, Calvin Univ Texas Austin Austin TX 78712 USA

ISBN: (纸本)9781450336895

This paper describes a general framework-and its implementation in a tool called EXPLORER-for statically answering a class of interprocedural control flow queries about Java programs. EXPLORER allows users to formulate queries about feasible callstack configurations using regular expressions, and it employs a precise, demand-driven algorithm for answering such queries. Specifically, EXPLORER constructs an automaton A that is iteratively refined until either the language accepted by A is empty (meaning that the query has been refuted) or until no further refinement is possible based on a precise, context-sensitive abstraction of the program. We evaluate EXPLORER by applying it to three different program analysis tasks, namely, (1) analysis of the observer design pattern in Java, (2) identification of a class of performance bugs, and (3) analysis of inter-component communication in Android applications. Our evaluation shows that EXPLORER is both efficient and precise.

关键词： Algorithms languages Program analysis Demand-driven analysis points-to analysis query language control flow properties

来源：评论

学校读者我要写书评

暂无评论

Disjoint Intersection Types 2016

Disjoint Intersection Types

引用

21st acm sigplan International conference on Functional programming (ICFP)

作者： Oliveira, Bruno C. d. S. Shi, Zhiyuan Alpuim, Joao Univ Hong Kong Hong Kong Hong Kong Peoples R China

ISBN: (纸本)9781450342193

Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression can elaborate to expressions that evaluate to different values. The lack of coherence is an important disadvantage for adoption of his core calculus in implementations of programming languages, as the semantics of the programming language becomes implementation-dependent. This paper presents lambda(i) : a coherent and type-safe calculus with a form of intersection types and a merge operator. Coherence is achieved by ensuring that intersection types are disjoint and programs are sufficiently annotated to avoid type ambiguity. We propose a definition of disjointness where two types A and B are disjoint only if certain set of types are common supertypes of A and B. We investigate three different variants of lambda(i), with three variants of disjointness. In the simplest variant, which does not allow inverted perpendicular types, two types are disjoint if they do not share any common supertypes at all. The other two variants introduce inverted perpendicular types and refine the notion of disjointness to allow two types to be disjoint when the only the set of common supertypes are top-like. The difference between the two variants with inverted perpendicular types is on the definition of top-like types, which has an impact on which types are allowed on intersections. We present a type system that prevents intersection types that are not disjoint, as well as an algorithmic specifications to determine whether two types are disjoint for all three variants.

关键词： Intersection Types Type System design languages Theory

来源：评论

学校读者我要写书评

暂无评论

Mirrors: design principles for meta-level facilities of object-oriented programming languages

Mirrors: Design principles for meta-level facilities of obje...

引用

19th conference on Object-Oriented programming, Systems, languages, and Applications

作者： Bracha, G Ungar, D Sun Microsyst Inc Santa Clara CA 95054 USA Sun Microsyst Inc Mountain View CA 94043 USA

ISBN: (纸本)1581138318

We identify three design principles for reflection and metaprogramming facilities in object oriented programming languages. Encapsulation: meta-level facilities must encapsulate their implementation. Stratification: meta-level facilities must be separated from base-level functionality. Ontological correspondence: the ontology of meta-level facilities should correspond to the ontology of the language they manipulate. Traditional/mainstream reflective architectures do not follow these precepts. In contrast, reflective APIs built around the concept of mirrors are characterized by adherence to these three principles. Consequently, mirror-based architectures have significant advantages with respect to distribution, deployment and general purpose metaprogramming.

关键词： design languages reflection metaprogramming mirrors Java self smalltalk

来源：评论

学校读者我要写书评

暂无评论

Compiling a subset of apl into a typed intermediate language∗ 1

Compiling a subset of apl into a typed intermediate language...

引用

1st acm sigplan International Workshop on Libraries, languages and Compilers for Array programming, ARRAY 2014 - Part of PLDI 2014

作者： Elsman, Martin Dybdal, Martin Department of Computer Science University of Copenhagen Denmark

ISBN: (纸本)9781450329378

We present a compiler and a typed intermediate language for a subset of APL. The intermediate language treats all numeric data as multi-dimensional arrays and the type system makes explicit the ranks of arrays. Primitive operators are polymorphic in rank and in the type of the underlying data operated on. The frontend of the APL compiler deals with much of the gory details of the APL language, including infix resolution, resolution of identity items for reduce operations, resolution of default element values for empty arrays, scalar extensions, and resolution of certain kinds of overloading. We demonstrate the usefulness of the intermediate language by showing that it can be compiled efficiently, using known techniques, such as delayed arrays, into a C-like language. We also demonstrate that the language is sufficiently expressive that some primitive operators, such as APL's inner product operator, which works on arrays of arbitrary dimensions, can be compiled using more primitive operators.. Copyright © 2014 acm 978-1-4503-2937-8/14/06. 15.00.

关键词： Calculations

来源：评论

学校读者我要写书评

暂无评论

Typed Lua: An optional type system for Lua

Typed Lua: An optional type system for Lua

引用

8th Workshop on Dynamic languages and Applications, Dyla 2014, with PLDI 2014

作者： Maidl, André Murbach Mascarenhas, Fabio Ierusalimschy, Roberto PUC-Rio Rio de Janeiro Brazil UFRJ Rio de Janeiro Brazil

ISBN: (纸本)9781450329163

Dynamically typed languages trade flexibility and ease of use for safety, while statically typed languages prioritize the early detection of bugs, and provide a better framework for structure large programs. The idea of optional typing is to combine the two approaches in the same language: the programmer can begin development with dynamic types, and migrate to static types as the program matures. The challenge is designing a type system that feels natural to the programmer that is used to programming in a dynamic language. This paper presents the initial design of Typed Lua, an optionally-typed extension of the Lua scripting language. Lua is an imperative scripting language with first class functions and lightweight metaprogramming mechanisms. The design of Typed Lua's type system has a novel combination of features that preserves some of the idioms that Lua programmers are used to, while bringing static type safety to them. We show how the major features of the type system type these idioms with some examples, and discuss some of the design issues we faced. © 2014 acm.

关键词： gradual typing Lua programming language optional typing type systems

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共129页 << < 45 46 47 48 49 50 51 52 53 54 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：