Algebraic and Logic Programming [[electronic resource] ] : 4th International Conference, ALP '94, Madrid, Spain, September 14-16, 1994. Proceedings / / edited by Giorgio Levi, Mario Rodriguez-Artalejo |
Edizione | [1st ed. 1994.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1994 |
Descrizione fisica | 1 online resource (X, 314 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computers Programming languages (Electronic computers) Computer logic Mathematical logic Artificial intelligence Software Engineering/Programming and Operating Systems Theory of Computation Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
ISBN | 3-540-48791-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Concurrent constraint programming -- Specifications using multiple-conclusion logic programs -- Viewing a program transformation system at work -- Proving implications by algebraic approximation -- Sufficient completeness and parameterized proofs by induction -- Proving behavioural theorems with standard first-order logic -- How to realize LSE narrowing -- Compositional analysis for equational Horn programs -- Equation solving in projective planes and planar ternary rings -- From eventual to atomic and locally atomic CC programs: A concurrent semantics -- Concurrent logic programming as uniform linear proofs -- Three-valued completion for abductive logic programs -- A sequential reduction strategy -- On modularity of termination and confluence properties of conditional rewrite systems -- Syntactical analysis of total termination -- Logic programs as term rewriting systems -- Higher-order minimal function graphs -- Reasoning about layered, wildcard and product patterns -- Preserving universal termination through unfold/fold -- A logic for variable aliasing in logic programs. |
Record Nr. | UNISA-996466130003316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1994 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Algebraic and Logic Programming [[electronic resource] ] : Third International Conference, Volterra, Italy, September 2-4, 1992. Proceedings / / edited by Helene Kirchner, Giorgio Levi |
Edizione | [1st ed. 1992.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1992 |
Descrizione fisica | 1 online resource (IX, 460 p.) |
Disciplina | 005.13/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Software engineering Programming languages (Electronic computers) Computer logic Mathematical logic Theory of Computation Software Engineering/Programming and Operating Systems Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-47302-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Outline of an object-oriented calculus of higher type -- High-level-replacement systems for equational algebraic specifications -- Termination of rewrite systems by elementary interpretations -- Termination of order-sorted rewriting -- Generalized sufficient conditions for modular termination of rewriting -- A theory of first-order built-in's of prolog -- Fixpoint semantics for partial computed answer substitutions and call patterns -- Oracle semantics for Prologa -- On the relation between primitive recursion, schematization, and divergence -- Term rewriting with sharing and memoïzation -- Definitional trees -- Multiparadigm logic programming -- Non-linear real constraints in constraint logic programming -- A general scheme for constraint functional logic programming -- Incremental rewriting in narrowing derivations -- Counterexamples to completeness results for basic narrowing (extended abstract) -- Uniform narrowing strategies -- Proof by consistency in constructive systems with final algebra semantics -- A fast algorithm for ground normal form analysis -- Eta-conversion for the languages of explicit substitutions -- Serialisation analysis of concurrent logic programs -- Implementation of a toolset for prototyping algebraic specifications of concurrent systems -- Axiomatizing permutation equivalence in the ?-calculus -- A CLP view of logic programming -- Partial deduction of logic programs WRT well-founded semantics -- The finiteness of logic programming derivations -- Theorem proving for hierarchic first-order theories -- A goal oriented strategy based on completion -- On n-syntactic equational theories. |
Record Nr. | UNISA-996465485803316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1992 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Foundations of Logic and Functional Programming [[electronic resource] ] : Workshop, Trento, Italy, December 15-19, 1986. Proceedings / / edited by Mauro Boscarol, Luigia Carlucci Aiello, Giorgio Levi |
Edizione | [1st ed. 1988.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1988 |
Descrizione fisica | 1 online resource (VIII, 224 p.) |
Disciplina | 005.11 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computer programming
Programming Techniques |
ISBN | 3-540-39126-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Rum an intensional theory of function and control abstractions -- Typechecking dependent types and subtypes -- Reducing recursion to iteration by means of pairs and N-tuples -- Unification revisited -- Rule rewriting methods for efficient implementations of horn logic -- PAP: a logic programming system based on a constructive logic -- A completeness result for E-unification algorithms based on conditional narrowing -- Representing domain structure of many-sorted Prolog knowledge bases -- Horn: An inference engine prototype to implement intelligent systems -- Hints for the design of a set calculus oriented to Automated Deduction. |
Record Nr. | UNISA-996465680903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1988 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 1987 [[electronic resource] ] : Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP '87) / / edited by Hartmut Ehrig, Robert Kowalski, Giorgio Levi, Ugo Montanari |
Edizione | [1st ed. 1987.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1987 |
Descrizione fisica | 1 online resource (XVIII, 294 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Mathematical logic Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-47746-2 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | On the complexity of branching programs and decision trees for clique functions -- Average complexity of additive properties for multiway tries: A unified approach -- Longest common factor of two words -- An unification semi-algorithm for intersection type schemes -- Optimal run time optimization proved by a new look at abstract interpretations -- Transformation ordering -- On parametric algebraic specifications with clean error handling -- Toward formal development of programs from algebraic specifications: Implementations revisited -- Finite algebraic specifications of semicomputable data types -- On the semantics of concurrency: Partial orders and transition systems -- CCS without ?'s -- A fully observational model for infinite behaviours of communicating systems -- SMoLCS-driven concurrent calculi -- Parameterized horn clause specifications: Proof theory and correctness -- Partial composition and recursion of module specifications -- Efficient representation of taxonomies -- Applications of compactness in the Smyth powerdomain of streams -- Characterizing Kripke structures in temporal logic -- Dialogue with a proof system -- Induction principles formalized in the calculus of constructions -- Algebraic semantics. |
Record Nr. | UNISA-996465971903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1987 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
TAPSOFT '87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23 - 27 1987 [[electronic resource] ] : Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and Logic Programming and Specifications (CFLP) / / edited by Hartmut Ehrig, Robert A. Kowalski, Giorgio Levi, Ugo Montanari |
Edizione | [1st ed. 1987.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1987 |
Descrizione fisica | 1 online resource (XIV, 336 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Mathematical logic Software Engineering Logics and Meanings of Programs Mathematical Logic and Formal Languages |
ISBN | 3-540-47717-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Models and equality for logical programming -- Fifth generation computer project: Current research activity and future plans -- A compositive abstraction algorithm for combinatory logic -- Linear logic and lazy computation -- The natural dynamic semantics of mini-Standard ML -- Listlog — A PROLOG extension for list processing -- Intensional negation of logic programs: Examples and implementation techniques -- Improving the execution speed of compiled Prolog with modes, clause selection, and determinism -- Simulation results of a multiprocessor PROLOG architecture based on a distributed and/or graph -- Generating efficient code from strictness annotations -- Hoisting: Lazy evaluation in a cold climate -- Inductive assertion method for logic programs -- Higher order generalization in program derivation -- Implementing algebraically specified abstract data types in an imperative programming language -- A declarative environment for concurrent logic programming -- Or-parallel execution models of Prolog -- Retractions: A functional paradigm for logic programming -- Refined strategies for semantic unification -- Extensional models for polymorphism -- A type discipline for program modules -- Theory and practice of canonical term functors in abstract data type specifications. |
Record Nr. | UNISA-996465964903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1987 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Verification, Model Checking, and Abstract Interpretation [[electronic resource] ] : 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings / / edited by Bernhard Steffen, Giorgio Levi |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XI, 325 p.) |
Disciplina | 005.82 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer science Programming languages (Electronic computers) Software Engineering Logics and Meanings of Programs Computer Science, general Programming Languages, Compilers, Interpreters |
ISBN |
1-280-30668-8
9786610306688 3-540-24622-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Tutorial -- Security, Protocols, and Trust -- Security -- Security Types Preserving Compilation -- History-Dependent Scheduling for Cryptographic Processes -- Formal Methods I -- Construction of a Semantic Model for a Typed Assembly Language -- Rule-Based Runtime Verification -- On the Expressive Power of Canonical Abstraction -- Boolean Algebra of Shape Analysis Constraints -- Approximate Probabilistic Model Checking -- Completeness and Complexity of Bounded Model Checking -- Model Checking for Object Specifications in Hidden Algebra -- Formal Methods II -- Model Checking Polygonal Differential Inclusions Using Invariance Kernels -- Checking Interval Based Properties for Reactive Systems -- Widening Operators for Powerset Domains -- Type Inference for Parameterized Race-Free Java -- Certifying Temporal Properties for Compiled C Programs -- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking -- Static Analysis versus Software Model Checking for Bug Finding -- Automatic Inference of Class Invariants -- Liveness with Invisible Ranking -- A Complete Method for the Synthesis of Linear Ranking Functions -- Symbolic Implementation of the Best Transformer -- Formal Methods III -- Constructing Quantified Invariants via Predicate Abstraction -- Analysis of Recursive Game Graphs Using Data Flow Equations -- Applying Jlint to Space Exploration Software -- Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone -- A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal. |
Record Nr. | UNISA-996465923103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Verification, Model Checking, and Abstract Interpretation : 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings / / edited by Bernhard Steffen, Giorgio Levi |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (XI, 325 p.) |
Disciplina | 005.82 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer science Programming languages (Electronic computers) Software Engineering Logics and Meanings of Programs Computer Science, general Programming Languages, Compilers, Interpreters |
ISBN |
1-280-30668-8
9786610306688 3-540-24622-3 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Tutorial -- Security, Protocols, and Trust -- Security -- Security Types Preserving Compilation -- History-Dependent Scheduling for Cryptographic Processes -- Formal Methods I -- Construction of a Semantic Model for a Typed Assembly Language -- Rule-Based Runtime Verification -- On the Expressive Power of Canonical Abstraction -- Boolean Algebra of Shape Analysis Constraints -- Approximate Probabilistic Model Checking -- Completeness and Complexity of Bounded Model Checking -- Model Checking for Object Specifications in Hidden Algebra -- Formal Methods II -- Model Checking Polygonal Differential Inclusions Using Invariance Kernels -- Checking Interval Based Properties for Reactive Systems -- Widening Operators for Powerset Domains -- Type Inference for Parameterized Race-Free Java -- Certifying Temporal Properties for Compiled C Programs -- Verifying Atomicity Specifications for Concurrent Object-Oriented Software Using Model-Checking -- Static Analysis versus Software Model Checking for Bug Finding -- Automatic Inference of Class Invariants -- Liveness with Invisible Ranking -- A Complete Method for the Synthesis of Linear Ranking Functions -- Symbolic Implementation of the Best Transformer -- Formal Methods III -- Constructing Quantified Invariants via Predicate Abstraction -- Analysis of Recursive Game Graphs Using Data Flow Equations -- Applying Jlint to Space Exploration Software -- Why AI + ILP Is Good for WCET, but MC Is Not, Nor ILP Alone -- A Grand Challenge for Computing: Towards Full Reactive Modeling of a Multi-cellular Animal. |
Record Nr. | UNINA-9910144210303321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|