the proceedings contain 137 papers. the special focus in this conference is on High-Level Parallel programming Models and Supportive Environments. the topics include: Efficient program partitioning based communication...
ISBN:
(纸本)3540658319
the proceedings contain 137 papers. the special focus in this conference is on High-Level Parallel programming Models and Supportive Environments. the topics include: Efficient program partitioning based communication;a flexible base for transparent shared memory programming models on clusters of PCs;flexible collective operations for distributed object groups;a framework for performance evaluation of scalable computing;recursive individually distributed objects;a flexible combination of on-stack execution and work-stealing;an automatic distribution front-end for java;concurrent language support for interoperable applications;on the distributed implementation of aggregate data structures by program transformation;a transformational framework for skeletal programs;implementing a non-strict functionalprogramming language on a threaded architecture;the biological basis of the immune system as a model for intelligent agents;a formal definition of the phenomenon of collective intelligence and its IQ measure;implementation of data flow logical operations via self-assembly of DNA;a parallel hybrid evolutionary metaheuristic for the period vehicle routing problem;distributed scheduling with decomposed optimization criterion;a parallel genetic algorithm for task mapping on parallel machines;evolution-based scheduling of fault-tolerant programs on multiple processors;a genetic-based fault-tolerant routing strategy for multiprocessor networks;regularity considerations in instance-based locality optimization;parallel ant colonies for combinatorial optimization problems;an analysis of synchronous and asynchronous parallel distributed genetic algorithms with structured and panmictic islands and GA-based parallel image registration on parallel clusters.
this paper presents an object-oriented functionalprogramming language core, its ML-style static type inference and a corresponding type reconstruction algorithm. the language allows object definitions as in Eiffel, a...
详细信息
Existing models for I/O in side-effect free languages focus on functional languages, which are usually based on a largely deterministic reduction strategy, allowing for a strict sequentialization of I/O operations. In...
详细信息
the proceedings contain 31 papers. the special focus in this conference is on Abstract Data Types, 1995. the topics include: Seven years of COMPASS;inductively defined relations;on the role of category theory in the a...
ISBN:
(纸本)3540616292
the proceedings contain 31 papers. the special focus in this conference is on Abstract Data Types, 1995. the topics include: Seven years of COMPASS;inductively defined relations;on the role of category theory in the area of algebraic specifications;a challenge for computing science;the larch shared language: some open problems;the lambda calculus as an abstract data type;unifying theories in different institutions;interchange format for inter-operability of tools and translation;experiments with partial evaluation domains for rewrite specifications;class-sort polymorphism in glider;deontic concepts in the algebraic specification of dynamic systems;reification - changing viewpoint but preserving truth;a category-based equational logic semantics to constraint programming 200;concurrent state transformations on abstract data types;categories of circuits;combining algebraic and set-theoretic specifications;minimal term rewriting systems;an interactive theorem and completeness prover for algebraic specifications with conditional equations;the non-ground case completeness;termination of curryfied rewrite systems;correctness and oracle;behavioural equivalence, bisimulation, and minimal realisation;using limits of parchments to systematically construct institutions of partial algebras;behavioural specifications in type theory;syntax, semantics, and theory;context institutions;object-oriented functionalprogramming and type reconstruction;moving between logical systems;modular algebraic specifications and the orientation of equations into rewrite rules;a model for I/O in equational languages with don't care non-determinism and tool design for structuring mechanisms for algebraic specification languages with initial semantics.
the Curry-Howard isomorphism identifies proofs with typed /spl lambda/-calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive tempor...
详细信息
the Curry-Howard isomorphism identifies proofs with typed /spl lambda/-calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive temporal logic with binding-time analysis. In particular we show how to extend the Curry-Howard isomorphism to include the O ("next") operator from linear-time temporal logic. this yields the simply typed /spl lambda//sup O/-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation for functionalprogramming languages. Further, we prove that normalization in /spl lambda//sup O/ can be done in an order corresponding to the times in the logic, which explains why /spl lambda//sup O/ is relevant to partial evaluation. We then extend /spl lambda//sup O/ to a small functional language, Mini-ML/sup O/, and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the binding-times in the language, a theorem which is the functionalprogramming analog of time-ordered normalization.
We present a functional framework for descriptive computational complexity, in which the Regular, First-order, Ptime, Pspace, k-Exptime, k-Expspace (k/spl ges/1), and Elementary sets have syntactic characterizations. ...
详细信息
We present a functional framework for descriptive computational complexity, in which the Regular, First-order, Ptime, Pspace, k-Exptime, k-Expspace (k/spl ges/1), and Elementary sets have syntactic characterizations. In this framework, typed lambda terms represent inputs and outputs as well as programs. the lambda calculi describing the above computational complexity classes are simply or let-polymorphically typed withfunctionalities of fixed order. they consist of: order 0 atomic constants, order 1 equality among these constants, variables, application, and abstraction. Increasing functionality order by one for these languages corresponds to increasing the computational complexity by one alternation. this exact correspondence is established using a semantic evaluation of languages for each fixed order, which is the primary technical contribution of this paper.
We prove that for sets of Horn clauses saturated under basic paramodulation, the word and unifiability problems are in NP, and the number of minimal unifiers is simply exponential (i). For Horn sets saturated wrt. a s...
详细信息
We prove that for sets of Horn clauses saturated under basic paramodulation, the word and unifiability problems are in NP, and the number of minimal unifiers is simply exponential (i). For Horn sets saturated wrt. a special ordering under the more restrictive inference rule of basic superposition, the word and unifiability problems are still decidable and unification is finitary (ii). We define standard theories, which include and significantly extend shallow theories. Standard presentations can be finitely closed under superposition and result (ii) applies. Generalizing shallow theories to the Horn case, we obtain (two versions of) a language we call Catalog, a natural extension of Datalog to include functions and equality. the closure under paramodulation is finite for Catalog sets, hence (i) applies. Since for shallow sets this closure is even polynomial, shallow unifiability is in NP, which is optimal: unifiability in ground theories is already NP-hard. We even go beyond: the shallow word problem is tractable and for Catalog sets S we prove decidability of the full first-order theory of T(F)/=/sub s/.
Explicit substitutions calculi are formal systems that implement /spl beta/-reduction by means of an internal substitution operator. In that calculi it is possible to delay the application of a substitution to a term ...
详细信息
Explicit substitutions calculi are formal systems that implement /spl beta/-reduction by means of an internal substitution operator. In that calculi it is possible to delay the application of a substitution to a term or to consider terms with partially applied substitutions. the /spl lambda//sub /spl sigma//-calculus of explicit substitutions, proposed by M. Abadi et al. (1991), is a first-order rewriting system that implements substitution and renaming mechanism of /spl lambda/-calculus. However; /spl lambda//sub /spl sigma// does not preserve strong normalisation of /spl lambda/-calculus and it is not a confluent system. Typed variants of /spl lambda//sub /spl sigma// without composition are strongly normalising but not confluent, while variants with composition are confluent but do not preserve strong normalisation. Neither of them enjoys both properties. In this paper we propose the /spl lambda//sub /spl zeta//-calculus. this is, as far as we know, the first confluent calculus of explicit substitutions that preserves strong normalisation.
In our efforts to develop an object-oriented visual programming language, the dataflow model of computation is extended from its traditional functional model to an object-oriented model. It is argued that the concept ...
详细信息
In our efforts to develop an object-oriented visual programming language, the dataflow model of computation is extended from its traditional functional model to an object-oriented model. It is argued that the concept of subroutine in the object-oriented model requires two different types of calling (activation) mechanisms, the synchronous call and the asynchronous call. Asynchronous subroutine call offers a new abstraction mechanism for object-oriented programming, different from the traditional class-based abstraction and functional abstraction.
the lambda calculus is a formal symbolic term rewrite system that has been used for many years both as a mechanism for defining the semantics of programming languages, and as the basis for functionalprogramming langu...
详细信息
the lambda calculus is a formal symbolic term rewrite system that has been used for many years both as a mechanism for defining the semantics of programming languages, and as the basis for functionalprogramming languages. In this paper, we describe a completely visual representation for lambda expressions, VEX, that has several advantages over traditional textual lambda calculus. Although VEX is designed as an expression-oriented component of VIPR, it can also be used in teaching the concepts of lambda calculus as a replacement for or augmentation to the teaching of traditional textual rewrite rules. Many semantic issues in lambda calculus that are confusing to students, including substitution, free variables, and binding, become apparent and explicit in VEX.
暂无评论