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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

2,278 篇 会议
296 篇 期刊文献
2 册 图书

馆藏范围

2,576 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

2,280 篇 工学
- 2,147 篇 软件工程
- 1,702 篇 计算机科学与技术...
- 85 篇 控制科学与工程
- 57 篇 信息与通信工程
- 55 篇 电气工程
- 23 篇 电子科学与技术（可...
- 17 篇 机械工程
- 14 篇 建筑学
- 14 篇 土木工程
- 13 篇 材料科学与工程（可...
- 13 篇 生物工程
- 10 篇 光学工程
- 9 篇 安全科学与工程
- 8 篇 化学工程与技术
- 5 篇 动力工程及工程热...
- 5 篇 生物医学工程（可授...
- 4 篇 力学（可授工学、理...
278 篇 理学
- 217 篇 数学
- 30 篇 系统科学
- 18 篇 统计学（可授理学、...
- 16 篇 物理学
- 16 篇 生物学
- 8 篇 化学
- 6 篇 地质学
207 篇 管理学
- 112 篇 图书情报与档案管...
- 107 篇 管理科学与工程(可...
- 48 篇 工商管理
22 篇 教育学
- 22 篇 教育学
17 篇 法学
- 15 篇 社会学
9 篇 经济学
- 9 篇 应用经济学
2 篇 农学
2 篇 艺术学
1 篇 军事学

主题

390 篇 design
369 篇 languages
186 篇 computer program...
182 篇 performance
162 篇 object oriented ...
89 篇 algorithms
88 篇 java programming...
81 篇 experimentation
78 篇 functional progr...
71 篇 theory
69 篇 computer program...
65 篇 java
63 篇 verification
61 篇 reliability
48 篇 semantics
47 篇 software design
45 篇 domain-specific ...
38 篇 parallel program...
37 篇 concurrency
35 篇 measurement

机构

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

作者

19 篇 hirschfeld rober...
16 篇 walker david
15 篇 visser eelco
15 篇 felleisen matthi...
14 篇 findler robert b...
13 篇 grossman dan
13 篇 bacon david f.
12 篇 chlipala adam
11 篇 flatt matthew
11 篇 sarkar vivek
11 篇 myers andrew c.
11 篇 mezini mira
11 篇 morrisett greg
10 篇 mckinley kathryn...
10 篇 bockisch christo...
10 篇 adl-tabatabai al...
10 篇 de moor oege
10 篇 dillig isil
9 篇 lumsdaine a
9 篇 van der storm ti...

语言

2,349 篇 英文
222 篇 其他
4 篇 中文
1 篇 葡萄牙文

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

共 2576 条记录，以下是1101-1110 订阅

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

详细简洁

排序：

Effective Interactive Proofs for Higher-Order Imperative Programs

Effective Interactive Proofs for Higher-Order Imperative Pro...

引用

14th acm sigplan International conference on Functional programming

作者： Chlipala, Adam Malecha, Gregory Morrisett, Greg Shinnar, Avraham Wisnesky, Ryan Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781605583327

We present a new approach for constructing and verifying higher-order, imperative programs using the Coq proof assistant. We build on the past work on the Ynot system, which is based on Hoare Type Theory. That original system was a proof of concept, where every program verification was accomplished via laborious manual proofs, with much code devoted to uninteresting low-level details. In this paper, we present a re-implementation of Ynot which makes it possible to implement fully-verified, higher-order imperative programs with reasonable proof burden. At the same time, our new system is implemented entirely in Coq source files, showcasing the versatility of that proof assistant as a platform for research on language design and verification. Both versions of the system have been evaluated with case studies in the verification of imperative data structures, such as hash tables with higher-order iterators. The verification burden in our new system is reduced by at least an order of magnitude compared to the old system, by replacing manual proof with automation. The core of the automation is a simplification procedure for implications in higher-order separation logic, with hooks that allow programmers to add domain-specific simplification rules. We argue for the effectiveness of our infrastructure by verifying a number of data structures and a packrat parser, and we compare to similar efforts within other projects. Compared to competing approaches to data structure verification, our system includes much less code that must be trusted;namely, about a hundred lines of Coq code defining a program logic. All of our theorems and decision procedures have or build machine-checkable correctness proofs from first principles, removing opportunities for tool bugs to create faulty verifications.

关键词： functional programming interactive proof assistants dependent types separation logic

来源：评论

学校读者我要写书评

暂无评论

Secure compilation of a multi-tier web language

Secure compilation of a multi-tier web language

引用

2009 acm sigplan Workshop on Types in language design and implementation, TLDI'09

作者： Baltopoulos, Ioannis G. Gordon, Andrew D. University of Cambridge Computer Laboratory United Kingdom Microsoft Research

ISBN: (纸本)9781605584201

Storing state in the client tier (in forms or cookies, for example) the efficiency of a web application, but it also renders secrecy and integrity of stored data vulnerable to untrustworthy. We study this general problem in the context of LINKS multi-tier programming language. Like other systems,INKS stores unencrypted application data, including web continuations, the client tier;hence, LINKS is open to attacks that secrets, and modify control flow and application data. We these attacks as failures of the general principle that properties of multi-tier applications should follow from review the source code (as opposed to the detailed study of the files for each tier, for example). We eliminate these threats by the LINKS compiler to encrypt and authenticate any stored on the client. We model this compilation strategy as a from a core fragment of the language to a concurrent l-equipped with a formal representation of cryptography. To source-level reasoning about LINKS programs, we define type-and-effect system for our core language;our implementation machine-check various integrity properties of the source code. appeal to a recent system of refinement types for secure implementations,show that our compilation strategy guarantees all the properties provable by our type-and-effect system. © 2009 acm.

关键词： Cryptography

来源：评论

学校读者我要写书评

暂无评论

Software Transactional Memory for Multicore Embedded Systems 09

Software Transactional Memory for Multicore Embedded Systems

引用

acm sigplan/SIGBED conference on languages, Compilers and Tool for Embedded Systems

作者： Mankin, Jennifer Kaeli, David Ardini, John Northeastern Univ Boston MA 02115 USA Charles Stark Draper Lab Inc Cambridge MA 02139 USA

ISBN: (纸本)9781605583563

Embedded systems, like general-purpose systems, can benefit from parallel execution on a symmetric multicore platform. Unfortunately, concurrency issues present in general-purpose programming also apply to embedded systems, protection from which is currently only offered with performance-limiting coarse-grained locking or error-prone and difficult-to-implement fine-grained locking. Transactional memory offers relief from these mechanisms, but has primarily been investigated on general-purpose systems. In this paper, we present Embedded Software Transactional Memory (ESTM) as a novel solution to the concurrency problem in parallel embedded applications. We investigate common software transactional memory design decisions and discuss the best decisions for an embedded platform. We offer a full implementation of an embedded STM and test it against both coarse-grained and fine-grained locking mechanisms. We find that we can meet or beat the performance of fine-grained locking over a range of application characteristics, including size of shared data, time spent in the critical section, and contention between threads. Our ESTM implementation benefits from the effective use of L1 memory, a feature which is built into our STM model but which cannot be directly utilized by traditional locking mechanisms.

关键词： design Experimentation Performance Embedded Systems Multicore Software Transactional Memory (STM) Synchronization Locking Transactions

来源：评论

学校读者我要写书评

暂无评论

Complementing Ada with Other programming languages 09

Complementing Ada with Other Programming Languages

引用

acm International conference on Ada and Related Technologies

作者： Tardieu, Samuel Polti, Alexis Telecom ParisTech Inst Telecom Networks & Comp Sci Dept Paris France

ISBN: (纸本)9781605584751

This paper presents our experience in using Ada and the Ravenscar profile in a robotics non-profit association and in a robotics competition. While Ada is our primary and dominant language, we have complemented it with a hardware description language (Verilog) and an interactive language (Forth). We describe the interface between those languages, and the design choices that have been made to minimize the risks taken by leaving the Ada world. We also explain why we chose in some conditions to relax restrictions imposed by the use of the Ravenscar profile.

关键词： Robotics FPGA Ravenscar high integrity profile Ada streams hardware interface

来源：评论

学校读者我要写书评

暂无评论

Multiparadigm programming in Object-Oriented languages: Current Research Report on the Workshop MPOOL'08 at ECOOP 2008

引用

22nd European conference on Object-Oriented programming (ECOOP 2008)

作者： Striegnitz, Joerg Davis, Kei Univ Appl Sci Regensburg D-93053 Regensburg Germany Los Alamos Natl Lab Los Alamos 87545 NM USA

ISBN: (纸本)9783642020469

While OO has, become ubiquitously employed for design;implementation, and even conceptualization, many practitioners recognize the concomitant need for other programming paradigms according to problem domain. Nevertheless, the choice of a programming paradigm is strongly influenced by the supporting programming language facilities. In turn, choice of programming language is usually highly constrained by practical considerations. We seek answers to the question of how to address the need for other programming paradigms, or even domain specific languages, in the general context of OO languages. It is clear that this field is active and fluid: novel, disparate approaches' and techniques are still being discovered or invented, And this very novelty adds a. significant element of intellectual entertainment. This article describes the cross section of research efforts reported at the, workshop on Multiparadigm programming in Object-Oriented languages held at, the 2008 European conference on Object-Oriented programming.

关键词： C# 3.0 CLOS Closures Delegates design patterns Eiffel Extension methods Function objects Functional programming Java 7 Multiparadigm programming Object-oriented programming OCaml Open classes Scala Smalltalk

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the 3rd Workshop on Virtual Machines and Intermediate languages, VMIL 2009, held at the 24th acm sigplan conference on Object-Oriented programming, Systems, languages, and Applications

Proceedings of the 3rd Workshop on Virtual Machines and Inte...

引用

3rd Workshop on Virtual Machines and Intermediate languages, VMIL 2009, held at the 24th acm sigplan conference on Object-Oriented programming, Systems, languages, and Applications

ISBN: (纸本)9781605588742

The proceedings contain 5 papers. The topics discussed include: virtual class support at the virtual machine level;bytecodes meet combinators: invokedynamic on the JVM;intermediate language design of high-level language virtual machines: towards comprehensive concurrency support;@J - towards rapid development of dynamic analysis tools for the Java virtual machine;challenging VMs on battery-powered embedded devices;and VM performance evaluation with functional models: an optimist's outlook.

关键词：

来源：评论

学校读者我要写书评

暂无评论

The Art of the Meta-Aspect Protocol 09

The Art of the Meta-Aspect Protocol

引用

8th International conference on Aspect-Oriented Software Development

作者： Dinkelaker, Tom Mezini, Mira Bockisch, Christoph Tech Univ Darmstadt Darmstadt Germany

ISBN: (纸本)9781605584423

Alternative semantics for aspect-oriented abstractions can be defined by language designers using extensible aspect compiler frameworks. However, application developers are prevented from tailoring the language semantics in an application-specific manner. To address this problem, we propose art architecture for aspect-oriented languages with an explicit meta-interface to language semantics. We demonstrate the benefits of such an architecture by presenting several scenarios in which aspect-oriented programs use the meta-interface of the language to tailor its semantics to a particular application execution context.

关键词： Aspect-Oriented programming Meta-Object Protocols Open implementation Debugging Aspect Interactions

来源：评论

学校读者我要写书评

暂无评论

Opis: Reliable Distributed Systems in OCaml

Opis: Reliable Distributed Systems in OCaml

引用

2009 acm sigplan Workshop on Types in language design and implementation, TLDI'09

作者： Dagand, Pierre-Évariste Kostic, Dejan Kuncak, Viktor ENS Cachan-Bretagne France EPFL Switzerland

ISBN: (纸本)9781605584201

Concurrency and distribution pose algorithmic and implementation in developing reliable distributed systems, the field an excellent testbed for evaluating language and verification paradigms. Several domain-specific languages and extensions of unsafe languages were proposed to aid distributed development. We present an alternative to these, showing that modern, higher-order, strongly, memory safe languages provide an excellent vehicle developing and debugging distributed systems. present Opis, a functional-reactive approach for developing systems in Objective Caml. An Opis description consists of a reactive function (called function) describing the behavior of a distributed system. The event functions in Opis are built from pure as building blocks, composed using the Arrow combinators. architecture aids reasoning about event functions informally and using interactive theorem provers. example, it facilitates simple termination arguments. a protocol description, a developer can use higherorder functions of Opis to 1) deploy the distributed, 2) run the distributed system in a network simulator full-replay capabilities, 3) apply explicit-state model to the distributed system, detecting undesirable behaviors, 4) do performance analysis on the system. We the design and implementation of Opis, and present experience in using Opis to develop peer-to-peer overlay, including the Chord distributed hash table and Cyclon random gossip protocol. We found that using results in high programmer productivity and leads to composable protocol descriptions. Opis tools were effective helping identify and eliminate correctness and performanceduring distributed system development. © 2009 acm.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

Versatile language semantics with reflective embedding

Versatile language semantics with reflective embedding

引用

OOPSLA 2009 Companion - 24th Annual acm conference on Object-Oriented programming, Systems, languages and Applications, OOPSLA 2009

作者： Dinkelaker, Tom Technische Universität Darmstadt Hochschulstr. 10 64289 Darmstadt Germany

ISBN: (纸本)9781605587660

Often, for one programming language, various implementations exist that have subtle but important variations in their syntax and semantics. While current technology provides good support for syntax variability in form of syntax extensions, there is only limited support for semantic variability in language implementations. My thesis is about a novel approach for adaptable language implementations that uses a meta-object protocol to embed language abstractions into the host language and that uses reflective techniques to adapt the language implementation. The techniques developed in my thesis open up several possibilities for adaptation in language implementations not addressed by related work. Similarly to the role of a meta-object protocol in general-purpose languages for adapting object-oriented abstractions, the meta-object protocol allows to adapt language abstractions of advanced language features, such as the abstractions of aspect-oriented programming and domain abstractions in domain-specific languages.

关键词： Aspect oriented programming

来源：评论

学校读者我要写书评

暂无评论

Debug All Your Code: Portable Mixed-Environment Debugging 09

Debug All Your Code: Portable Mixed-Environment Debugging

引用

24th Annual acm conference on Object-Oriented programming, Systems, languages and Applications

作者： Lee, Byeongcheol Hirzel, Martin Grimm, Robert McKinley, Kathryn S. Univ Texas Austin Austin TX 78712 USA NYU New York NY 10003 USA

ISBN: (纸本)9781605587660

Programmers build large-scale systems with multiple languages to reuse legacy code and leverage languages best suited to their problems. For instance, the same program may use Java for ease-of-programming and C to interface with the operating system. These programs pose significant debugging challenges, because programmers need to understand and control code across languages, which may execute in different environments. Unfortunately, traditional multilingual debuggers require a single execution environment. This paper presents a novel composition approach to building portable mixed-environment debuggers, in which an intermediate agent interposes on language transitions, controlling and reusing single-environment debuggers. We implement debugger composition in Blink, a debugger for Java, C, and the Jeannie programming language. We show that Blink is (1) relatively simple: it requires modest amounts of new code;(2) portable: it supports multiple Java Virtual Machines, C compilers, operating systems, and component debuggers;and (3) powerful: composition eases debugging, while supporting new mixed-language expression evaluation and Java Native Interface (JNI) bug diagnostics. In real-world case studies, we show that language-interface errors require single-environment debuggers to restart execution multiple times, whereas Blink directly diagnoses them with one execution. We also describe extensions for other mixed-environments to show debugger composition will generalize.

关键词： languages design Reliability Foreign Function Interface JNI Composition

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共258页 << < 107 108 109 110 111 112 113 114 115 116 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：