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

Computer Security foundations workshop

作者： Daniel Schoepe Toby Murray Andrei Sabelfeld Chalmers University of Technology University of Melbourne and Data61

ISBN: (数字)9781728165721

ISBN: (纸本)9781728165738

Methods for proving that concurrent software does not leak its secrets has remained an active topic of research for at least the past four decades. Despite an impressive array of work, the present situation remains highly unsatisfactory. With contemporary compositional proof methods one is forced to choose between expressiveness (the ability to reason about a wide variety of security policies), on the one hand, and precision (the ability to reason about complex thread interactions and program behaviours), on the other. Achieving both is essential and, we argue, requires a new style of compositional reasoning. We present VERONICA, the first program logic for proving concurrent programs information flow secure that supports compositional, high-precision reasoning about a wide range of security policies and program behaviours (e.g. expressive declassification, value-dependent classification, secret-dependent branching). Just as importantly, VERONICA embodies a new approach for engineering such logics that can be re-used elsewhere, called decoupled functional correctness (DFC). DFC leads to a simple and clean logic, even while achieving this unprecedented combination of features. We demonstrate the virtues and versatility of VERONICA by verifying a range of example programs, beyond the reach of prior methods.

关键词： Security Cognition Concurrent computing programming Sensitivity Instruction sets

来源：评论

学校读者我要写书评

暂无评论

LFMTP 2014 - Proceedings of the 9th International workshop on logical Frameworks and Meta-Languages: Theory and Practice, Held as Part of: Vienna Summer of logic, FLoC 2014, CSL-LICS 2014, IJCAR 2014

LFMTP 2014 - Proceedings of the 9th International Workshop o...

引用

9th International workshop on logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2014

ISBN: (纸本)9781450328173

The proceedings contain 6 papers. The topics discussed include: session types meet separation logic;Idris: implementing a dependently typed programming language;a framework for the verified transformation of functional programs;some constructions on Ω-groupoids;a generic approach to proofs about substitution;hybrid extensions in a logical framework;proof-theoretic foundations of indexing in logic programming;internal adequacy of bookkeeping in Coq;and automatically deriving schematic theorems for dynamic contexts.

关键词：

来源：评论

学校读者我要写书评

暂无评论

What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common

What Sequential Games, the Tychonoff Theorem and the Double-...

引用

3rd workshop on Mathematically Structured functional programming

作者： Escardo, Martin Oliva, Paulo Univ Birmingham Birmingham B15 2TT W Midlands England

ISBN: (纸本)9781450302555

This is a tutorial for mathematically inclined functional programmers, based on previously published, peered reviewed theoretical work. We discuss a higher-type functional, written here in the functional programming language Haskell, which (1) optimally plays sequential games, (2) implements a computational version of the Tychonoff Theorem from topology, and (3) realizes the Double-Negation Shift from logic and proof theory. The functional makes sense for finite and infinite (lazy) lists, and in the binary case it amounts to an operation that is available in any (strong) monad. In fact, once we define this monad in Haskell, it turns out that this amazingly versatile functional is already available in Haskell, in the standard prelude, called sequence, which iterates this binary operation. Therefore Haskell proves that this functional is even more versatile than anticipated, as the function sequence was introduced for other purposes by the language designers, in particular the iteration of a list of monadic effects (but effects are not what we discuss here).

关键词： functional programming Haskell monad search game theory optimal strategy exhaustible set axiom of choice infinite data dependent type Agda topology logic foundations

来源：评论

学校读者我要写书评

暂无评论

Refinement Types for Secure Implementations

Refinement Types for Secure Implementations

引用

Computer Security foundations workshop

作者： Jesper Bengtson Karthikeyan Bhargavan Cédric Fournet Andrew D. Gordon Sergio Maffeis University of Uppsala Sweden Microsoft Research Limited USA University of California Santa Cruz USA

We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a λ-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.

关键词： Cryptography Authorization Cryptographic protocols Authentication Computer security Surface-mount technology Libraries logic programming Educational institutions Mechanical factors

来源：评论

学校读者我要写书评

暂无评论

Evaluation strategies for functional logic programming

引用

JOURNAL OF SYMBOLIC COMPUTATION 2005年第1期40卷 875-903页

作者： Antoy, S Portland State Univ Dept Comp Sci Portland OR 97207 USA

Recent advances in the foundations and the implementations of functional logic programming languages originate from far-reaching results on narrowing evaluation strategies. Narrowing is a computation similar to rewriting which yields substitutions in addition to normal forms. In functional logic programming, the classes of rewrite systems to which narrowing is applied are, for the most part, subclasses of the constructor-based, possibly conditional, rewrite systems. Many interesting narrowing strategies, particularly for the smallest subclasses of the constructor-based rewrite systems, are generalizations of well-known rewrite strategies. However, some strategies for larger non-confluent subclasses have been developed just for functional logic computations. This paper discusses the elements that play a relevant role in evaluation strategies for functional logic computations, describes some important classes of rewrite systems that model functional logic programs, shows examples of the differences in expressiveness provided by these classes, and reviews the characteristics of narrowing strategies proposed for each class of rewrite systems. (c) 2005 Elsevier Ltd. All rights reserved.

关键词： evaluation strategies narrowing definitional trees constructor-based rewrite systems functional logic programming

来源：评论

学校读者我要写书评

暂无评论

Theoretical foundations of value withdrawal explanations for domain reduction

Theoretical foundations of value withdrawal explanations for...

引用

WFLP 2002, 11th International workshop on functional and (Constraint) logic programming, Selected Papers

作者： Ferrand, G. Lesaint, W. Tessier, A. Laboratoire d'Informatique Fondamentale d'Orléans rue Léonard de Vinci F-45067 Orléans Cedex 2 France

Solvers on finite domains use local consistency notions to remove values from the domains. This paper defines value withdrawal explanations. Domain reduction is formalized with chaotic iterations of monotonic operators. With each operator is associated its dual which will be described by a set of rules. For classical consistency notions, there exists such a natural system of rules. The rules express value removals as consequences of other value removals. The linking of these rules inductively defines proof trees. Such a proof tree clearly explains the removal of a value (which is the root of the tree). Explanations can be considered as the essence of domain reduction. © 2002 Published by Elsevier Science B.V.

关键词： Constraint theory

来源：评论

学校读者我要写书评

暂无评论

Evaluation strategies for functional logic programming

Evaluation strategies for functional logic programming

引用

WRS 2001, 1st International workshop on Reduction Strategies in Rewriting and programming

作者： Antoy, Sergio Computer Science Department Portland State University P.O. Box 751 Portland OR 97207 United States

Recent advances in the foundations and the development of functional logic programming languages originate from far-reaching results on narrowing evaluation strategies. Narrowing is a computation similar to rewriting which yields substitutions in addition to normal forms. In functional logic programming, the classes of rewrite systems to which narrowing is applied are, for the most part, subclasses of the constructor-based, possibly conditional, rewrite systems. Many interesting narrowing strategies, particularly for the smallest subclasses of the constructor-based rewrite systems, are generalizations of well-known rewrite strategies. However, some strategies for larger non-confluents subclasses have been developed just for functional logic computations. In this paper, I will discuss the elements that play a relevant role in evaluation strategies for functional logic programming, describe some important classes of rewrite systems that model functional logic programs, show examples of the differences in expressiveness provided by these classes, and review the characteristics of narrowing strategies proposed for each class of rewrite systems. © 2001 Published by Elsevier Science B. V.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Matching typed and untyped readability (Extended abstract)

Matching typed and untyped readability (Extended abstract)

引用

workshop on Domains IV

作者： Longley, John Laboratory for the Foundations of Computer Science JCMB The. King's Buildings May field Road Edinburgh EH9 3JZ United Kingdom

Realizability interpretations of logics are given by saying what it means for computational objects of some kind to realize, logical formulae. The computational objects in question might be drawn from an untyped universe of computation, such as a partial combinatory algebra, or they might be typed objects such as terms of a PCF-style programming language. In some instances, one can show that a particular untyped realizability interpretation matches a particular typed one, in the sense that they give the same set of realizable formulae. In this case, we have a very good fit indeed between the typed language and the untyped realizability model-we refer to this condition as (constructive) logical full abstraction., We give some examples of this situation for a variety of extensions of PCF. Of particular interest are some models that are logically fully abstract for typed languages including non-functional, features. Our results establish connections between what is computable in various programming languages, and what is true inside various realizability toposes. We consider some examples of logical formulae to illustrate these ideas, in particular their application to exact real-number computability. The present article summarizes the material I presented at the Domains IV workshop, plus a few subsequent developments;it is really an extended abstract for a projected journal paper. No proofs are included in the present version. I am grateful to Martin Escardó for many stimulating discussions, and especially for his input to the material in Sections 4.3 and 5.2. I also thank all the participants in the Domains IV workshop for their interest and encouragement. Andrej Bauer drew my attention to some over-enthusiastic claims involving uniform continuity on my Last Slide. The motivating philosophy behind this work owes much to the influence of Martin Hyland, and to my collaboration with Alex Simpson. This research was funded by the EPSRC Research Grant GR/L89532 "Notions of

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Matching typed and untyped realizability

Matching typed and untyped realizability

引用

Tutorial workshop on Realizability Semantics and Applications (Associated to FLoC'99, the 1999 Federated logic Conference)

作者： Longley, John Laboratory for the Foundations of Computer Science University of Edinburgh King's Buildings Edinburgh EH9 3JZ United Kingdom

Realizability interpretations of logics are given by saying what it means for computational objects of some kind to realize logical formulae. The computational objects in question might be drawn from an untyped universe of computation, such as a partial combinatory algebra, or they might be typed objects such as terms of a PCF-style programming language. In some instances, one can show that a particular untyped realizability interpretation matches a particular typed one, in the sense that they give the same set of realizable formulae. In this case, we have a very good fit indeed between the typed language and the untyped realizability model - we refer to this condition as (constructive) logical full abstraction. We give some examples of this situation for a variety of extensions of PCF. Of particular interest are some models that are logically fully abstract for typed languages including non-functional features. Our results establish connections between what is computable in various programming languages and what is true inside various realizability toposes. We consider some examples of logical formulae to illustrate these ideas, in particular their application to exact real-number computability. © 1999 Published by Elsevier B.V.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

COMPUTATIONAL INTERPRETATIONS OF LINEAR logic

引用

THEORETICAL COMPUTER SCIENCE 1993年第1-2期111卷 3-57页

作者： ABRAMSKY, S Department of Computing Imperial College of Science Technology and Medicine 180 Queen's Gate London SW7 2BZ UK

We study Girard's linear logic from the point of view of giving a concrete computational interpretation of the logic, based on the Curry-Howard isomorphism. In the case of Intuitionistic linear logic, this leads to a refinement of the lambda calculus, giving finer control over order of evaluation and storage allocation, while maintaining the logical content of programs as proofs, and computation as cut-elimination. In the classical case, it leads to a concurrent process paradigm with an operational semantics in the style of Berry and Boudol's chemical abstract machine. This opens up a promising new approach to the parallel implementation of functional programming languages;and offers the prospect of typed concurrent programming in which correctness is guaranteed by the typing.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：