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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

9 篇 会议

馆藏范围

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

日期分布

学科分类号

9 篇 工学
- 9 篇 计算机科学与技术...
- 9 篇 软件工程
- 2 篇 电子科学与技术（可...
- 1 篇 材料科学与工程（可...
- 1 篇 电气工程
- 1 篇 信息与通信工程
- 1 篇 建筑学
- 1 篇 轻工技术与工程
- 1 篇 环境科学与工程（可...
- 1 篇 安全科学与工程
2 篇 理学
- 1 篇 数学
- 1 篇 物理学
1 篇 管理学
- 1 篇 管理科学与工程(可...

主题

1 篇 teaching
1 篇 model checking
1 篇 specifications
1 篇 application prog...
1 篇 industrial resea...
1 篇 c (programming l...
1 篇 computer softwar...
1 篇 computer program...
1 篇 distributed comp...

机构

1 篇 inria
1 篇 paul g. allen sc...
1 篇 university of wa...
1 篇 university colle...
1 篇 microsoft resear...
1 篇 plt and northeas...
1 篇 plt and universi...
1 篇 computer science...
1 篇 plt and northwes...
1 篇 plt and indiana ...
1 篇 cornell universi...
1 篇 microsoft resear...
1 篇 computer science...
1 篇 mit csail cambri...
1 篇 plt and google n...
1 篇 cognition group ...
1 篇 university of wa...
1 篇 microsoft resear...

作者

2 篇 tatlock zachary
1 篇 hriţcu cǎtǎlin
1 篇 zinzindohoué jea...
1 篇 flatt matthew
1 篇 lorch jay
1 篇 bhargavan karthi...
1 篇 maillard kenji
1 篇 grossman dan
1 篇 swamy nikhil
1 篇 singh rishabh
1 篇 pang jianyang
1 篇 protzenko jonath...
1 篇 greenman ben
1 篇 wilcox james r.
1 篇 sampson adrian
1 篇 kuraj ivan
1 篇 rane ashay
1 篇 delignat-lavaud ...
1 篇 strickland t. st...
1 篇 tobin-hochstadt ...

语言

9 篇 英文

检索条件"任意字段=2nd Summit on Advances in Programming Languages, SNAPL 2017"

共 9 条记录，以下是1-10 订阅

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

详细简洁

排序：

Let's fix openGL 2

Let's fix openGL

引用

2nd summit on advances in programming languages, snapl 2017

作者： Sampson, Adrian Cornell University IthacaNY United States

ISBN: (纸本)9783959770323

From windowing systems to virtual reality, real-time graphics code is ubiquitous. programming models for constructing graphics software, however, have largely escaped the attention of programming languages researchers. This essay introduces the programming model of OpenGL, a ubiquitous API for real-time graphics applications, for a language-oriented audience. It highlights six broad problems with the programming model and connects them to traditions in PL research. The issues range from classic pitfalls, where established thinking can apply, to new open problems, where novel research is needed. © Adrian Sampson;licensed under Creative Commons License CC-BY.

关键词： Application programming interfaces (API)

来源：评论

学校读者我要写书评

暂无评论

Teaching programming languages by experimental and adversarial thinking 2

Teaching programming languages by experimental and adversari...

引用

2nd summit on advances in programming languages, snapl 2017

作者： Pombrio, Justin Krishnamurthi, Shriram Fisler, Kathi Computer Science Brown University ProvidenceRI United States Computer Science WPI WorcesterMA United States

ISBN: (纸本)9783959770323

We present a new approach to teaching programming language courses. Its essence is to view programming language learning as a natural science activity, where students probe languages experimentally to understand both the normal and extreme behaviors of their features. This has natural parallels to the "security mindset" of computer security, with languages taking the place of servers and other systems. The approach is modular (with minimal dependencies), incremental (it can be introduced slowly into existing classes), interoperable (it does not need to push out other, existing methods), and complementary (since it introduces a new mode of thinking). © Justin Pombrio, Shriram Krishnamurthi, and Kathi Fisler;licensed under Creative Commons License CC-BY.

关键词： Teaching

来源：评论

学校读者我要写书评

暂无评论

Leveraging sequential computation for programming efficient and reliable distributed systems 2

Leveraging sequential computation for programming efficient ...

引用

2nd summit on advances in programming languages, snapl 2017

作者： Kuraj, Ivan Solar-Lezama, Armando MIT CSAIL CambridgeMA United States

ISBN: (纸本)9783959770323

While sequential programs represent a simple and natural form for expressing functionality, corresponding distributed implementations get considerably more complex. We examine the possibility of using the sequential computation model for programming distributed systems and requirements for making that possible. The benefits of such an approach include easier specification and reasoning about behaviors in the system, as well as a possibility to directly reuse existing techniques for checking correctness and optimization of sequential programs to produce efficient and reliable distributed implementations. © Ivan Kuraj and Armando Solar-Lezama;licensed under Creative Commons License CC-BY.

关键词： Computer software reusability

来源：评论

学校读者我要写书评

暂无评论

programming language tools and techniques for 3D printing 2

Programming language tools and techniques for 3D printing

引用

2nd summit on advances in programming languages, snapl 2017

作者： Nandi, Chandrakana Caspi, Anat Grossman, Dan Tatlock, Zachary Paul G. Allen School of Computer Science and Engineering University of Washington SeattleWA United States

ISBN: (纸本)9783959770323

We propose a research agenda to investigate programming language techniques for improving affordable, end-user desktop manufacturing processes such as 3D printing. Our goal is to adapt programming languages tools and extend the decades of research in industrial, high-end CAD/CAM in order to help make affordable desktop manufacturing processes more accurate, fast, reliable, and accessible to end-users. We focus on three major areas where 3D printing can benefit from programming language tools: design synthesis, optimizing compilation, and runtime monitoring. We present preliminary results on synthesizing editable CAD models from difficult-to-edit surface meshes, discuss potential new compilation strategies, and propose runtime monitoring techniques. We conclude by discussing additional near-future directions we intend to pursue. © Chandrakana Nandi, Anat Caspi, Dan Grossman, and Zachary Tatlock;licensed under Creative Commons License CC-BY.

关键词： Industrial research

来源：评论

学校读者我要写书评

暂无评论

Natural language is a programming language: Applying natural language processing to software development 2

Natural language is a programming language: Applying natural...

引用

2nd summit on advances in programming languages, snapl 2017

作者： Ernst, Michael D. University of Washington Computer Science and Engineering SeattleWA United States

ISBN: (纸本)9783959770323

A powerful, but limited, way to view software is as source code alone. Treating a program as a sequence of instructions enables it to be formalized and makes it amenable to mathematical techniques such as abstract interpretation and model checking. A program consists of much more than a sequence of instructions. Developers make use of test cases, documentation, variable names, program structure, the version control repository, and more. I argue that it is time to take the blinders off of software analysis tools: tools should use all these artifacts to deduce more powerful and useful information about the program. Researchers are beginning to make progress towards this vision. This paper gives, as examples, four results that find bugs and generate code by applying natural language processing techniques to software artifacts. The four techniques use as input error messages, variable names, procedure documentation, and user questions. They use four different NLP techniques: document similarity, word semantics, parse trees, and neural networks. The initial results suggest that this is a promising avenue for future work. © Michael D. Ernst;licensed under Creative Commons License CC-BY.

关键词： Model checking

来源：评论

学校读者我要写书评

暂无评论

Migratory typing: Ten years later 2

Migratory typing: Ten years later

引用

2nd summit on advances in programming languages, snapl 2017

作者： Tobin-Hochstadt, Sam Felleisen, Matthias Findler, Robert Bruce Flatt, Matthew Greenman, Ben Kent, Andrew M. St-Amour, Vincent Strickland, T. Stephen Takikawa, Asumu PLT and Indiana University BloomingtonIN United States PLT and Northeastern University BostonMA United States PLT and Northwestern University EvanstonIL United States PLT and University of Utah Salt Lake CityUT United States PLT and Google New York New York CityNY United States

ISBN: (纸本)9783959770323

In this day and age, many developers work on large, untyped code repositories. Even if they are the creators of the code, they notice that they have to figure out the equivalent of method signatures every time they work on old code. This step is time consuming and error prone. Ten years ago, the two lead authors outlined a linguistic solution to this problem. Specifically they proposed the creation of typed twins for untyped programming languages so that developers could migrate scripts from the untyped world to a typed one in an incremental manner. Their programmatic paper also spelled out three guiding design principles concerning the acceptance of grown idioms, the soundness of mixed-typed programs, and the units of migration. This paper revisits this idea of a migratory type system as implemented for Racket. It explains how the design principles have been used to produce the Typed Racket twin and presents an assessment of the project's status, highlighting successes and failures. © Sam Tobin-Hochstadt, Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Ben Greenman, Andrew M. Kent, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa;licensed under Creative Commons License CC-BY.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

programming language abstractions for modularly verified distributed systems 2

Programming language abstractions for modularly verified dis...

引用

2nd summit on advances in programming languages, snapl 2017

作者： Wilcox, James R. Sergey, Ilya Tatlock, Zachary University of Washington SeattleWA United States University College London London United Kingdom

ISBN: (纸本)9783959770323

Distributed systems are rarely developed as monolithic programs. Instead, like any software, these systems may consist of multiple program components, which are then compiled separately and linked together. Modern systems also incorporate various services interacting with each other and with client applications. However, state-of-the-art verification tools focus predominantly on verifying standalone, closed-world protocols or systems, thus failing to account for the compositional nature of distributed systems. For example, standalone verification has the drawback that when protocols and their optimized implementations evolve, one must re-verify the entire system from scratch, instead of leveraging compositionality to contain the reverification effort. In this paper, we focus on the challenge of modular verification of distributed systems with respect to high-level protocol invariants as well as for low-level implementation safety properties. We argue that the missing link between the two is a programming paradigm that would allow one to reason about both high-level distributed protocols and low-level implementation primitives in a single verification-friendly framework. Such a link would make it possible to reap the benefits from both the vast body of research in distributed computing, focused on modular protocol decomposition and consistency properties, as well as from the recent advances in program verification, enabling construction of provably correct systems implementations. To showcase the modular verification challenges, we present some typical scenarios of decomposition between a distributed protocol and its implementations. We then describe our ongoing research agenda, in which we are attempting to address the outlined problems by providing a typing discipline and a set of domain-specific primitives for specifying, implementing and verifying distributed systems. Our approach, mechanized within a proof assistant, provides the means of decomposition necessary

关键词： Distributed computer systems

来源：评论

学校读者我要写书评

暂无评论

AP: Artificial programming 2

AP: Artificial programming

引用

2nd summit on advances in programming languages, snapl 2017

作者： Singh, Rishabh Kohli, Pushmeet Cognition Group Microsoft Research RedmondWA United States

ISBN: (纸本)9783959770323

The ability to automatically discover a program consistent with a given user intent (specification) is the holy grail of Computer Science. While significant progress has been made on the socalled problem of Program Synthesis, a number of challenges remain;particularly for the case of synthesizing richer and larger programs. This is in large part due to the difficulty of search over the space of programs. In this paper, we argue that the above-mentioned challenge can be tackled by learning synthesizers automatically from a large amount of training data. We present a first step in this direction by describing our novel synthesis approach based on two neural architectures for tackling the two key challenges of Learning to understand partial input-output specifications and Learning to search programs. The first neural architecture called the Spec Encoder computes a continuous representation of the specification, whereas the second neural architecture called the Program Generator incrementally constructs programs in a hypothesis space that is conditioned by the specification vector. The key idea of the approach is to train these architectures using a large set of (θ, P) pairs, where P denotes a program sampled from the DSL L and (θ denotes the corresponding specification satisfied by P. We demonstrate the effectiveness of our approach on two preliminary instantiations. The first instantiation, called Neural FlashFill [29], corresponds to the domain of string manipulation programs similar to that of FlashFill [13, 14]. The second domain considers string transformation programs consisting of composition of API functions. We show that a neural system is able to perform quite well in learning a large majority of programs from few input-output examples. We believe this new approach will not only dramatically expand the applicability and effectiveness of Program Synthesis, but also would lead to the coming together of the Program Synthesis and Machine Learning research discipl

关键词： Specifications

来源：评论

学校读者我要写书评

暂无评论

Everest: Towards a verified, drop-in replacement of HTTPS 2

Everest: Towards a verified, drop-in replacement of HTTPS

引用

2nd summit on advances in programming languages, snapl 2017

作者： Bhargavan, Karthikeyan Bond, Barry Delignat-Lavaud, Antoine Fournet, Cédric Hawblitzel, Chris Hriţcu, Cǎtǎlin Ishtiaq, Samin Kohlweiss, Markulf Leino, Rustan Lorch, Jay Maillard, Kenji Pang, Jianyang Parno, Bryan Protzenko, Jonathan Ramananandro, Tahina Rane, Ashay Rastogi, Aseem Swamy, Nikhil Thompson, Laure Wang, Peng Zanella-Béguelin, Santiago Zinzindohoué, Jean-Karim Inria Paris France Microsoft Research RedmondWA United States Microsoft Research Cambridge United Kingdom Microsoft Research Bangalore India

ISBN: (纸本)9783959770323

The HTTPS ecosystem is the foundation on which Internet security is built. At the heart of this ecosystem is the Transport Layer Security (TLS) protocol, which in turn uses the X.509 publickey infrastructure and numerous cryptographic constructions and algorithms. Unfortunately, this ecosystem is extremely brittle, with headline-grabbing attacks and emergency patches many times a year. We describe our ongoing efforts in Everest1 a project that aims to build and deploy a verified version of TLS and other components of HTTPS, replacing the current infrastructure with proven, secure software. Aiming both at full verification and usability, we conduct high-level code-based, game-playing proofs of security on cryptographic implementations that yield efficient, deployable code, at the level of C and assembly. Concretely, we use F∗ a dependently typed language for programming, meta-programming, and proving at a high level, while relying on low-level DSLs embedded within F∗ for programming low-level components when necessary for performance and, sometimes, sidechannel resistance. To compose the pieces, we compile all our code to source-like C and assembly, suitable for deployment and integration with existing code bases, as well as audit by independent security experts. Our main results so far include (1) the design of Low∗, a subset of F∗ designed for C-like imperative programming but with high-level verification support, and KreMLin, a compiler that extracts Low∗ programs to C;(2) an implementation of the TLS-1.3 record layer in Low∗, together with a proof of its concrete cryptographic security;(3) Vale, a new DSL for verified assembly language, and several optimized cryptographic primitives proven functionally correct and side-channel resistant. In an early deployment, all our verified software is integrated and deployed within libcurl, a widely used library of networking protocols. © Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawbl

关键词： C (programming language)

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

共1页 << < 1 > >>

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：