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

Structural recursion with locally scoped names

JOURNAL OF FUNCTIONAL programming 2011年第3期21卷 235-286页

作者： Pitts, Andrew M. Univ Cambridge Comp Lab Cambridge CB3 0FD England

this paper introduces a new recursion principle for inductively defined data modulo alpha-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is formulated in simply typed lambda-calculus extended with names that can be restricted to a lexical scope, tested for equality, explicitly swapped and abstracted. the new recursion principle is motivated by the nominal sets notion of 'alpha-structural recursion', whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. the new calculus has a simple interpretation in nominal sets equipped with name-restriction operations. It is shown to adequately represent alpha-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. the paper is a revised and expanded version of Pitts (Nominal System T. In proceedings of the 37th acm SIGACT-sigplan symposium on principles of programming languages, POPL 2010 (Madrid, Spain). acm Press, pp. 159-170, 2010).

关键词： DATA structures (Computer science) programming languages (Electronic computers) CONFERENCES & conventions RECURSION theory TESTING CALCULUS COMPUTER science

来源：评论

学校读者我要写书评

暂无评论

Foundations for Structured programming with GADTs

Foundations for Structured Programming with GADTs

引用

35th acm-sigplan-SIGACT symposium on principles of programming languages

作者： Johann, Patricia Ghani, Neil Rutgers State Univ Camden NJ 08102 USA

ISBN: (纸本)9781595936899

GADTs are at the cutting edge of functional programming and becomemore widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derivean initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools - analogous to the well-known and widely-used ones for algebraic and nested data types - for reasoning about, programming with, and improving the performance of programs involving, GADTs;we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. the main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can bederived. © 2008 acm.

关键词： GADTs initial algebra semantics program fusion

来源：评论

学校读者我要写书评

暂无评论

A Compiler and Run-time System for Network programming languages 12

A Compiler and Run-time System for Network Programming Langu...

引用

39th Annual acm sigplan-SIGACT symposium on principles of programming languages

作者： Monsanto, Christopher Foster, Nate Harrison, Rob Walker, David Princeton Univ Princeton NJ 08544 USA

ISBN: (纸本)9781450310833

Software-defined networks (SDNs) are a new kind of network architecture in which a controller machine manages a distributed collection of switches by instructing them to install or uninstall packet-forwarding rules and report traffic statistics. the recently formed Open Networking Consortium, whose members include Google, Facebook, Microsoft, Verizon, and others, hopes to use this architecture to transform the way that enterprise and data center networks are implemented. In this paper, we define a high-level, declarative language, called Net Core, for expressing packet-forwarding policies on SDNs. Net-Core is expressive, compositional, and has a formal semantics. To ensure that a majority of packets are processed efficiently on switches instead of on the controller we present new compilation algorithms for Net Core and couple them with a new run-time system that issues rule installation commands and traffic-statistics queries to switches. Together, the compiler and run-time system generate efficient rules whenever possible and outperform the simple, manual techniques commonly used to program SDNs today. In addition, the algorithms we develop are generic, assuming only that the packet-matching capabilities available on switches satisfy some basic algebraic laws. Overall, this paper delivers a new design for a high-level network programming language;an improved set of compiler algorithms;a new run-time system for SDN architectures;the first formal semantics and proofs of correctness in this domain;and an implementation and evaluation that demonstrates the performance benefits over traditional manual techniques.

关键词： Software-defined Networking OpenFlow Frenetic Network programming languages Domain specific languages

来源：评论

学校读者我要写书评

暂无评论

Parametric shape analysis via 3-valued logic

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

引用

Conference Record of the Annual acm symposium on principles of programming languages 1999年 105-118页

作者： Sagiv, Mooly Reps, thomas Wilhelm, Reinhard Tel-Aviv Univ Tel-Aviv Israel

We present a family of abstract-interpretation algorithms that are capable of determining `shape invariants' of programs that perform destructive updating on dynamically allocated storage. the main idea is to represent the stores that can possibly arise during execution using three-valued logical structures. Questions about properties of stores can be answered by evaluating predicate-logic formulae using Kleene's semantics of three-valued logic: If a formula evaluates to true, then the formula holds in every store represented by the three-valued structure. If a formula evaluates to false, then the formula does not hold in any store represented by the three-valued structure. If a formula evaluates to unknown, then we do not know if this formula always holds, never holds, or sometimes holds and sometimes does not hold in the stores represented by the three-valued structure. three-valued logical structures are thus a conservative representation of memory stores. the approach described is a parametric framework: It provides the basis for generating a family of shape-analysis algorithms by varying the vocabulary used in the three-valued logic.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

programming with Binders and Indexed Data-Types 12

Programming with Binders and Indexed Data-Types

引用

39th Annual acm sigplan-SIGACT symposium on principles of programming languages

作者： Cave, Andrew Pientka, Brigitte McGill Univ Montreal PQ H3A 2T5 Canada

ISBN: (纸本)9781450310833

We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a restricted form of dependent types where index objects are drawn from contextual LF. this allows the user to specify formal systems within the logical framework LF and index ML types with contextual LF objects. Our language design keeps the index language generic only requiring decidability of equality of the index language providing a modular design. To illustrate the elegance and effectiveness of our language, we give programs for closure conversion and normalization by evaluation. Our three key technical contribution are: 1) We give a bidirectional type system for our core language which is centered around refinement substitutions instead of constraint solving. As a consequence, type checking is decidable and easy to trust, although constraint solving may be undecidable. 2) We give a big-step environment based operational semantics with environments which lends itself to efficient implementation. 3) We prove our language to be type safe and have mechanized our theoretical development in the proof assistant Coq using the fresh approach to binding.

关键词： Logical frameworks higher-order abstract syntax dependent types recursive types

来源：评论

学校读者我要写书评

暂无评论

Automatic Safety Proofs for Asynchronous Memory Operations 11

Automatic Safety Proofs for Asynchronous Memory Operations

引用

16th acm symposium on principles and Practice of Parallel programming

作者： Botincan, Matko Dodds, Mike Donaldson, Alastair F. Parkinson, Matthew J. Univ Cambridge Cambridge CB2 1TN England Univ Oxford Oxford OX1 2JD England Microsoft Res Cambridge Cambridge England

We present a work-in-progress proof system and tool, based on separation logic, for analysing memory safety of multicore programs that use asynchronous memory operations.

ISBN: (纸本)9781450301190

We present a work-in-progress proof system and tool, based on separation logic, for analysing memory safety of multicore programs that use asynchronous memory operations.

关键词： languages theory Verification Separation logic memory safety concurrency

来源：评论

学校读者我要写书评

暂无评论

Contextual Effects for Version-Consistent Dynamic Software Updating and Safe Concurrent programming

Contextual Effects for Version-Consistent Dynamic Software U...

引用

35th acm-sigplan-SIGACT symposium on principles of programming languages

作者： Neamtiu, Iulian Hicks, Michael Foster, Jeffrey S. Pratikakis, Polyvios Univ Maryland Dept Comp Sci College Pk MD 20742 USA

ISBN: (纸本)9781595936899

this paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we compute the effect of the computation that has already occurred (the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency (TVC), a novel correctness property for dynamic software updates. TVC ensures that program mer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. this is an essential step in applications such as data race detection.

关键词： Contextual effects computation effects type and effect systems version consistency dynamic software updating data race detection

来源：评论

学校读者我要写书评

暂无评论

proceedings of the acm sigplan symposium on principles and Practice of Parallel programming, PPOPP

Proceedings of the ACM SIGPLAN Symposium on Principles and P...

引用

4th acm sigplan symposium on principles and Practice of Parallel programming, PPOPP 1993

ISBN: (纸本)0897915895

the proceedings contain 26 papers. the topics discussed include: LogP: towards a realistic model of parallel computation;exploiting task and data parallelism on a multicomputer;ActorSpace: an open distributed programming paradigm;experiences using the ParaScope editor: an interactive parallel programming tool;perturbation analysis of high level instrumentation for SPMD programs;integrating message-passing and shared-memory: early experience;using scheduler information to achieve optimal barrier synchronization performance;and a concurrent copying garbage collector for languages that distinguish (im)mutable data.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A Dynamically Customizable Process-Centered Evaluation Model

A Dynamically Customizable Process-Centered Evaluation Model

引用

11th International acm sigplan symposium on principles and Practice of Declarative programming (PPDP 09)

作者： Clerici, Silvia Zoltan, Cristina Univ Politecn Cataluna Dept Llenguatges & Sistemes Informat Barcelona Spain

ISBN: (纸本)9781605585680

We present the graph operational semantics approach used for defining NiMo nets execution, which mix lazy, data-driven and a weak form of eager evaluation, all in parallel. NiMo is a totally graphic language from the family of higher order typed languages but with a strong data-flow inspiration. Programs are process networks that evolve showing the full state at each execution step and can be dynamically changed or completed. In NiMo parallelization is implicit. the conjunction of two kinds of tags determine which processes are able to act in the same execution step. According to their tag, processes can behave in five modes that can be globally or locally set for each one, and can be also dynamically changed. Combining modes gives a very flexible way to experiment different strategies to increase processor usage, decrease channel population, and achieve subnet synchronization. Together with symbolic execution it also provides the means for generative and multi-stage programming.

关键词： Computation model functional languages

来源：评论

学校读者我要写书评

暂无评论

SCRATCH: a Tool for Automatic Analysis of DMA Races 11

SCRATCH: a Tool for Automatic Analysis of DMA Races

引用

16th acm symposium on principles and Practice of Parallel programming

作者： Donaldson, Alastair F. Kroening, Daniel Ruemmer, Philipp Univ Oxford Comp Lab Oxford OX1 3QD England

We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races.

ISBN: (纸本)9781450301190

We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races.

关键词： languages theory Verification Model checking k-induction Cell BE DMA

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：