We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative thre...
详细信息
ISBN:
(纸本)354022940X
We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant. Our method generalises an approach designed for first-order functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasi-interpretation. We show that these two methods can be combined to obtain an explicit polynomial bound on the resources needed for the execution of the system during an instant. As a second contribution, we introduce a virtual machine and a related bytecode thus producing a precise description of the resources needed for the execution of a system. In this context, we present a suitable control flow analysis that allows to formulate the static analyses for resource control at bytecode level. (C) 2006 Elsevier B.V. All rights reserved.
the proceedings contain 26 papers. the topics discussed include: Acute: high-level programming language design for distributed computation;an expressive language of signatures;dynamic optimization for functional react...
ISBN:
(纸本)1595930647
the proceedings contain 26 papers. the topics discussed include: Acute: high-level programming language design for distributed computation;an expressive language of signatures;dynamic optimization for functional reactive programming using generalized algebraic data types;combining programming withtheorem proving;AtomCaml: first-class atomicity via rollback;a principled approach to operating system construction in Haskell;simple, partial type-inference for system F based on type-containment;type inference, principal typings, and let-polymorphism for first-class mixin modules;backtracking, interleaving, and terminating monad transformers (functional Pearl);scrap your boilerplate with class: extensible generic functions;continuations from generalized stack inspection;fast narrowing-driven partial evaluation for inductively sequential programs;mechanizaing the meta-theory of programming languages;and modular verification of concurrent assembly code with dynamic thread creation and termination.
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper desc...
详细信息
We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. this paper describes the design and implementation issues of those AOP mechanisms that give us insights into the interaction between AOP features and common features in strongly-typed functional languages such as type inference, polymorphic types and curried functions. We implemented a prototype compiler of the language and used the language for separating crosscutting concerns in application programs, including for separating descriptions of a type system from compiler descriptions.
Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, the...
详细信息
Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developing earlier work on associated data types, we propose to add functionally-dependent types as type synonyms to type-class bodies. these associated type synonyms constitute an interesting new alternative to explicit functional dependencies.
In this paper a language-based approach to functionally correct imperative programming is proposed. the approach is based on a programming language called RSP1, which combines dependent types, general recursion, and i...
详细信息
In this paper a language-based approach to functionally correct imperative programming is proposed. the approach is based on a programming language called RSP1, which combines dependent types, general recursion, and imperative features in a type-safe way, while preserving decidability of type checking. the methodology used is that of internal verification, where programs manipulate programmer-supplied proofs explicitly as data. the fundamental technical idea of RSP1 is to identify problematic operations as impure, and keep them out of dependent types. the resulting language is powerful enough to verify statically non-trivial properties of imperative and functional programs. the paper presents the ideas through the examples of statically verified merge sort, statically verified imperative binary search trees, and statically verified directed acyclic graphs.
We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, cons...
详细信息
We design and implement a library for adding backtracking computations to any Haskell monad. Inspired by logic programming, our library provides, in addition to the operations required by the MonadPlus interface, constructs for fair disjunctions, fair conjunctions, conditionals, pruning, and an expressive top-level interface. Implementing these additional constructs is easy in models of backtracking based on streams, but not known to be possible in continuation-based models. We show that all these additional constructs can be generically and monadically realized using a single primitive msplit. We present two implementations of the library: one using success and failure continuations;and the other using control operators for manipulating delimited continuations.
Applied Type System (ATS) is recently proposed as a framework for designing and formalizing (advanced) type systems in support Of practical programming. In ATS, the definition of type equality involves a constraint re...
详细信息
Applied Type System (ATS) is recently proposed as a framework for designing and formalizing (advanced) type systems in support Of practical programming. In ATS, the definition of type equality involves a constraint relation, which may or may not be algorithmically decidable. To support practical programming, we adopted a design in the past that imposes certain restrictions on the syntactic form of constraints so that some effective means can be found for solving constraints automatically. Evidently, this is a rather ad hoc design in its nature. In this paper, we rectify the situation by presenting a fundamentally different design, which we claim to be both novel and practical. Instead of imposing syntactical restrictions on constraints, we provide a means for the programmer to construct proofs that attest to the validity of constraints. In particular, we are to accommodate a programming paradigm that enables the programmer to combine programming withtheorem proving. Also we present some concrete examples in support of the practicality of this design.
Recent research has shown how boilerplate code, or repetitive code for traversing datatypes, can be eliminated using generic programming techniques already available within some implementations of Haskell. One particu...
详细信息
Recent research has shown how boilerplate code, or repetitive code for traversing datatypes, can be eliminated using generic programming techniques already available within some implementations of Haskell. One particularly intractable kind of boilerplate is nameplate, or code having to do with names, name-binding, and fresh name generation. One reason for the difficulty is that operations on data structures involving names, as usually implemented, are not regular instances of standard map, fold, or zip operations. However, in nominal abstract syntax, an alternative treatment of names and binding based on swapping, operations such as a-equivalence, capture-avoiding substitution, and free variable set functions are much better-behaved. In this paper, we show how nominal abstract syntax techniques similar to those of FreshML can be provided as a Haskell library called FreshLib. In addition, we show how existing generic programming techniques can be used to reduce the amount of nameplate code that needs to be written for new datatypes involving names and binding to almost nothing-in short, how to scrap your nameplate.
the 'Scrap your boilerplate' approach to generic programming allows the programmer to write generic functions that can traverse arbitrary data structures, and yet have type-specific cases. However, the origina...
详细信息
the 'Scrap your boilerplate' approach to generic programming allows the programmer to write generic functions that can traverse arbitrary data structures, and yet have type-specific cases. However, the original approach required all the type-specific cases to be supplied at once, when the recursive knot of generic function definition is tied. Hence, generic functions were closed. In contrast, Haskell's type classes support open, or extensible, functions that can be extended with new type-specific cases as new data types are defined. In this paper, we extend the 'Scrap your boilerplate' approach to support this open style. On the way, we demonstrate the desirability of abstraction over type classes, and the usefulness of recursive dictionaries.
Writing loops with tail-recursive function calls is the equivalent of writing them with goto's. Given that loop packages for Lisp-family languages have been around for over 20 years, it is striking that none have ...
详细信息
Writing loops with tail-recursive function calls is the equivalent of writing them with goto's. Given that loop packages for Lisp-family languages have been around for over 20 years, it is striking that none have had much success in the Scheme world. I suggest the reason is that Scheme forces us to be precise about the scoping of the various variables introduced by our loop forms, something previous attempts to design ambitious loop forms have not managed to do. I present the design of a loop package for Scheme with a well-defined and natural scoping rule, based on a notion of control dominance that generalizes the standard lexical-scope rule of the lambda-calculus. the new construct is powerful, clear, modular and extensible. the loop language is defined in terms of an underlying language for expressing control-flow graphs. this language itself has interesting properties as an intermediate representation.
暂无评论