A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. the description of the small-step operational semantics ...
详细信息
ISBN:
(纸本)9781450323260
A concurrent implementation of software transactional memory in Concurrent Haskell using a call-by-need functional language with processes and futures is given. the description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. this implies that our implementation is a correct evaluator for an abstract specification equipped with a bigstep semantics.
this paper presents a new functionalprogramming model for graph structures called stru c tu red graphs. Structured graphs extend conventional algebraic datatypes with explicit definition and manipulation of cycles an...
详细信息
ISBN:
(纸本)9781450310543
this paper presents a new functionalprogramming model for graph structures called stru c tu red graphs. Structured graphs extend conventional algebraic datatypes with explicit definition and manipulation of cycles and/or sharing, and offer a practical and convenient way to program graphs in functionalprogramming languages like Haskell. the representation of sharing and cycles (edges) employs recursive binders and uses an encoding inspired by par a metric higher-order abstract synt a x. Unlike traditional approaches based on mutable references or node/edge lists, well-formedness of the graph structure is ensured statically and reasoning can be done with standard functionalprogramming techniques. Since the binding structure is generic, we can define many useful generic combinators for manipulating structured graphs. We give applications and show how to reason about structured graphs.
Several recent security-typed programming languages, such as Aura, PCML5, and Fine, allow programmers to express and enforce access control and information flow policies. In this paper, we show that security-typed pro...
详细信息
ISBN:
(纸本)9781605587943
Several recent security-typed programming languages, such as Aura, PCML5, and Fine, allow programmers to express and enforce access control and information flow policies. In this paper, we show that security-typed programming can be embedded as a library within a general-purpose dependently typed programming language, Agda. Our library, Aglet, accounts for the major features of existing security-typed programming languages, such as decentralized access control, typed proof-carrying authorization, ephemeral and dynamic policies, authentication, spatial distribution, and information flow. the implementation of Aglet consists of the following ingredients: First, we represent the syntax and proofs of an authorization logic, Garg and Pfenning's BL0, using dependent types. Second, we implement a proof search procedure, based on a focused sequent calculus, to ease the burden of constructing proofs. third, we represent computations using a monad indexed by pre- and post-conditions drawn from the authorization logic, which permits ephemeral policies that change during execution. We describe the implementation of our library and illustrate its use on benchmark examples considered in the literature.
Representing a syntax tree using a data type often involves having many similar-looking constructors. Functions operating on such types often end up having many similar-looking cases. Different languages often make us...
详细信息
ISBN:
(纸本)9781450310543
Representing a syntax tree using a data type often involves having many similar-looking constructors. Functions operating on such types often end up having many similar-looking cases. Different languages often make use of similar-looking constructions. We propose a generic model of abstract syntax trees capable of representing a wide range of typed languages. Syntactic constructs can be composed in a modular fashion enabling reuse of abstract syntax and syntactic processing within and across languages. Building on previous methods of encoding extensible data types in Haskell, our model is a pragmatic solution to Wadler's "expression problem". Its practicality has been confirmed by its use in the implementation of the embedded language Feldspar.
this pearl presents a novel technique for constructing a first-order syntax tree directly from a higher-order interface. We exploit circular programming to generate names for new variables, resulting in a simple yet e...
详细信息
ISBN:
(纸本)9781450323260
this pearl presents a novel technique for constructing a first-order syntax tree directly from a higher-order interface. We exploit circular programming to generate names for new variables, resulting in a simple yet efficient method. Our motivating application is the design of embedded languages supporting variable binding, where it is convenient to use higher-order syntax when constructing programs, but first-order syntax when processing or transforming programs.
this pearl aims to demonstrate the ideas of wholemeal and projective programming using the Towers of Hanoi puzzle as a running example. the puzzle has its own beauty, which we hope to expose along the way.
ISBN:
(纸本)9781605583327
this pearl aims to demonstrate the ideas of wholemeal and projective programming using the Towers of Hanoi puzzle as a running example. the puzzle has its own beauty, which we hope to expose along the way.
We present a method for synthesizing regular expressions for introductory automata assignments. Given a set of positive and negative examples, the method automatically synthesizes the simplest possible regular express...
详细信息
ISBN:
(纸本)9781450344463
We present a method for synthesizing regular expressions for introductory automata assignments. Given a set of positive and negative examples, the method automatically synthesizes the simplest possible regular expression that accepts all the positive examples while rejecting all the negative examples. the key novelty is the search-based synthesis algorithm that leverages ideas from over- and under-approximations to effectively prune out a large search space. We have implemented our technique in a tool and evaluated it with non-trivial benchmark problems that students often struggle with. the results show that our system can synthesize desired regular expressions in 6.7 seconds on the average, so that it can be interactively used by students to enhance their understanding of regular expressions.
We present a novel set of meta-programming primitives for use in a dependently-typed functional language. the types of our meta-programs provide strong and precise guarantees about their termination, correctness and c...
详细信息
ISBN:
(纸本)9781450323260
We present a novel set of meta-programming primitives for use in a dependently-typed functional language. the types of our meta-programs provide strong and precise guarantees about their termination, correctness and completeness. Our system supports typesafe construction and analysis of terms, types and typing contexts. Unlike alternative approaches, they are written in the same style as normal programs and use the language's standard functional computational model. We formalise the new meta-programming primitives, implement them as an extension of Agda, and provide evidence of usefulness by means of two compelling applications in the fields of datatype-generic programming and proof tactics.
We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. this rules out certain mistak...
详细信息
ISBN:
(纸本)9781450323260
We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and ownership. this rules out certain mistakes, including representation exposure and data races, and enables new idioms, such as gradual initialization, memory re-use, and (type) state changes. Although the core static discipline disallows sharing a mutable data structure, Mezzo offers several ways of working around this restriction, including a novel dynamic ownership control mechanism which we dub "adoption and abandon".
programming with versions is a recent proposal that supports multiple versions of software components in a program. though it would provide greater freedom for the programmer, the concept is only realized as a simple ...
详细信息
ISBN:
(纸本)9781450399197
programming with versions is a recent proposal that supports multiple versions of software components in a program. though it would provide greater freedom for the programmer, the concept is only realized as a simple core calculus, called..VL, where a value consists of lambda-terms with multiple versions. We explore a design space of programming with versions in the presence of data structures and module systems, and propose BatakJava, an object-oriented programming language in which multiple versions of a class can be used in a program. this paper presents BatakJava's language design, its core semantics with subject reduction, an implementation as a source-to-Java translator, and a case study to understand how we can exploit multiple versions in BatakJava for developing an application program with an evolving library.
暂无评论