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

acm SIGPLAN NOTICES 2015年第1期50卷 663-676页

作者： Padon, Oded Immerman, Neil Karbyshev, Aleksandr Lahav, Ori Sagiv, Mooly Shoham, Sharon Tel Aviv Univ IL-69978 Tel Aviv Israel Univ Massachusetts Amherst MA 01003 USA Acad Coll Tel Aviv Yaffo Tel Aviv Israel

Software-defined networking (SDN) is a new paradigm for operating and managing computer networks. SDN enables logically centralized control over network devices through a "controller" software that operates independently of the network hardware. Network operators can run both in-house and third-party SDN programs on top of the controller, e.g., to specify routing and access control policies. In practice, having the controller handle events limits the network scalability. Therefore, the feasibility of SDN depends on the ability to efficiently decentralize network event-handling by installing forwarding rules on the switches. However, installing a rule too early or too late may lead to incorrect behavior, e.g., (1) packets may be forwarded to the wrong destination or incorrectly dropped;( 2) packets handled by the switch may hide vital information from the controller, leading to incorrect forwarding behavior. The second issue is subtle and sometimes missed even by experienced programmers. The contributions of this paper are two fold. First, we formalize the correctness and optimality requirements for decentralizing network policies. Second, we identify a useful class of network policies which permits automatic synthesis of a controller which performs optimal forwarding rule installation.

关键词： Software-defined networking Network programming languages Synthesis Logic programming Distributed systems

来源：评论

学校读者我要写书评

暂无评论

Databases and programming: Two Subjects Divided by a Common Language? 15

Databases and Programming: Two Subjects Divided by a Common ...

引用

Proceedings of the 42nd Annual acm SIGPLAN-sigact symposium on principles of programming languages

作者： Peter Buneman University of Edinburgh Edinburgh Scotland Uk

ISBN: (纸本)9781450333009

The 1990s saw a hugely productive interaction between database and programming language research. Ideas about type systems from programming languages played a central role in generalizing and adapting relational database systems to new data models. At the same time databases provided some of the best concrete examples of the application of concurrency theory and of the benefits of high-level optimization in functional programming languages. One of the driving ambitions behind this research was the idea that database access should be properly embedded in programming languages: one should not have to be bilingual in order to use a database from a programming language; and that goal has to some extent been *** the past fifteen years, new data models, both for data storage and for data exchange have appeared with depressing regularity and with each such model, the inevitable query language. Does programming language research have anything to contribute to these new languages? Should we take the time to to worry about embedding these models in conventional languages? Over the same period, some interesting new connections between databases and programming languages have emerged, notably in the areas of scientific databases, annotation and provenance. Will this provide new opportunities for cross-fertilization?

关键词： computer science

来源：评论

学校读者我要写书评

暂无评论

Differential Privacy: Now it's Getting Personal

引用

acm SIGPLAN NOTICES 2015年第1期50卷 69-81页

作者： Ebadi, Hamid Sands, David Schneider, Gerardo Chalmers Univ Technol S-41296 Gothenburg Sweden Univ Gothenburg Gothenburg Sweden

Differential privacy provides a way to get useful information about sensitive data without revealing much about any one individual. It enjoys many nice compositionality properties not shared by other approaches to privacy, including, in particular, robustness against side-knowledge. Designing differentially private mechanisms from scratch can be a challenging task. One way to make it easier to construct new differential private mechanisms is to design a system which allows more complex mechanisms (programs) to be built from differentially private building blocks in principled way, so that the resulting programs are guaranteed to be differentially private by construction. This paper is about a new accounting principle for building differentially private programs. It is based on a simple generalisation of classic differential privacy which we call Personalised Differential Privacy (PDP). In PDP each individual has its own personal privacy level. We describe ProPer, a interactive system for implementing PDP which maintains a privacy budget for each individual. When a primitive query is made on data derived from individuals, the provenance of the involved records determines how the privacy budget of an individual is affected: the number of records derived from Alice determines the multiplier for the privacy decrease in Alice's budget. This offers some advantages over previous systems, in particular its fine-grained character allows better utilisation of the privacy budget than mechanisms based purely on the concept of global sensitivity, and it applies naturally to the case of a live database where new individuals are added over time. We provide a formal model of the ProPer approach, prove that it provides personalised differential privacy, and describe a prototype implementation based on McSherry's PINQ system.

关键词： Design languages Theory differential privacy provenance

来源：评论

学校读者我要写书评

暂无评论

30 Years of research and development around Coq 14

30 Years of research and development around Coq

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages, POPL 2014

作者： Huet, Gérard Herbelin, Hugo INRIA Paris Rocquencourt France

No abstract available.

ISBN: (纸本)9781450325448

No abstract available.

关键词： interactive theorem proving certified programming coq proof assistant formalization of mathematics calculus of inductive constructions

来源：评论

学校读者我要写书评

暂无评论

Modular, Higher-Order Cardinality Analysis in Theory and Practice 14

Modular, Higher-Order Cardinality Analysis in Theory and Pra...

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Sergey, Ilya Vytiniotis, Dimitrios Jones, Simon Peyton IMDEA Software Inst Madrid Spain

ISBN: (纸本)9781450325448

Since the mid '80s, compiler writers for functional languages (especially lazy ones) have been writing papers about identifying and exploiting thunks and lambdas that are used only once. However it has proved difficult to achieve both power and simplicity in practice. We describe a new, modular analysis for a higher-order language, which is both simple and effective, and present measurements of its use in a full-scale, state of the art optimising compiler. The analysis finds many single-entry thunks and one-shot lambdas and enables a number of program optimisations.

关键词： languages Theory Analysis compilers program optimisation static analysis functional programming languages Haskell lazy evaluation thunks cardinality analysis types and effects operational semantics

来源：评论

学校读者我要写书评

暂无评论

Applying Quantitative Semantics to Higher-Order Quantum Computing 14

Applying Quantitative Semantics to Higher-Order Quantum Comp...

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Pagani, Michele Selinger, Peter Valiron, Benoit Univ Paris 13 Sorbonne Paris Cite Villetaneuse France Dalhousie Univ Halifax NS Canada Univ Penn CIS Dept Philadelphia PA 19104 USA

ISBN: (纸本)9781450325448

Finding a denotational semantics for higher order quantum computation is a long-standing problem in the semantics of quantum programming languages. Most past approaches to this problem fell short in one way or another, either limiting the language to an un-usably small finitary fragment, or giving up important features of quantum physics such as entanglement. In this paper, we propose a denotational semantics for a quantum lambda calculus with recursion and an infinite data type, using constructions from quantitative semantics of linear logic.

关键词： higher-order quantum computation functional programming completely positive maps categorical model

来源：评论

学校读者我要写书评

暂无评论

Closed Type Families with Overlapping Equations 14

Closed Type Families with Overlapping Equations

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Eisenberg, Richard A. Vytiniotis, Dimitrios Jones, Simon Peyton Weirich, Stephanie Univ Penn Philadelphia PA 19104 USA Microsoft Res Cambridge Cambridge England

ISBN: (纸本)9781450325448

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go beyond conventional dependent type theory in some respects, and have a subtle metatheory.

关键词： Design languages Theory Type families Type-level computation Haskell System FC

来源：评论

学校读者我要写书评

暂无评论

NetKAT: Semantic Foundations for Networks 14

NetKAT: Semantic Foundations for Networks

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Anderson, Carolyn Jane Foster, Nate Guha, Arjun Jeannin, Jean-Baptiste Kozen, Dexter Schlesinger, Cole Walker, David Swarthmore Coll Swarthmore PA 19081 USA Cornell Univ Ithaca NY 14853 USA Univ Massachusetts Amherst MA 01003 USA Carnegie Mellon Univ Pittsburgh PA 15213 USA Princeton Univ Princeton NJ 08544 USA

ISBN: (纸本)9781450325448

Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets;union and sequential composition operators;and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isolation between programs, and establishing the correctness of compilation algorithms.

关键词： Software-defined networking Frenetic Network programming languages Domain-specific languages Kleene algebra with tests NetKAT

来源：评论

学校读者我要写书评

暂无评论

Tabular: A Schema-Driven Probabilistic programming Language 14

Tabular: A Schema-Driven Probabilistic Programming Language

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Gordon, Andrew D. Graepel, Thore Rolland, Nicolas Russo, Claudio Borgstroem, Johannes Guiver, John Univ Edinburgh Edinburgh EH8 9YL Midlothian Scotland Uppsala Univ Uppsala Sweden

ISBN: (纸本)9781450325448

We propose a new kind of probabilistic programming language for machine learning. We write programs simply by annotating existing relational schemas with probabilistic model expressions. We describe a detailed design of our language, Tabular, complete with formal semantics and type system. A rich series of examples illustrates the expressiveness of Tabular. We report an implementation, and show evidence of the succinctness of our notation relative to current best practice. Finally, we describe and verify a transformation of Tabular schemas so as to predict missing values in a concrete database. The ability to query for missing values provides a uniform interface to a wide variety of tasks, including classification, clustering, recommendation, and ranking.

关键词： Bayesian reasoning machine learning model-learner pattern probabilistic programming relational data

来源：评论

学校读者我要写书评

暂无评论

From Parametricity to Conservation Laws, via Noether's Theorem 14

From Parametricity to Conservation Laws, via Noether's Theor...

引用

41st Annual acm SIGPLAN-sigact symposium on principles of programming languages (POPL)

作者： Atkey, Robert United Kingdom

ISBN: (纸本)9781450325448

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy is by Noether's theorem a consequence of a system's invariance under time-shifting. In this paper, we link Reynolds' relational parametricity with Noether's theorem for deriving conserved quantities. We propose an extension of System F omega with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of our extension of F omega, that relational parametricity is enough to satisfy the hypotheses of Noether's theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.

关键词： languages Theory Types Physics classical mechanics relational parametricity higher-kinded types invariance conservation laws

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：