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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

69 篇 会议
1 册 图书
1 篇 期刊文献

馆藏范围

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

日期分布

学科分类号

59 篇 工学
- 57 篇 软件工程
- 48 篇 计算机科学与技术...
- 4 篇 控制科学与工程
- 3 篇 信息与通信工程
- 1 篇 光学工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 纺织科学与工程
- 1 篇 生物工程
- 1 篇 安全科学与工程
11 篇 理学
- 8 篇 数学
- 3 篇 系统科学
- 1 篇 物理学
- 1 篇 生物学
- 1 篇 统计学（可授理学、...
7 篇 管理学
- 5 篇 图书情报与档案管...
- 2 篇 管理科学与工程(可...
- 1 篇 工商管理

主题

5 篇 design
3 篇 program synthesi...
3 篇 languages
3 篇 probabilistic pr...
3 篇 software design
3 篇 java programming...
3 篇 programming by e...
3 篇 programming lang...
2 篇 object oriented ...
2 篇 experimentation
2 篇 performance
2 篇 compilers
2 篇 modules
2 篇 intel ixa
2 篇 parallel program...
2 篇 java
2 篇 register allocat...
2 篇 bank assignment
2 篇 composition
2 篇 end-user program...

机构

3 篇 univ michigan an...
3 篇 carnegie mellon ...
3 篇 univ penn philad...
2 篇 university of to...
2 篇 kyushu institute...
2 篇 kyushu universit...
2 篇 univ chicago il ...
2 篇 univ calif santa...
2 篇 univ texas austi...
1 篇 programming tool...
1 篇 google ca united...
1 篇 univ wisconsin d...
1 篇 univ southern ca...
1 篇 mpi sws saarbruc...
1 篇 univ wisconsin m...
1 篇 radboud univ nij...
1 篇 network speed te...
1 篇 institute for co...
1 篇 university of ma...
1 篇 university of tw...

作者

2 篇 wang xinyu
2 篇 sherwood timothy
2 篇 fursin grigori
2 篇 chong frederic t...
2 篇 alur rajeev
2 篇 hardekopf ben
2 篇 dillig isil
1 篇 milano matthew
1 篇 blinn andrew
1 篇 tao runzhou
1 篇 kashyap vineeth
1 篇 pailoor shankara
1 篇 campagna giovann...
1 篇 fedorova alexand...
1 篇 collins nick
1 篇 sewe andreas
1 篇 lerner sorin
1 篇 best micah j.
1 篇 f.r.m. barnes
1 篇 ekman torbjorn

语言

71 篇 英文

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

共 71 条记录，以下是21-30 订阅

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

详细简洁

排序：

Synthesizing Data Structure Refinements from Integrity Constraints 2021

Synthesizing Data Structure Refinements from Integrity Const...

引用

42nd acm sigplan International conference on programming language design and implementation (PLDI)

作者： Pailoor, Shankara Wang, Yuepeng Wang, Xinyu Dillig, Isil Univ Texas Austin Austin TX 78712 USA Univ Penn Philadelphia PA 19104 USA Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9781450383912

implementations of many data structures use several correlated fields to improve their performance;however, inconsistencies between these fields can be a source of serious program errors. To address this problem, we propose a new technique for automatically refining data structures from integrity constraints. In particular, consider a data structure D with fields F and methods M, as well as a new set of auxiliary fields F' that should be added to D. Given this input and an integrity constraint Phi relating F and F', our method automatically generates a refinement of.. that satisfies the provided integrity constraint. Our method is based on a modular instantiation of the CEGIS paradigm and uses a novel inductive synthesizer that augments top-down search with three key ideas. First, it computes necessary preconditions of partial programs to dramatically prune its search space. Second, it augments the grammar with promising new productions by leveraging the computed preconditions. Third, it guides top-down search using a probabilistic context-free grammar obtained by statically analyzing the integrity checking function and the original code base. We evaluated our method on 25 data structures from popular Java projects and show that our method can successfully refine 23 of them. We also compare our method against two state-of-the-art synthesis tools and perform an ablation study to justify our design choices. Our evaluation shows that (1) our method is successful at refining many data structure implementations in the wild, (2) it advances the state-of-the-art in synthesis, and (3) our proposed ideas are crucial for making this technique practical.

关键词： programming languages Program Synthesis Data structure refinement

来源：评论

学校读者我要写书评

暂无评论

SOAP 2021 - proceedings of the 10th acm sigplan International Workshop on the State of the Art in Program Analysis, co-located with PLDI 2021

SOAP 2021 - Proceedings of the 10th ACM SIGPLAN Internationa...

引用

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

ISBN: (纸本)9781450384681

The proceedings contain 8 papers. The topics discussed include: static analysis for dummies: experiencing LiSA;security and quality: two sides of the same coin?;program analysis for reversible languages;PerfLens: a data-driven performance bug detection and fix platform;Weldr: fusing binaries for simplified analysis;multi-language static code analysis on the LARA framework;serialization-aware call graph construction;and scalable string analysis: an experience report.

关键词：

来源：评论

学校读者我要写书评

暂无评论

MixT: A language for Mixing Consistency in Geodistributed Transactions 2018

MixT: A Language for Mixing Consistency in Geodistributed Tr...

引用

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

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

ISBN: (纸本)9781450356985

programming concurrent, distributed systems is hard-especially when these systems mutate shared, persistent state replicated at geographic scale. To enable high availability and scalability, a new class of weakly consistent data stores has become popular. However, some data needs strong consistency. To manipulate both weakly and strongly consistent data in a single transaction, we introduce a new abstraction: mixed-consistency transactions, embodied in a new embedded language, MixT. Programmers explicitly associate consistency models with remote storage sites;each atomic, isolated transaction can access a mixture of data with different consistency models. Compile-time information-flow checking, applied to consistency models, ensures that these models are mixed safely and enables the compiler to automatically partition transactions. New run-time mechanisms ensure that consistency models can also be mixed safely, even when the data used by a transaction resides on separate, mutually unaware stores. Performance measurements show that despite their stronger guarantees, mixed-consistency transactions retain much of the speed of weak consistency, significantly outperforming traditional serializable transactions.

关键词： Consistency Transactions Information Flow

来源：评论

学校读者我要写书评

暂无评论

Exadapt'11 - proceedings of the 1st International Workshop on Adaptive Self-Tuning Computing Systems for the Exaflop Era - In Cooperation with the 32nd acm sigplan conference on programming language design and implementation, PLDI 2011

Exadapt'11 - Proceedings of the 1st International Workshop o...

引用

1st acm sigplan International Workshop on Adaptive Self-Tuning Computing Systems for the Exaflop Era, Exadapt 2011 - Co-located with 32nd acm sigplan conference on programming language design and implementation, PLDI 2011 at FCRC 2011

ISBN: (纸本)9781450307086

The proceedings contain 7 papers. The topics discussed include: AARTS: low overhead online adaptive auto-tuning;contentiousness vs. sensitivity: improving contention aware runtime systems on multicore architectures;probabilistic auto-tuning for architectures with complex constraints;efficiently exploring compiler optimization sequences with pair-wise pruning;adapt or become extinct!;loaf: a framework and infrastructure for creating online adaptive solutions;and using a codelet program execution model for exascale machines.

关键词： Software architecture

来源：评论

学校读者我要写书评

暂无评论

ContextErlang: Introducing context-oriented programming in the actor model 12

ContextErlang: Introducing context-oriented programming in t...

引用

11th Annual International conference on Aspect Oriented Software Development, AOSD'12

作者： Salvaneschi, Guido Ghezzi, Carlo Pradella, Matteo DEEPSE Group DEI Politecnico di Milano Piazza L. Da Vinci 32 Milano Italy

ISBN: (纸本)9781450310925

Self-adapting systems are becoming widespread in emerging fields such as autonomic, mobile and ubiquitous computing. Context-oriented programming (COP) is a promising language-level solution for the implementation of context-aware, self-adaptive software. However, current COP approaches struggle to effectively manage the asynchronous nature of context provisioning. We argue that, to solve these issues, COP features should be designed to fit nicely in the concurrency model supported by the language. This work presents the design rationale of CONTEXTERLANG, which introduces COP in the Actor Model. We provide evidence that CONTEXTERLANG constitutes a viable solution to implement context-aware software in a highly concurrent and distributed setting. We discuss a case study and an evaluation of run-time performance. © 2012 acm.

关键词： Ubiquitous computing

来源：评论

学校读者我要写书评

暂无评论

PLDI'11 - proceedings of the 2011 acm conference on programming language design and implementation

PLDI'11 - Proceedings of the 2011 ACM Conference on Programm...

引用

32nd acm conference on programming language design and implementation, PLDI 2011

ISBN: (纸本)9781450306638

The proceedings contain 55 papers. The topics discussed include: commutative set: a language extension for implicit parallel programming;the Tao of parallelism in algorithms;data representation synthesis;synthesizing geometry constructions;synthesis of loop-free programs;generalized just-in-time trace compilation using a parallel task farm in a dynamic binary translator;brainy: effective selection of data structures;an SSA-based algorithm for optimal speculative code motion under an execution profile;caisson: a hardware description language for secure information flow;steno: automatic optimization of declarative queries;languages as libraries;automatic CPU-GPU communication management and optimization;automatic compilation of MATLAB programs for synergistic execution on heterogeneous processors;partial-coherence abstractions for relaxed memory models;and probabilistic, modular and scalable inference of typestate specifications.

关键词： Optimal systems

来源：评论

学校读者我要写书评

暂无评论

Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic 11

Mostly-Automated Verification of Low-Level Programs in Compu...

引用

32nd acm sigplan conference on programming language design and implementation (PLDI 11)

作者： Chlipala, Adam Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781450306638

Several recent projects have shown the feasibility of verifying low-level systems software. Verifications based on automated theorem-proving have omitted reasoning about first-class code pointers, which is critical for tasks like certifying implementations of threads and processes. Conversely, verifications that deal with first-class code pointers have featured long, complex, manual proofs. In this paper, we introduce the Bedrock framework, which supports mostly-automated proofs about programs with the full range of features needed to implement, e.g., language runtime systems. The heart of our approach is in mostly-automated discharge of verification conditions inspired by separation logic. Our take on separation logic is computational, in the sense that function specifications are usually written in terms of reference implementations in a purely functional language. Logical quantifiers are the most challenging feature for most automated verifiers;by relying on functional programs (written in the expressive language of the Coq proof assistant), we are able to avoid quantifiers almost entirely. This leads to some dramatic improvements compared to both past work in classical verification, which we compare against with implementations of data structures like binary search trees and hash tables;and past work in verified programming with code pointers, which we compare against with examples like function memoization and a cooperative threading library.

关键词： interactive proof assistants separation logic low-level programming languages functional programming

来源：评论

学校读者我要写书评

暂无评论

Commutative Set: A language Extension for Implicit Parallel programming 11

Commutative Set: A Language Extension for Implicit Parallel ...

引用

32nd acm sigplan conference on programming language design and implementation (PLDI 11)

作者： Prabhu, Prakash Ghosh, Soumyadeep Zhang, Yun Johnson, Nick P. August, David I. Princeton Univ Princeton NJ 08544 USA

ISBN: (纸本)9781450306638

Sequential programming models express a total program order, of which a partial order must be respected. This inhibits parallelizing tools from extracting scalable performance. Programmer written semantic commutativity assertions provide a natural way of relaxing this partial order, thereby exposing parallelism implicitly in a program. Existing implicit parallel programming models based on semantic commutativity either require additional programming extensions, or have limited expressiveness. This paper presents a generalized semantic commutativity based programming extension, called Commutative Set (COMMSET), and associated compiler technology that enables multiple forms of parallelism. COMMSET expressions are syntactically succinct and enable the programmer to specify commutativity relations between groups of arbitrary structured code blocks. Using only this construct, serializing constraints that inhibit parallelization can be relaxed, independent of any particular parallelization strategy or concurrency control mechanism. COMMSET enables well performing parallelizations in cases where they were inapplicable or non-performing before. By extending eight sequential programs with only 8 annotations per program on average, Comm S ET and the associated compiler technology produced a geomean speedup of 5.7x on eight cores compared to 1.5x for the best non-COMMSET parallelization.

关键词： Implicit parallelism semantic commutativity programming model automatic parallelization static analysis

来源：评论

学校读者我要写书评

暂无评论

Caisson: A Hardware Description language for Secure Information Flow 11

Caisson: A Hardware Description Language for Secure Informat...

引用

32nd acm sigplan conference on programming language design and implementation (PLDI 11)

作者： Li, Xun Tiwari, Mohit Oberg, Jason K. Kashyap, Vineeth Chong, Frederic T. Sherwood, Timothy Hardekopf, Ben Univ Calif Santa Barbara Dept Comp Sci Santa Barbara CA 93106 USA

ISBN: (纸本)9781450306638

Information flow is an important security property that must be incorporated from the ground up, including at hardware design time, to provide a formal basis for a system's root of trust. We incorporate insights and techniques from designing information-flow secure programming languages to provide a new perspective on designing secure hardware. We describe a new hardware description language, Caisson, that combines domain-specific abstractions common to hardware design with insights from type-based techniques used in secure programming languages. The proper combination of these elements allows for an expressive, provably-secure HDL that operates at a familiar level of abstraction to the target audience of the language, hardware architects. We have implemented a compiler for Caisson that translates designs into Verilog and then synthesizes the designs using existing tools. As an example of Caisson's usefulness we have addressed an open problem in secure hardware by creating the first-ever provably information-flow secure processor with micro-architectural features including pipelining and cache. We synthesize the secure processor and empirically compare it in terms of chip area, power consumption, and clock frequency with both a standard (insecure) commercial processor and also a processor augmented at the gate level to dynamically track information flow. Our processor is competitive with the insecure processor and significantly better than dynamic tracking.

关键词： Hardware Description language Non-interference State Machine

来源：评论

学校读者我要写书评

暂无评论

Spreadsheet Table Transformations from Examples 11

Spreadsheet Table Transformations from Examples

引用

32nd acm sigplan conference on programming language design and implementation (PLDI 11)

作者： Harris, William R. Gulwani, Sumit Univ Wisconsin Dept Comp Sci Madison WI 53706 USA

ISBN: (纸本)9781450306638

Every day, millions of computer end-users need to perform tasks over large, tabular data, yet lack the programming knowledge to do such tasks automatically. In this work, we present an automatic technique that takes from a user an example of how the user needs to transform a table of data, and provides to the user a program that implements the transformation described by the example. In particular, we present a language of programs TableProg that can describe transformations that real users require. We then present an algorithm ProgFrornEx that takes an example input and output table, and infers a program in TableProg that implements the transformation described by the example. When the program is applied to the example input, it reproduces the example output. When the program is applied to another, potentially larger, table with a "similar" layout as the example input table, then the program produces a corresponding table with a layout that is similar to the example output table. A user can apply ProgFrornEx interactively, providing multiple small examples to obtain a program that implements the transformation that the user desires. Moreover, ProgFromEx can help identify "noisy" examples that contain errors. To evaluate the practicality of TableProg and ProgFromEx, we implemented ProgFromEx as a module for the Microsoft Excel spreadsheet program. We applied the module to automatically implement over 50 table transformations specified by end-users through examples on online Excel help forums. In seconds, ProgFromEx found programs that satisfied the examples and could be applied to larger input tables. This experience demonstrates that TableProg and ProgFromEx can significantly automate the tasks over tabular data that users need to perform.

关键词： Program Synthesis End-user programming programming by Example Spreadsheet programming Table Manipulation User Intent

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：