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

您好，读者！请登录

内蒙古大学图书馆

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

咨询与建议

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

您的常用邮箱：*

您的手机号码：*

问题描述：

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

分类表

所选分类

>> <<

限定检索结果

文献类型

566 篇 会议
56 篇 期刊文献
6 册 图书

馆藏范围

622 篇 电子文献
6 种 纸本馆藏

日期分布

学科分类号

567 篇 工学
- 550 篇 软件工程
- 520 篇 计算机科学与技术...
- 51 篇 控制科学与工程
- 18 篇 信息与通信工程
- 13 篇 材料科学与工程（可...
- 5 篇 电子科学与技术（可...
- 1 篇 机械工程
- 1 篇 光学工程
- 1 篇 电气工程
- 1 篇 建筑学
- 1 篇 土木工程
- 1 篇 化学工程与技术
192 篇 理学
- 187 篇 数学
- 7 篇 统计学（可授理学、...
- 3 篇 系统科学
- 2 篇 物理学
- 1 篇 化学
- 1 篇 生物学
69 篇 管理学
- 45 篇 管理科学与工程(可...
- 28 篇 图书情报与档案管...
- 8 篇 工商管理
4 篇 法学
- 2 篇 法学
- 2 篇 社会学
1 篇 教育学
- 1 篇 教育学
1 篇 农学

主题

235 篇 computer program...
82 篇 computer program...
39 篇 languages
26 篇 object oriented ...
20 篇 programming theo...
20 篇 high level langu...
18 篇 logic programmin...
18 篇 theory
16 篇 computer systems...
13 篇 semantics
11 篇 functional progr...
10 篇 verification
9 篇 parallel program...
8 篇 java programming...
7 篇 design
5 篇 performance
5 篇 algorithms
5 篇 static analysis
5 篇 security
4 篇 reliability

机构

14 篇 carnegie mellon ...
6 篇 inria rocquencou...
6 篇 cornell univ ith...
5 篇 univ of glasgow ...
4 篇 univ of tokyo
4 篇 ibm t.j. watson ...
4 篇 indiana univ blo...
4 篇 rice univ housto...
4 篇 ecole normale su...
4 篇 carnegie mellon ...
4 篇 microsoft resear...
3 篇 north carolina s...
3 篇 univ of edinburg...
3 篇 princeton univ p...
3 篇 bell laboratorie...
3 篇 sri int menlo pa...
3 篇 inria rocquencou...
3 篇 stanford univ st...
3 篇 univ of copenhag...
3 篇 univ of aarhus a...

作者

14 篇 anon
9 篇 leroy xavier
9 篇 cardelli luca
9 篇 harper robert
8 篇 wadler philip
8 篇 felleisen matthi...
8 篇 jones simon peyt...
7 篇 halpern joseph y...
7 篇 mitchell john c.
7 篇 morrisett greg
7 篇 walker david
7 篇 abadi martin
6 篇 wand mitchell
6 篇 acm symposium on...
6 篇 riecke jon g.
6 篇 pierce benjamin ...
6 篇 odersky martin
5 篇 meyer albert r.
5 篇 friedman daniel ...
5 篇 hudak paul

语言

603 篇 英文
23 篇 其他
2 篇 中文

检索条件"任意字段=Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages"

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

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

详细简洁

排序：

CPP 2024 - Proceedings of the 13th acm SIGPLAN International conference on Certified Programs and Proofs, Co-located with: POPL 2024

CPP 2024 - Proceedings of the 13th ACM SIGPLAN International...

引用

13th acm SIGPLAN International conference on Certified Programs and Proofs, CPP 2024, in affiliation with the annual symposium on principles of programming, languages, ,POPL 2024

ISBN: (纸本)9798400704888

The proceedings contain 20 papers. The topics discussed include: UTC time, formally verified;VCFloat2: floating-point error analysis in coq;the last yard: foundational end-to-end verification of high-speed cryptography;rooting for efficiency: mechanized reasoning about array-based trees in separation logic;compositional verification of concurrent C programs with search structure templates;unification for subformula linking under quantifiers;PfComp: a verified compiler for packet filtering leveraging binary decision diagrams;memory simulations, security and optimization in a verified compiler;lean formalization of extended regular expression matching with lookarounds;certification of confluence- and commutation-proofs via parallel critical pairs;a temporal differential dynamic logic formal embedding;and strictly monotone Brouwer trees for well-founded recursion over multiple arguments.

关键词：

来源：评论

学校读者我要写书评

暂无评论

conference record of the annual acm symposium on principles of programming languages

Conference Record of the Annual ACM Symposium on Principles ...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

ISBN: (纸本)9781450346603

The proceedings contain 63 papers. The topics discussed include: a posteriori environment analysis with pushdown Delta CFA;semantic-directed clumping of disjunctive abstract states;polymorphism, subtyping, and type inference in MLsub;Java generics are Turing complete;stochastic invariants for probabilistic termination;coupling proofs are probabilistic product programs;a promising semantics for relaxed-memory concurrency;automatically comparing memory consistency models;interactive proofs in higher-order concurrent separation logic;monadic second-order logic on finite sequences;on the relationship between higher-order recursion schemes and higher-order fix-point logic;coming to terms with quantified reasoning;a program optimization for automatic database result caching;contract-based resource verification for higher-order functions with memoization;context-sensitive data-dependence analysis via linear conjunctive language reachability;towards automatic resource bound analysis for OCaml;the exp-log normal form of types: decomposing extensional equality and representing terms compactly;serializability for eventual consistency: criterion, analysis, and applications;thread modularity at many levels: a pearl in compositional verification;and Cantor meets Scott: semantic foundations for probabilistic networks.

关键词：

来源：评论

学校读者我要写书评

暂无评论

conference record of the annual acm symposium on principles of programming languages

Conference Record of the Annual ACM Symposium on Principles ...

引用

43rd annual acm SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2016

ISBN: (纸本)9781450335492

The proceedings contain 61 papers. The topics discussed include: programming the world of uncertain things;type theory in type theory using quotient inductive types;system F-omega with equirecursive types for datatype-generic programming;a theory of effects and resources: adjunction models and polarized calculi;temporal verification of higher-order functional programs;scaling network verification using symmetry and surgery;model checking for symbolic-heap separation logic with inductive predicates;reducing crash recoverability to reachability;query-guided maximum satisfiability;string solving with word equations and transducers: towards a logic for analyzing mutation XSS;symbolic computation of differential equivalences;and unboundedness and downward closures of higher-order pushdown automata.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Learning nominal automata 17

Learning nominal automata

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Moerman, Joshua Sammartino, Matteo Silva, Alexandra Klin, Bartek Szynwelski, Michal Radboud University Netherlands University College London United Kingdom University of Warsaw Poland

ISBN: (纸本)9781450346603

We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting. In particular we can learn a subclass of nominal non-deterministic automata. An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments. © 2017 acm.

关键词： Functional programming

来源：评论

学校读者我要写书评

暂无评论

Ogre and pythia: An invariance proof method for weak consistency models 17

Ogre and pythia: An invariance proof method for weak consist...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Alglave, Jade Cousot, Patrick University College London Microsoft Research Cambridge United Kingdom New York University United States Emer. École Normale Supérieure PSL France

ISBN: (纸本)9781450346603

We design an invariance proof method for concurrent programs parameterised by a weak consistency model. The calculational design of the invariance proof method is by abstract interpretation of a truly parallel analytic semantics. This generalises the methods by Lamport and Owicki-Gries for sequential consistency. We use cat as an example of language to write consistency specifications of both concurrent programs and machine architectures. © 2017 acm.

关键词： Parallel programming

来源：评论

学校读者我要写书评

暂无评论

Automatically generating the dynamic semantics of gradually typed languages 17

Automatically generating the dynamic semantics of gradually ...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Cimini, Matteo Siek, Jeremy G. Indiana University United States

ISBN: (纸本)9781450346603

Many language designers have adopted gradual typing. However, there remains open questions regarding how to gradualize languages. Cimini and Siek (2016) created a methodology and algorithm to automatically generate the type system of a gradually typed language from a fully static version of the language. In this paper, we address the next challenge of how to automatically generate the dynamic semantics of gradually typed languages. Such languages typically use an intermediate language with explicit casts. Our first result is a methodology for generating the syntax, type system, and dynamic semantics of the intermediate language with casts. Next, we present an algorithm that formalizes and automates the methodology, given a language definition as input. We show that our approach is general enough to automatically gradualize several languages, including features such as polymorphism, recursive types and exceptions. We prove that our algorithm produces languages that satisfy the key correctness criteria of gradual typing. Finally, we implement the algorithm, generating complete specifications of gradually typed languages in lambda-Prolog, including executable interpreters. © 2017 acm.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

LMS-Verify: Abstraction without regret for verified systems programming 17

LMS-Verify: Abstraction without regret for verified systems ...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Amin, Nada Rompf, Tiark EPFL Switzerland Purdue University United States

ISBN: (纸本)9781450346603

Performance critical software is almost always developed in C, as programmers do not trust high-level languages to deliver the same reliable performance. This is bad because low-level code in unsafe languages attracts security vulnerabilities and because development is far less productive, with PL advances mostly lost on programmers operating under tight performance constraints. Highlevel languages provide memory safety out of the box, but they are deemed too slow and unpredictable for serious system software. Recent years have seen a surge in staging and generative programming: the key idea is to use high-level languages and their abstraction power as glorified macro systems to compose code fragments in first-order, potentially domain-specific, intermediate languages, from which fast C can be emitted. But what about security? Since the end result is still C code, the safety guarantees of the high-level host language are lost. In this paper, we extend this generative approach to emit ACSL specifications along with C code. We demonstrate that staging achieves "abstraction without regret" for verification: we show how high-level programming models, in particular higher-order composable contracts from dynamic languages, can be used at generation time to compose and generate first-order specifications that can be statically checked by existing tools. We also show how type classes can automatically attach invariants to data types, reducing the need for repetitive manual annotations. We evaluate our system on several case studies that varyingly exercise verification of memory safety, overflow safety, and functional correctness. We feature an HTTP parser that is (1) fast (2) high-level: implemented using staged parser combinators (3) secure: with verified memory safety. This result is significant, as input parsing is a key attack vector, and vulnerabilities related to HTTP parsing have been documented in all widely-used web servers. © 2017 acm.

关键词： HTTP

来源：评论

学校读者我要写书评

暂无评论

Fencing off Go: Liveness and safety for channel-based programming 17

Fencing off Go: Liveness and safety for channel-based progra...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Lange, Julien Ng, Nicholas Toninho, Bernardo Yoshida, Nobuko Imperial College London United Kingdom

ISBN: (纸本)9781450346603

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mismatches or partial deadlocks. This work develops a static verification framework for liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation, unbounded thread creation and recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural type. By checking a syntactic restriction on channel usage, dubbed fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many times. This restriction allows us to implement a decision procedure for liveness and safety in types which in turn statically ensures liveness and safety in Go programs. We have implemented a type inference and decision procedures in a tool-chain and tested it against publicly available Go programs. © 2017 acm.

关键词： Message passing

来源：评论

学校读者我要写书评

暂无评论

Contract-based resource verification for higher-order functions with memoization 17

Contract-based resource verification for higher-order functi...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Madhavan, Ravichandhran Kulal, Sumith Kuncak, Viktor EPFL Switzerland IIT Bombay India

ISBN: (纸本)9781450346603

We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. as steps ≤ ?∗size(l) + ? in the contracts of functions. They can also express invariants necessary for establishing the bounds that may depend on the state of memoization. Our approach operates in two phases: first generating an instrumented first-order program that accurately models the higher-order control flow and the effects of memoization on resources using sets, algebraic datatypes and mutual recursion, and then verifying the contracts of the first-order program by producing verification conditions of the form 'using an extended assume/guarantee reasoning. We use our approach to verify precise bounds on resources such as evaluation steps and number of heap-allocated objects on 17 challenging data structures and algorithms. Our benchmarks, comprising of 5K lines of functional Scala code, include lazy mergesort, Okasaki'fs real-time queue and deque data structures that rely on aliasing of references to first-class functions;lazy data structures based on numerical representations such as the conqueue data structure of Scala-fs dataparallel library, cyclic streams, as well as dynamic programming algorithms such as knapsack and Viterbi. Our evaluations show that when averaged over all benchmarks the actual runtime resource consumption is 80% of the value inferred by our tool when estimating the number of evaluation steps, and is 88% for the number of heap-allocated objects. © 2017 acm.

关键词： Dynamic programming

来源：评论

学校读者我要写书评

暂无评论

Context-sensitive data-dependence analysis via linear conjunctive language reachability 17

Context-sensitive data-dependence analysis via linear conjun...

引用

44th acm SIGPLAN symposium on principles of programming languages, POPL 2017

作者： Zhang, Qirun Su, Zhendong University of California Davis United States

ISBN: (纸本)9781450346603

Many program analysis problems can be formulated as graph reachability problems. In the literature, context-free language (CFL) reachability has been the most popular formulation and can be computed in subcubic time. The context-sensitive data-dependence analysis is a fundamental abstraction that can express a broad range of program analysis problems. It essentially describes an interleaved matched-parenthesis language reachability problem. The language is not context-free, and the problem is well-known to be undecidable. In practice, many program analyses adopt CFL-reachability to exactly model the matched parentheses for either context-sensitivity or structure-transmitted data-dependence, but not both. Thus, the CFL-reachability formulation for context-sensitive data-dependence analysis is inherently an approximation. To support more precise and scalable analyses, this paper introduces linear conjunctive language (LCL) reachability, a new, expressive class of graph reachability. LCL not only contains the interleaved matched-parenthesis language, but is also closed under all set-theoretic operations. Given a graph with n nodes and m edges, we propose an O(mn) time approximation algorithm for solving all-pairs LCL-reachability, which is asymptotically better than known CFL-reachability algorithms. Our formulation and algorithm offer a new perspective on attacking the aforementioned undecidable problem-the LCL-reachability formulation is exact, while the LCL-reachability algorithm yields a sound approximation. We have applied the LCL-reachability framework to two existing client analyses. The experimental results show that the LCL-reachability framework is both more precise and scalable than the traditional CFL-reachability framework. This paper opens up the opportunity to exploit LCL-reachability in program analysis. © 2017 acm.

关键词： Context free languages

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

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

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

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

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

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

联系人：

所在院系：

联系邮箱：

联系电话：

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

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：