作者：
ZANIOLO, CMCC
3500 West Balcones Center Drive Austin 78759 TX United States
Deductive Databases are coming of age with the emergence of efficient and easy to use systems that support queries, reasoning, and application development on databases through declarative logic-based languages. Buildi...
详细信息
We are convinced that logicprogramming needs specifications as much as traditional programming. For this reason, it is necessary to study also for logic programs how correctness with respect to a given specification ...
详细信息
In this paper we shall consider proofs of declarative properties of logic Programs, i.e. properties associated with the logical semantics of pure logic Programs, in particular what is called the partial correctness of...
详细信息
The independence of negative constraints is a recurring phenomenon in logicprogramming. This property has in fact a natural interpretation in the context of linear programming that we exploit here to address problems...
详细信息
The proceedings contain 48 papers. The special focus in this conference is on theory and practice of Software Development. The topics include: Polymorphic subtype inference: Closing the theory-practice gap;FACILE: A s...
ISBN:
(纸本)9783540509400
The proceedings contain 48 papers. The special focus in this conference is on theory and practice of Software Development. The topics include: Polymorphic subtype inference: Closing the theory-practice gap;FACILE: A symmetric integration of concurrent and functional programming;development of concurrent programs: An example;horn clause programs with polymorphic types: Semantics and resolution;Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions DRAFT;is type checking practical for system configuration?;An introduction to PSFd;processes and functions;binding time analysis for polymorphically typed higher order languages;algebraic specification and functionals for transformational program and meta program development;A fine grain parallel implementation of PARLOG;Specification and verification of TCSP systems by means of partial abstract data types;LEAP: A language with eval and polymorphism;the semantics of program slicing and program integration;Toward formal development of ML programs: Foundations and methodology;on the use of specification styles in the design of distributed systems;specifying avalon objects in larch;a self-applicable partial evaluator for term rewriting systems;verifying correctness of logic programs;specifying the behavior of graphical objects using Esterel;a preprocessor based module system for Prolog;Formulas, processes, and Petri-Nets applied to the specification and verification of a HDLC protocol.
Constructor-based sets of Horn clauses constitute a class of formulas for presenting verification problems occurring in data type specification as well as functional and logicprogramming. Inductive proofs of such cla...
详细信息
Linear logic [6] provides a refinement of functional programming and suggests a new implementation technique, with the following features: • a synthesis of strict and lazy evaluation, • a clean...
详细信息
Linear logic [6] provides a refinement of functional programming and suggests a new implementation technique, with the following features: • a synthesis of strict and lazy evaluation, • a clean semantics of side effects, • no garbage collector.
A comparison is performed between narrowing and SLD-resolution as regards their use in semantic unification (or E -unification). An E -unification algorithm based on flattening and SLD-resolution is developed and prov...
详细信息
A comparison is performed between narrowing and SLD-resolution as regards their use in semantic unification (or E -unification). An E -unification algorithm based on flattening and SLD-resolution is developed and proved sound and complete by establishing a correspondence between narrowing sequences and resolution sequences. An E -unification algorithm based on a refined (“selection”) narrowing strategy is derived by adapting the SLD-strategy to narrowing. Finally, possible applications to the domain of logic+functional programming are considered.
Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations ...
详细信息
Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning. In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (e.g., OR-parallelism or Prolog backtracking) is assumed. The method may also be used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.
The proceedings contain 28 papers. The topics discussed include: type inference with subtypes;a proper extension of ml with an effective type-assignment;global value numbers and redundant computations;strictness analy...
ISBN:
(纸本)0897912527
The proceedings contain 28 papers. The topics discussed include: type inference with subtypes;a proper extension of ml with an effective type-assignment;global value numbers and redundant computations;strictness analysis aids time analysis;structural subtyping and the notion of power type;on the adequacy of program dependence graphs for representing programs;polymorphic effect systems;stores and partial continuations as first-class objects in a language and its environment;integrating non-interfering versions of programs;detecting equality of variables in programs;correct flow analysis in continuation semantics;sacrificing simplicity for convenience: where do you draw the line?;towards fully abstract semantics for local variables: preliminary report;bisimulation can't be traced: preliminary report;the theory and practice of first-class prompts;inductive methods for reasoning about abstract data types;a compositional approach to superimposition;efficient dataflow analysis of logic programs;incremental data flow analysis via dominator and attribute updates;lifetime analysis of dynamically allocated objects;and optimal code generation for expression trees: an application of BURS theory.
暂无评论