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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入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,080 篇 会议
132 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

1,046 篇 工学
- 982 篇 软件工程
- 752 篇 计算机科学与技术...
- 44 篇 控制科学与工程
- 42 篇 电气工程
- 32 篇 信息与通信工程
- 9 篇 电子科学与技术（可...
- 8 篇 机械工程
- 5 篇 土木工程
- 5 篇 安全科学与工程
- 4 篇 材料科学与工程（可...
- 4 篇 建筑学
- 4 篇 化学工程与技术
- 4 篇 航空宇航科学与技...
- 3 篇 生物工程
- 2 篇 光学工程
- 2 篇 冶金工程
- 2 篇 农业工程
126 篇 理学
- 106 篇 数学
- 12 篇 系统科学
- 8 篇 统计学（可授理学、...
- 5 篇 物理学
- 5 篇 生物学
- 4 篇 化学
81 篇 管理学
- 48 篇 管理科学与工程(可...
- 36 篇 图书情报与档案管...
- 26 篇 工商管理
12 篇 教育学
- 12 篇 教育学
6 篇 经济学
- 6 篇 应用经济学
5 篇 法学
- 4 篇 社会学
2 篇 农学
- 2 篇 作物学

主题

170 篇 design
157 篇 languages
100 篇 computer program...
96 篇 performance
57 篇 algorithms
49 篇 computer program...
47 篇 object oriented ...
43 篇 experimentation
39 篇 verification
35 篇 java programming...
34 篇 reliability
29 篇 functional progr...
26 篇 program synthesi...
26 篇 java
24 篇 probabilistic pr...
20 篇 concurrency
19 篇 domain-specific ...
19 篇 theory
17 篇 compilers
17 篇 type systems

机构

16 篇 carnegie mellon ...
13 篇 princeton univ p...
11 篇 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 篇 yale univ new ha...
9 篇 harvard univ cam...
9 篇 cornell univ ith...
8 篇 microsoft res re...
8 篇 univ chicago il ...
7 篇 microsoft res re...
7 篇 swiss fed inst t...
7 篇 mit cambridge ma...
7 篇 northeastern uni...

作者

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

语言

1,134 篇 英文
77 篇 其他
1 篇 中文

检索条件"任意字段=Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation"

共 1212 条记录，以下是311-320 订阅

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

详细简洁

排序：

Reconciling Exhaustive Pattern Matching with Objects

Reconciling Exhaustive Pattern Matching with Objects

引用

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

作者： Isradisaikul, Chinawat Myers, Andrew C. Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

ISBN: (纸本)9781450320146

Pattern matching, an important feature of functional languages, is in conflict with data abstraction and extensibility, which are central to object-oriented languages. Modal abstraction offers an integration of deep pattern matching and convenient iteration abstractions into an object-oriented setting;however, because of data abstraction, it is challenging for a compiler to statically verify properties such as exhaustiveness. In this work, we extend modal abstraction in the JMatch language to support static, modular reasoning about exhaustiveness and redundancy. New matching specifications allow these properties to be checked using an SMT solver. We also introduce expressive pattern-matching constructs. Our evaluation shows that these new features enable more concise code and that the performance of checking exhaustiveness and redundancy is acceptable.

关键词： JMatch pattern matching named constructor equality constructor matching specification exhaustiveness redundancy modal abstraction Java data abstraction subtyping design Verification languages

来源：评论

学校读者我要写书评

暂无评论

Automated Feedback Generation for Introductory programming Assignments

Automated Feedback Generation for Introductory Programming A...

引用

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

作者： Singh, Rishabh Gulwani, Sumit Solar-Lezama, Armando MIT CSAIL Cambridge MA USA Microsoft Res Redmond WA USA

ISBN: (纸本)9781450320146

We present a new method for automatically providing feedback for introductory programming problems. In order to use this method, we need a reference implementation of the assignment, and an error model consisting of potential corrections to errors that students might make. Using this information, the system automatically derives minimal corrections to student's incorrect solutions, providing them with a measure of exactly how incorrect a given solution was, as well as feedback about what they did wrong. We introduce a simple language for describing error models in terms of correction rules, and formally define a rule-directed translation strategy that reduces the problem of finding minimal corrections in an incorrect program to the problem of synthesizing a correct program from a sketch. We have evaluated our system on thousands of real student attempts obtained from the Introduction to programming course at MIT (6.00) and MITx (6.00x). Our results show that relatively simple error models can correct on average 64% of all incorrect submissions in our benchmark set.

关键词： Automated Grading Computer-Aided Education Program Synthesis

来源：评论

学校读者我要写书评

暂无评论

CONCURRIT: A Domain Specific language for Reproducing Concurrency Bugs

CONCURRIT: A Domain Specific Language for Reproducing Concur...

引用

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

作者： Elmas, Tayfun Burnim, Jacob Necula, George Sen, Koushik Univ Calif Berkeley Dept Elect Engn & Comp Sci Berkeley CA 94720 USA

ISBN: (纸本)9781450320146

We present CONCURRIT, a domain-specific language (DSL) for reproducing concurrency bugs. Given some partial information about the nature of a bug in an application, a programmer can write a CONCURRIT script to formally and concisely specify a set of thread schedules to explore in order to find a schedule exhibiting the bug. Further, the programmer can specify how these thread schedules should be searched to find a schedule that reproduces the bug. We implemented CONCURRIT as an embedded DSL in C++, which uses manual or automatic source instrumentation to partially control the scheduling of the software under test. Using CONCURRIT, we were able to write concise tests to reproduce concurrency bugs in a variety of benchmarks, including the Mozilla's Spider-Monkey JavaScript engine, Memcached, Apache's HTTP server, and MySQL.

关键词： Concurrency Errors Domain-Specific languages Software Testing

来源：评论

学校读者我要写书评

暂无评论

P: Safe Asynchronous Event-Driven programming

P: Safe Asynchronous Event-Driven Programming

引用

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

作者： Desai, Ankush Gupta, Vivek Jackson, Ethan Qadeer, Shaz Rajamani, Sriram Zufferey, Damien Microsoft Corp Redmond WA 98052 USA

ISBN: (纸本)9781450320146

We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to "close" the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code;a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhandled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P);we have more confidence in the robustness of its design due to the language abstractions and verification provided by P.

关键词： domain-specific language device driver event-driven programming state machine verification systematic testing

来源：评论

学校读者我要写书评

暂无评论

A General Constraint-centric Scheduling Framework for Spatial Architectures

A General Constraint-centric Scheduling Framework for Spatia...

引用

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

作者： Nowatzki, Tony Sartin-Tarm, Michael De Carli, Lorenzo Sankaralingam, Karthikeyan Estan, Cristian Robatmili, Behnam Univ Wisconsin Madison WI 53706 USA

ISBN: (纸本)9781450320146

Specialized execution using spatial architectures provides energy efficient computation, but requires effective algorithms for spatially scheduling the computation. Generally, this has been solved with architecture-specific heuristics, an approach which suffers from poor compiler/architect productivity, lack of insight on optimality, and inhibits migration of techniques between architectures. Our goal is to develop a scheduling framework usable for all spatial architectures. To this end, we expresses spatial scheduling as a constraint satisfaction problem using Integer Linear programming (ILP). We observe that architecture primitives and scheduler responsibilities can be related through five abstractions: placement of computation, routing of data, managing event timing, managing resource utilization, and forming the optimization objectives. We encode these responsibilities as 20 general ILP constraints, which are used to create schedulers for the disparate TRIPS, DySER, and PLUG architectures. Our results show that a general declarative approach using ILP is implementable, practical, and typically matches or outperforms specialized schedulers.

关键词： Spatial Architectures Spatial Architecture Scheduling Integer Linear programming

来源：评论

学校读者我要写书评

暂无评论

Fast Algorithms for Dyck-CFL-Reachability with Applications to Alias Analysis

Fast Algorithms for Dyck-CFL-Reachability with Applications ...

引用

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

作者： Zhang, Qirun Lyu, Michael R. Yuan, Hao Su, Zhendong Chinese Univ Hong Kong Hong Kong Hong Kong Peoples R China Univ Calif Davis Davis CA 95616 USA City Univ Hong Kong Hong Kong Hong Kong Peoples R China

ISBN: (纸本)9781450320146

The context-free language (CFL) reachability problem is a well-known fundamental formulation in program analysis. In practice, many program analyses, especially pointer analyses, adopt a restricted version of CFL-reachability, Dyck-CFL-reachability, and compute on edge-labeled bidirected graphs. Solving the all-pairs Dyck-CFL-reachability on such bidirected graphs is expensive. For a bidirected graph with n nodes and m edges, the traditional dynamic programming style algorithm exhibits a subcubic time complexity for the Dyck language with k kinds of parentheses. When the underlying graphs are restricted to bidirected trees, an algorithm with O(n log n log k) time complexity was proposed recently. This paper studies the Dyck-CFL-reachability problems on bidirected trees and graphs. In particular, it presents two fast algorithms with O(n) and O(n+m log m) time complexities on trees and graphs respectively. We have implemented and evaluated our algorithms on a state-of-the-art alias analysis for Java. Results on standard benchmarks show that our algorithms achieve orders of magnitude speedup and consume less memory.

关键词： Algorithms design Experimentation languages Dyck-CFL-reachability alias analysis

来源：评论

学校读者我要写书评

暂无评论

Harmonizing Classes, Functions, Tuples, and Type Parameters in Virgil III 13

Harmonizing Classes, Functions, Tuples, and Type Parameters ...

引用

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

作者： Titzer, Ben L. Google Mountain View CA USA

ISBN: (纸本)9781450320146

languages are becoming increasingly multi-paradigm. Subtype polymorphism in statically-typed object-oriented languages is being supplemented with parametric polymorphism in the form of generics. Features like first-class functions and lambdas are appearing everywhere. Yet existing languages like Java, C#, C++, D, and Scala seem to accrete ever more complexity when they reach beyond their original paradigm into another;inevitably older features have some rough edges that lead to nonuniformity and pitfalls. Given a fresh start, a new language designer is faced with a daunting array of potential features. Where to start? What is important to get right first, and what can be added later? What features must work together, and what features are orthogonal? We report on our experience with Virgil III, a practical language with a careful balance of classes, functions, tuples and type parameters. Virgil intentionally lacks many advanced features, yet we find its core feature set enables new species of design patterns that bridge multiple paradigms and emulate features not directly supported such as interfaces, abstract data types, ad hoc polymorphism, and variant types. Surprisingly, we find variance for function types and tuple types often replaces the need for other kinds of type variance when libraries are designed in a more functional style.

关键词： Multi-paradigm languages parametric types object-oriented programming functional programming monomorphization variance closures tuples flattening unboxing static compilation

来源：评论

学校读者我要写书评

暂无评论

Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths

Static Analysis for Probabilistic Programs: Inferring Whole ...

引用

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

作者： Sankaranarayanan, Sriram Chakarov, Aleksandar Gulwani, Sumit Univ Colorado Boulder CO 80309 USA Microsoft Res Redmond WA USA

ISBN: (纸本)9781450320146

We propose an approach for the static analysis of probabilistic programs that sense, manipulate, and control based on uncertain data. Examples include programs used in risk analysis, medical decision making and cyber-physical systems. Correctness properties of such programs take the form of queries that seek the probabilities of assertions over program variables. We present a static analysis approach that provides guaranteed interval bounds on the values (assertion probabilities) of such queries. First, we observe that for probabilistic programs, it is possible to conclude facts about the behavior of the entire program by choosing a finite, adequate set of its paths. We provide strategies for choosing such a set of paths and verifying its adequacy. The queries are evaluated over each path by a combination of symbolic execution and probabilistic volume-bound computations. Each path yields interval bounds that can be summed up with a "coverage" bound to yield an interval that encloses the probability of assertion for the program as a whole. We demonstrate promising results on a suite of benchmarks from many different sources including robotic manipulators and medical decision making programs.

关键词： Probabilistic programming Program Verification Volume Bounding Symbolic Execution Monte-Carlo Sampling

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共122页 << < 28 29 30 31 32 33 34 35 36 37 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：