More methods and agent-oriented programming languages have been introduced based on the java language is based, we show that C++ is an agent-oriented programming carried by the object-oriented approach, to do so, the ...
详细信息
Erlang is a concurrent functional programming language designed to ease the development of large-scale distributed soft real-time control applications. It has so far been quite successful in this application domain, d...
详细信息
ISBN:
(纸本)1581132654
Erlang is a concurrent functional programming language designed to ease the development of large-scale distributed soft real-time control applications. It has so far been quite successful in this application domain, despite the fact that its currently available implementations are emulators of virtual machines. In this paper, we improve on the performance aspects of Erlang implementations by presenting HiPE, an open-source native code compiler for Erlang. HiPE is a complete implementation of Erlang, offers flexible integration between emulated and native code, and efficiently supports features crucial for Erlang's application domain such as concurrency. As our performance evaluations show, HiPE is currently the fastest among all Erlang implementations.
We characterize the symmetric structure of Cousot's hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal...
详细信息
ISBN:
(纸本)1581132654
We characterize the symmetric structure of Cousot's hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal method for systematically deriving complementary semantics of programming languages. We prove that under suitable hypothesis the semantics abstraction commutes with respect to domain complementation. This result allows us to prove that angelic and demonic/infinite semantics are complementary and provide a minimal decomposition of all natural-style trace-based, relational, denotational, Dijkstra's predicate transformer and Hoare's axiomatic semantics. We apply this construction to the case of concurrent constraint programming, characterizing well known semantics as abstract interpretation of maximal traces of constraints.
The natural representation of solutions of finite constraint satisfaction problems is as a (set of) function(s) or relation(s). In (constraint) logic programming, answers are in the form of substitutions to the variab...
详细信息
ISBN:
(纸本)1581132654
The natural representation of solutions of finite constraint satisfaction problems is as a (set of) function(s) or relation(s). In (constraint) logic programming, answers are in the form of substitutions to the variables in the query. This results in a not very declarative programming style where a table has to be presented as a complex term. Recently, stable logic programming, also called answer set programming and abductive logic programming have been proposed as approaches supporting a more declarative style for solving such problems. The approach developed in this paper is to extend the constraint domain of a constraint logic programming language with open functions, functions for which the interpretation is not fixed in advance. Their interpretation contains the solution of the problem. This enrichment of the constraint domain yields a language which is almost as expressive as abductive logic programming and is very well suited for expressing finite domain constraint satisfaction problems. Implementation requires only to extend the constraint solver of the underlying CLP language.
We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of such programs. The method resembles the one based on Galois connection as develo...
详细信息
ISBN:
(纸本)1581132654
We present a method for approximating the semantics of probabilistic programs to the purpose of constructing semantics-based analyses of such programs. The method resembles the one based on Galois connection as developed in the Cousot framework for abstract interpretation. The main difference between our approach and the standard theory of abstract interpretation is the choice of linear space structures instead of order-theoretic ones as semantical (concrete and abstract) domains. We show that our method generates "best approximations" according to an appropriate notion of precision defined in terms of a norm. Moreover, if re-casted in a order-theoretic setting these approximations are correct in the sense of classical abstract interpretation theory. We use Concurrent Constraint programming as a reference programming paradigm. The basic concepts and ideas can nevertheless be applied to any other paradigm. The results we present, are intended to be the first step towards a general theory of probabilistic abstract interpretation, which re-formulates the classical theory in a setting suitable for a quantitative reasoning about programs.
Functional logic languages combine nondeterministic search facilities of logic languages with features of functional languages, e.g., monadic I/O to provide a declarative method to deal with I/O actions. Unfortunately...
详细信息
ISBN:
(纸本)1581132654
Functional logic languages combine nondeterministic search facilities of logic languages with features of functional languages, e.g., monadic I/O to provide a declarative method to deal with I/O actions. Unfortunately, monadic I/O cannot be used in programs which split the computation due to nondeterministic reductions. This problem can be avoided if nondeterministic computations are encapsulated by search operators which are available, for instance, in the multi-paradigm language Curry. To support the programmer in identifying nondeterministic parts of a program, we develop a method based on a type and effect system that will find every possible source of nondeterminism. Additionally, such information can be exploited in compilers to optimize deterministically reducible parts of a program.
This paper presents a new type analysis for logic programs. The type information in a set of substitutions is described by a disjunction of variable typings each of which maps a variable to a non-deterministic regular...
详细信息
ISBN:
(纸本)1581132654
This paper presents a new type analysis for logic programs. The type information in a set of substitutions is described by a disjunction of variable typings each of which maps a variable to a non-deterministic regular type. The use of non-deterministic regular types, set union and intersection operators, and disjunctions of variable typings makes the new type analysis more precise than those found in the literature. Experimental results on the performance of the new analysis are given together with comparable results from an existing type analysis. The fundamental problem of checking the emptiness of non-deterministic regular types is more complex in the new analysis. The experimental results, however, show that careful use of tabling reduces the effect to an average of 15% of execution time on a set of benchmarks.
We prove some new results that simplify termination proofs for non-overlapping term rewriting systems. The first one is a refined modularity result (for not necessarily disjoint systems). The second, more important on...
详细信息
ISBN:
(纸本)1581132654
We prove some new results that simplify termination proofs for non-overlapping term rewriting systems. The first one is a refined modularity result (for not necessarily disjoint systems). The second, more important one, gives conditions under which the simplification of right-hand sides (using rules of the original system) is a sound preprocessing step, in the sense that termination of the original system is equivalent to termination of the simplified system, and that the equational theory is preserved. The proofs are based on some powerful structural properties known for non-overlapping systems. Finally, we show how to (partially) extend these results, in particular, to the case of conditional rewrite systems where we additionally treat simplification of conditions of rules. The presented results provide the theoretical basis for sound (and automatic) preprocessing steps when proving termination of (possibly conditional) non-overlapping rewrite systems and equational programs defined by such systems.
We develop a notion of equivalence between interpretations of the simply typed λ-calculus together with an equationally defined abstract data-type, and we show that two interpretations are equivalent if and only if t...
详细信息
ISBN:
(纸本)1581132654
We develop a notion of equivalence between interpretations of the simply typed λ-calculus together with an equationally defined abstract data-type, and we show that two interpretations are equivalent if and only if they are linked by a logical relation. We show that our construction generalises from the simply typed λ-calculus to include the linear λ-calculus and calculi with additional type and term constructors, such as those given by sum types or by a strong monad for modelling phenomena such as partiality or nondeterminism. This is all done in terms of category theoretic structure, using fibrations to model logical relations following Hermida, and adapting Jung and Tiuryn's logical relations of varying arity to provide the completeness results, which form the heart of the work.
This paper gives denotational models for three logic programming languages of progressive complexity, adopting the "logic programming without logic" approach. The first language is the control flow kernel of...
详细信息
ISBN:
(纸本)1581132654
This paper gives denotational models for three logic programming languages of progressive complexity, adopting the "logic programming without logic" approach. The first language is the control flow kernel of sequential Prolog, featuring sequential composition and backtracking. A committed-choice concurrent logic language with parallel composition (parallel And) and don't care nondeterminism is studied next. The third language is the core of Warren's basic Andorra model, combining parallel composition and don't care nondeterminism with two forms of don't know nondeterminism (interpreted as sequential and parallel OR) and favoring deterministic over nondeterministic computation. We show that continuations are a valuable tool in the analysis and design of semantic models for both sequential and parallel logic programming. Instead of using mathematical notation, we use the functional programming language Haskell as a metalanguage for our denotational semantics, and employ monads in order to facilitate the transition from one language under study to another.
暂无评论