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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

250 篇 会议
5 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

210 篇 工学
- 202 篇 软件工程
- 92 篇 计算机科学与技术...
- 7 篇 电气工程
- 3 篇 控制科学与工程
- 1 篇 动力工程及工程热...
- 1 篇 电子科学与技术（可...
- 1 篇 生物工程
7 篇 理学
- 6 篇 数学
- 1 篇 生物学
5 篇 管理学
- 4 篇 管理科学与工程(可...
- 2 篇 工商管理
- 1 篇 图书情报与档案管...
2 篇 经济学
- 2 篇 应用经济学
2 篇 教育学
- 2 篇 教育学

主题

49 篇 design
40 篇 languages
22 篇 performance
15 篇 algorithms
14 篇 probabilistic pr...
12 篇 verification
12 篇 functional progr...
11 篇 program synthesi...
10 篇 object oriented ...
10 篇 reliability
10 篇 concurrency
9 篇 experimentation
9 篇 programming lang...
8 篇 type systems
8 篇 domain-specific ...
7 篇 java
6 篇 optimization
6 篇 theory
5 篇 compilers
5 篇 metaprogramming

机构

8 篇 purdue univ w la...
7 篇 carnegie mellon ...
6 篇 harvard univ cam...
5 篇 univ penn philad...
4 篇 univ wisconsin m...
4 篇 princeton univ p...
4 篇 univ calif davis...
4 篇 northeastern uni...
4 篇 cornell univ ith...
4 篇 stanford univ st...
4 篇 univ washington ...
3 篇 microsoft res re...
3 篇 swiss fed inst t...
3 篇 mit cambridge ma...
3 篇 yale univ new ha...
3 篇 rice univ housto...
3 篇 univ calif berke...
3 篇 univ texas austi...
2 篇 microsoft corp r...
2 篇 oracle labs pots...

作者

5 篇 foster nate
5 篇 gulwani sumit
5 篇 walker david
4 篇 dillig isil
3 篇 ahmed amal
3 篇 huang jeff
3 篇 vechev martin
3 篇 shao zhong
3 篇 tobin-hochstadt ...
3 篇 su zhendong
3 篇 chaudhuri swarat
3 篇 felleisen matthi...
3 篇 myers andrew c.
3 篇 zhang xiangyu
3 篇 acar umut a.
3 篇 mansinghka vikas...
2 篇 hirschfeld rober...
2 篇 flatt matthew
2 篇 gupta gagan
2 篇 shull thomas

语言

251 篇 英文
3 篇 其他
1 篇 中文

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

共 255 条记录，以下是171-180 订阅

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

详细简洁

排序：

MORBIG: A Static Parser for POSIX Shell 11

MORBIG: A Static Parser for POSIX Shell

引用

11th acm sigplan International conference on Software language Engineering (SLE) part of SPLASH conference

作者： Regis-Gianas, Yann Jeannerod, Nicolas Treinen, Ralf Univ Paris Diderot CNRS INRIA IRIFPI R2 Paris France Univ Paris Diderot CNRS IRIF Ecole Normale Super Paris France Univ Paris Diderot CNRS IRIF Paris France

ISBN: (纸本)9781450360296

the POSIX shell language defies conventional wisdom of compiler construction on several levels: the shell language was not designed for static parsing, but with an intertwining of syntactic analysis and execution by expansion in mind. Token recognition cannot be specified by regular expressions, lexical analysis depends on the parsing context and the evaluation context, and the shell grammar given in the specification is ambiguous. Besides, the unorthodox design choices of the shell language fit badly in the usual specification languages used to describe other programming languages. this makes the standard usage of LEX and YACC as a pipeline inadequate for the implementation of a parser for POSIX shell. the existing implementations of shell parsers are complex and use low-level character-level parsing code which is difficult to relate to the POSIX specification. We find it hard to trust such parsers, especially when using them for writing automatic verification tools for shell scripts. this paper offers an overview of the technical difficulties related to the syntactic analysis of the POSIX shell language. It also describes how we have resolved these difficulties using advanced parsing techniques (namely speculative parsing, parser state introspection, context-dependent lexical analysis and longest-prefix parsing) while keeping the implementation at a sufficiently high level of abstraction so that experts can check that the POSIX standard is respected. the resulting tool, called MORBIG, is an open-source static parser for a well-defined and realistic subset of the POSIX shell language.

关键词： Parsing POSIX shell functional programming

来源：评论

学校读者我要写书评

暂无评论

Scala 2018 - proceedings of the 9th acm sigplan International Symposium on Scala, co-located with ICFP 2018

Scala 2018 - Proceedings of the 9th ACM SIGPLAN Internationa...

引用

9th acm sigplan International Symposium on Scala, Scala 2018, Part of the acm sigplan International conference on Functional programming, ICFP 2018

ISBN: (纸本)9781450358361

the proceedings contain 9 papers. the topics discussed include: a domain-specific language for microservices;parser combinators for context-free path querying;garnishing parsec with parsley;path dependent types with path-equality;kDOT: scaling DOT with mutation and constructors;truly abstract interfaces for algebraic data types: the extractor typing problem;interflow: interprocedural flow-sensitive type inference and method duplication;and extending scala with records: design, implementation, and evaluation.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Input Responsiveness: Using Canary Inputs to Dynamically Steer Approximation 16

Input Responsiveness: Using Canary Inputs to Dynamically Ste...

引用

37th acm sigplan conference on programming language design and implementation

作者： Laurenzano, Michael A. Hill, Parker Samadi, Mehrzad Mahlke, Scott Mars, Jason Tang, Lingjia Univ Michigan Dept Elect Engn & Comp Sci Ann Arbor MI 48109 USA

ISBN: (纸本)9781450342612

this paper introduces Input Responsive Approximation ( IRA), an approach that uses a canary input - a small program input carefully constructed to capture the intrinsic properties of the original input - to automatically control how program approximation is applied on an input-by-input basis. Motivating this approach is the observation that many of the prior techniques focusing on choosing how to approximate arrive at conservative decisions by discounting substantial differences between inputs when applying approximation. the main challenges in overcoming this limitation lie in making the choice of how to approximate both effectively (e.g., the fastest approximation that meets a particular accuracy target) and rapidly for every input. With IRA, each time the approximate program is run, a canary input is constructed and used dynamically to quickly test a spectrum of approximation alternatives. Based on these runtime tests, the approximation that best fits the desired accuracy constraints is selected and applied to the full input to produce an approximate result. We use IRA to select and parameterize mixes of four approximation techniques from the literature for a range of 13 image processing, machine learning, and data mining applications. Our results demonstrate that IRA significantly outperforms prior approaches, delivering an average of 10.2x speedup over exact execution while minimizing accuracy losses in program outputs.

关键词： Performance Runtime Systems Compilers Approximate Computing Performance Experimentation design

来源：评论

学校读者我要写书评

暂无评论

Developing a stage lighting system for scratch

Developing a stage lighting system for scratch

引用

6th acm sigplan Internatinal conference on Functional programming (ICFP'01)

作者： Sperber, M. Wilhelm-Schickard-Institut fur Info. Universität Tübingen Tübingen Germany

Lula is a system for computer-assisted stage lighting design and control. Whereas other systems for the same purpose are usually the results of long chains of incremental improvements of historic concepts. Lula represents a complete redesign. Whereas other systems focus on control aspects of lighting. Lula focuses on design and generates control information from it. this approach gives significantly more flexibility to the lighting designer and shortens the design process itself. Lula's design and implementation draw from a number of disciplines in advanced programming. It is written in Scheme and runs atop PLT Scheme, and benefits from its high-level GUI library. Lula uses an algebraic model for lighting looks based on just three combinators. It employs Functional Reactive programming for all dynamic aspects of lighting, and is programmable via a functional-reactive domain-specific language. Lula is an actual product and has users who have neither interest in nor knowledge of functional programming.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

LaminarIR: Compile-Time Queues for Structured Streams 15

LaminarIR: Compile-Time Queues for Structured Streams

引用

36th acm sigplan conference on programming language design and implementation

作者： Ko, Yousun Burgstaller, Bernd Scholz, Bernhard Yonsei Univ Seoul 120749 South Korea Univ Sydney Sydney NSW 2006 Australia

ISBN: (纸本)9781450334686

Stream programming languages employ FIFO (first-in, first-out) semantics to model data channels between producers and consumers. A FIFO data channel stores tokens in a buffer that is accessed indirectly via read-and write-pointers. this indirect token-access decouples a producer's write-operations from the read-operations of the consumer, thereby making dataflow implicit. For a compiler, indirect token-access obscures data-dependencies, which renders standard optimizations ineffective and impacts stream program performance negatively. In this paper we propose a transformation for structured stream programming languages such as StreamIt that shifts FIFO buffer management from run-time to compile-time and eliminates splitters and joiners, whose task is to distribute and merge streams. To show the effectiveness of our lowering transformation, we have implemented a StreamIt to C compilation framework. We have developed our own intermediate representation (IR) called LaminarIR, which facilitates the transformation. We report on the enabling effect of the LaminarIR on LLVM's optimizations, which required the conversion of several standard StreamIt benchmarks from static to randomized input, to prevent computation of partial results at compile-time. We conducted our experimental evaluation on the Intel i7-2600K, AMD Opteron 6378, Intel Xeon Phi 3120A and ARM Cortex-A15 platforms. Our LaminarIR reduces data-communication on average by 35.9% and achieves platform-specific speedups between 3.73x and 4.98x over StreamIt. We reduce memory accesses by more than 60% and achieve energy savings of up to 93.6% on the Intel i7-2600K.

关键词： languages Algorithms Performance stream programming synchronous data flow program transformation performance analysis compiler optimization

来源：评论

学校读者我要写书评

暂无评论

End-to-End Verification of Information-Flow Security for C and Assembly Programs 16

End-to-End Verification of Information-Flow Security for C a...

引用

37th acm sigplan conference on programming language design and implementation

作者： Costanzo, David Shao, Zhong Gu, Ronghui Yale Univ New Haven CT 06520 USA

ISBN: (纸本)9781450342612

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly;we verify all of the code, regardless of language.

关键词： Verification Security Reliability languages design Information Flow Control Security Policy Specification Security-Preserving Simulation Program Verification Certified OS Kernels

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Classbox/J: Controlling the scope of change in Java

Classbox/J: Controlling the scope of change in Java

引用

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

作者： Bergel, A Ducasse, S Nierstrasz, O Univ Bern Software Composit Grp Bern Switzerland Univ Savoie Language & Software Evolut Grp LISTIC Chambery France

Unanticipated changes to complex software systems can introduce anomalies such as duplicated code, suboptimal inheritance relationships and a proliferation of run-tirne downcasts. Refactoring to eliminate these anomalies may not be an option, at least in certain stages of software evolution. Classboxes are modules that restrict the visibility of changes to selected clients only, thereby offering more freedom in the way unanticipated changes may be implemented, and thus reducing the need for convoluted design anomalies. In this paper we demonstrate how classboxes can be implemented in statically-typed languages like Java. We also present an extended case study of Swing, a Java GUI package built on top of AWT, and we document the ensuing anomalies that Swing introduces. We show how Classbox/J, a prototype implementation of classboxes for Java, is used to provide a cleaner implementation of Swing using local refinement rather than subclassing.

关键词： language design module package open-classes class extension

来源：评论

学校读者我要写书评

暂无评论

Multiple instances and symbolic variables in executable sequence charts 02

Multiple instances and symbolic variables in executable sequ...

引用

17th Meeting on Object-Oriented programming, Systems, languages and Applications (OOPSLA 2002)

作者： Marelly, R Harel, D Kugler, H Weizmann Inst Sci Dept Comp Sci & Appl Math IL-76100 Rehovot Israel

ISBN: (纸本)9781581134711

We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. the extension involves support for instances that can bind to multiple objects and symbolic variables that can bind to arbitrary values. the result is a powerful executable language for expressing behavioral requirements on the level of inter-object interaction. the extension is implemented in full in our play-engine tool, with which one can execute the requirements directly without the need to build or synthesize an intra-object system model. It seems that in addition to many advantages in testing and requirements engineering, for some kinds of systems this could lead to the requirements actually serving as the final implementation.

关键词： design languages verification

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共26页 << < 14 15 16 17 18 19 20 21 22 23 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：