Cambridge Tracts in Theoretical Computer Science – serie

Visar alla böcker i serien Cambridge Tracts in Theoretical Computer Science. Handla med fri frakt och snabb leverans.

67 produkter

Kategorier

67 produkter

Del 27 - Cambridge Tracts in Theoretical Computer Science
Programs, Recursion and Unbounded Choice
AvWim H. Hesselink,C. J. van Rijsbergen
Häftad, Engelska, 2005
657 kr
Skickas inom 10-15 vardagar
This book is a complete account of the predicate transformation calculus semantics of sequential programs, including repetitions, recursive procedures, computational induction and unbounded nondeterminacy. Predicate transformation semantics are the best specification method for the development of correct and well-structured computer programs. The author develops this theory to a greater depth than has been achieved before, and describes it in a way that makes it readily compatible with programming rules for partial and total correctness of repetitions and recursive procedures, supplies new rules for proving incorrectness, and a stronger rule for proving that two programs satisfy the same specifications. Finally, the semantics are extended so that non-terminating programs can be specified as well. This will be essential reading for all computer scientists working in specification and verification of programs.
Del 23 - Cambridge Tracts in Theoretical Computer Science
Nets, Terms and Formulas
Three Views of Concurrent Processes and their Relationship
AvE. -R. Olderog,C. J. Van Rijsbergenm. fl.
Häftad, Engelska, 2005
657 kr
Skickas inom 10-15 vardagar
The author presents a theory of concurrent processes where three different semantic description methods that are usually studied in isolation are brought together. Petri nets describe processes as concurrent and interacting machines; algebraic process terms describe processes as abstract concurrent processes; and logical formulas specify the intended communication behaviour of processes. At the heart of this theory are two sets of transformation rules for the top-down design of concurrent processes. The first set can be used to transform stepwise logical formulas into process terms, whilst process terms can be transformed into Petri nets by the second set. These rules are based on novel techniques for the operational and denotational semantics of concurrent processes. Various results and relationships between nets, terms and formulas starting with formulas and illustrated by examples. The use of transformations is demonstrated in a series of case studies, and the author also identifies directions for research.
Del 34 - Cambridge Tracts in Theoretical Computer Science
Two-Level Functional Languages
AvFlemming Nielson,Hanne Riis Nielsonm. fl.
Häftad, Engelska, 2005
739 kr
Skickas inom 10-15 vardagar
The authors describe here a framework in which the type notation of functional languages is extended to include a notation for binding times (that is run-time and compile-time) that distinguishes between them. Consequently the ability to specify code and verify program correctness can be improved. Two developments are needed, the first of which introduces the binding time distinction into the lambda calculus, in a manner analogous with the introduction of types into the untyped lambda calculus. Methods are also presented for introducing combinators for run-time. The second concerns the interpretation of the resulting language, which is known as the mixed lambda-calculus and combinatory logic. The notion of 'parametrized semantics' is used to describe code generation and abstract interpretation. The code generation is for a simple abstract machine designed for the purpose; it is close to the categorical abstract machine. The abstract interpretation focuses on a strictness analysis that generalises Wadler's analysis for lists.
Del 19 - Cambridge Tracts in Theoretical Computer Science
Extensions of First-Order Logic
AvMaria Manzano,C. J. Van Rijsbergenm. fl.
Häftad, Engelska, 2005
973 kr
Skickas inom 10-15 vardagar
Classical logic has proved inadequate in various areas of computer science, artificial intelligence, mathematics, philosopy and linguistics. This is an introduction to extensions of first-order logic, based on the principle that many-sorted logic (MSL) provides a unifying framework in which to place, for example, second-order logic, type theory, modal and dynamic logics and MSL itself. The aim is two fold: only one theorem-prover is needed; proofs of the metaproperties of the different existing calculi can be avoided by borrowing them from MSL. To make the book accessible to readers from different disciplines, whilst maintaining precision, the author has supplied detailed step-by-step proofs, avoiding difficult arguments, and continually motivating the material with examples. Consequently this can be used as a reference, for self-teaching or for first-year graduate courses.
Del 40 - Cambridge Tracts in Theoretical Computer Science
Free Choice Petri Nets
AvJorg Desel,Javier Esparzam. fl.
Häftad, Engelska, 2005
584 kr
Skickas inom 10-15 vardagar
Petri nets are a popular and powerful formal model for the analysis and modelling of concurrent systems, and a rich theory has developed around them. Petri nets are taught to undergraduates, and also used by industrial practitioners. This book focuses on a particular class of petri nets, free choice petri nets, which play a central role in the theory. The text is very clearly organised, with every notion carefully explained and every result proved. Clear exposition is given for place invariants, siphons, traps and many other important analysis techniques. The material is organised along the lines of a course book, and each chapter contains numerous exercises, making this book ideal for graduate students and research workers alike.
Del 32 - Cambridge Tracts in Theoretical Computer Science
The Logic of Typed Feature Structures
With Applications to Unification Grammars, Logic Programs and Constraint Resolution
AvRobert L. Carpenter,C. J. Van Rijsbergenm. fl.
Häftad, Engelska, 2005
657 kr
Skickas inom 10-15 vardagar
This book develops the theory of typed feature structures, a data structure that generalizes both first-order terms and feature structures of unification-based grammars to include inheritance, typing, inequality, cycles and intensionality. The resulting synthesis serves as a logical foundation for grammars, logic programming and constraint-based reasoning systems. A logical perspective is adopted which employs an attribute-value description language along with complete equational axiomatizations of the various systems of feature structures. At the same time, efficiency concerns are kept in mind and complexity and representability results are provided. The application of feature structures to phrase structure grammars is described and completeness results are shown for standard evaluation strategies. Definite clause logic programs are treated as a special case of phrase structure grammars. Constraint systems are introduced and an enumeration technique is developed for solving arbitrary attribute-value logic constraints. This book, with its innovative approach to data structure, will be essential reading for researchers in computational linguistics, logic programming and knowledge representation. Its self-contained presentation makes it flexible enough to serve as both a research tool and a text book.
Del 28 - Cambridge Tracts in Theoretical Computer Science
Deductive and Declarative Programming
AvPeter Padawitz,C. J. van Rijsbergen
Häftad, Engelska, 2006
657 kr
Skickas inom 10-15 vardagar
Declarative programs consist of mathematical functions and relations and are amenable to formal specification and verification, since the methods of logic and proof can be applied to the programs in a well-defined manner. Here Dr Padawitz emphasizes verification based on logical inference rules, i.e. deduction (in contrast with model-theoretic approaches, deductive methods can be automated to some extent). His treatment of the subject differs from others in that he tries to capture the actual styles and applications of programming; neither too general with respect to the underlying logic, nor too restrictive for the practice of programming. He generalizes and unifies results from classical theorem-proving and term rewriting to provide proof methods tailored to declarative program synthesis and verification. Detailed examples accompany the development of the methods, whose use is supported by a documented prototyping system. The book can be used for graduate courses or as a reference for researchers in formal methods, theorem-proving and declarative languages.
Del 39 - Cambridge Tracts in Theoretical Computer Science
The Uncertain Reasoner's Companion
A Mathematical Perspective
AvJ. B. Paris,C. J. Van Rijsbergenm. fl.
Häftad, Engelska, 2006
684 kr
Skickas inom 10-15 vardagar
Reasoning under uncertainty, that is, making judgements with only partial knowledge, is a major theme in artificial intelligence. Professor Paris provides here an introduction to the mathematical foundations of the subject. It is suited for readers with some knowledge of undergraduate mathematics but is otherwise self-contained, collecting together the key results on the subject and formalizing within a unified framework the main contemporary approaches and assumptions. The author has concentrated on giving clear mathematical formulations, analyses, justifications and consequences of the main theories about uncertain reasoning, so the book can serve as a textbook for beginners or as a starting point for further basic research into the subject. It will be welcomed by graduate students and research workers in logic, philosophy and computer science as an account of how mathematics and artificial intelligence can complement and enrich each other.
Del 3 - Cambridge Tracts in Theoretical Computer Science
Understanding Z
A Specification Language and its Formal Semantics
AvJ. M. Spivey
Häftad, Engelska, 2008
509 kr
Skickas inom 10-15 vardagar
The Z notation is a language for expressing mathematical specifications of computing systems. By providing a formal semantics for Z, this book justifies the claim that Z is a precise specification language, and provides a standard framework for understanding Z specifications. Z is compared with other methods such as VDM and CLEAR, and in the final chapter, a number of studies in Z style are presented to show that Z can be used in a wide variety of specification tasks. This book will appeal to those who wish to deepen their understanding of the mathematical background of the Z method, those who want a concise definition of the language, and those interested in the design of specification languages.
Del 42 - Cambridge Tracts in Theoretical Computer Science
Basic Simple Type Theory
AvJ. Roger Hindley
Häftad, Engelska, 2008
520 kr
Skickas inom 10-15 vardagar
Type theory is one of the most important tools in the design of higher-level programming languages, such as ML. This book introduces and teaches its techniques by focusing on one particularly neat system and studying it in detail. In this way, all the key ideas are covered without getting involved in the complications of more advanced systems, but concentrating rather on the principles that make the theory work in practice. This book takes a type-assignment approach to type theory, and the system considered is the simplest polymorphic one. The author covers all the basic ideas, including the system's relation to propositional logic, and gives a careful treatment of the type-checking algorithm which lies at the heart of every such system. Also featured are two other interesting algorithms that have been buried in inaccessible technical literature. The mathematical presentation is rigorous but clear, making the book at a level which can be used as an introduction to type theory for computer scientists.
Del 46 - Cambridge Tracts in Theoretical Computer Science
Domains and Lambda-Calculi
AvRoberto M. Amadio,Pierre-Louis Curien
Häftad, Engelska, 2008
798 kr
Skickas inom 10-15 vardagar
This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way, and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modelling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computer science.
Del 22 - Cambridge Tracts in Theoretical Computer Science
Mathematical Theory of Domains
AvV. Stoltenberg-Hansen,I. Lindströmm. fl.
Häftad, Engelska, 2008
747 kr
Skickas inom 10-15 vardagar
Domain theory is an established part of theoretical computer science, used in giving semantics to programming languages and logics. In mathematics and logic it has also proved to be useful in the study of algorithms. This book is devoted to providing a unified and self-contained treatment of the subject. The theory is presented in a mathematically precise manner which nevertheless is accessible to mathematicians and computer scientists alike. The authors begin with the basic theory including domain equations, various domain representations and universal domains. They then proceed to more specialized topics such as effective and power domains, models of lambda-calculus and so on. In particular, the connections with ultrametric spaces and the Kleene-Kreisel continuous functionals are made precise. Consequently the text will be useful as an introductory textbook (earlier versions have been class-tested in Uppsala, Gothenburg, Passau, Munich and Swansea), or as a general reference for professionals in computer science and logic.
Del 44 - Cambridge Tracts in Theoretical Computer Science
Information Flow
The Logic of Distributed Systems
AvJon Barwise,Jerry Seligman
Häftad, Engelska, 2008
798 kr
Skickas inom 10-15 vardagar
Information is a central topic in computer science, cognitive science and philosophy. In spite of its importance in the 'information age', there is no consensus on what information is, what makes it possible, and what it means for one medium to carry information about another. Drawing on ideas from mathematics, computer science and philosophy, this book addresses the definition and place of information in society. The authors, observing that information flow is possible only within a connected distribution system, provide a mathematically rigorous, philosophically sound foundation for a science of information. They illustrate their theory by applying it to a wide range of phenomena, from file transfer to DNA, from quantum mechanics to speech act theory.
Del 36 - Cambridge Tracts in Theoretical Computer Science
Algebraic Specification of Communication Protocols
AvS. Mauw,G. J. Veltink
Häftad, Engelska, 2008
629 kr
Skickas inom 10-15 vardagar
Modern computer networks now circle the world, but the transmission of information between them depends on the many different protocols that define the behaviour of the sender and receiver. It is clear therefore, that the accurate description of these protocols is important if harmonious communication is to be maintained. In this book the authors use the formal specification language PSF to provide an unambiguous description of several communication protocols of varying levels of complexity, ranging from the alternating bit protocol to the token ring protocol. Beginners, as well as professionals in the field of communication protocols, will benefit from both the methods of specification described and the protocols discussed in this book.
Del 47 - Cambridge Tracts in Theoretical Computer Science
Data Refinement
Model-Oriented Proof Methods and their Comparison
AvWillem-Paul de Roever,Kai Engelhardt
Häftad, Engelska, 2008
795 kr
Skickas inom 10-15 vardagar
The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors concentrate in the first part on the general principles needed to prove data refinement correct. They begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The book's second part contains a detailed survey of important methods in this field, which are carefully analysed, and shown to be either incomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all these methods can be described and analysed in terms of two simple notions: forward and backward simulation. The book is self-contained, going from advanced undergraduate level and taking the reader to the state of the art in methods for proving simulation.
Del 49 - Cambridge Tracts in Theoretical Computer Science
Hybrid Graph Theory and Network Analysis
AvLadislav Novak,Alan Gibbons
Häftad, Engelska, 2009
544 kr
Skickas inom 10-15 vardagar
First published in 1999, this book combines traditional graph theory with the matroidal view of graphs and throws light on mathematical aspects of network analysis. This approach is called here hybrid graph theory. This is essentially a vertex-independent view of graphs naturally leading into the domain of graphoids, a generalisation of graphs. This enables the authors to combine the advantages of both the intuitive view from graph theory and the formal mathematical tools from the theory of matroids. A large proportion of the material is either new or is interpreted from a fresh viewpoint. Hybrid graph theory has particular relevance to electrical network analysis, which was one of the earliest areas of application of graph theory. It was essentially out of developments in this area that hybrid graph theory evolved.
Del 4 - Cambridge Tracts in Theoretical Computer Science
Lambda-calculus, Combinators and Functional Programming
AvG. E. Revesz
Häftad, Engelska, 2009
767 kr
Skickas inom 10-15 vardagar
Originally published in 1988, this book presents an introduction to lambda-calculus and combinators without getting lost in the details of mathematical aspects of their theory. Lambda-calculus is treated here as a functional language and its relevance to computer science is clearly demonstrated. The main purpose of the book is to provide computer science students and researchers with a firm background in lambda-calculus and combinators and show the applicabillity of these theories to functional programming. The presentation of the material is self-contained. It can be used as a primary text for a course on functional programming. It can also be used as a supplementary text for courses on the structure and implementation of programming languages, theory of computing, or semantics of programming languages.
Del 31 - Cambridge Tracts in Theoretical Computer Science
Higher Order Logic and Hardware Verification
AvT. F. Melham
Häftad, Engelska, 2009
544 kr
Skickas inom 10-15 vardagar
This 1993 book shows how formal logic can be used to specify the behaviour of hardware designs and reason about their correctness. A primary theme of the book is the use of abstraction in hardware specification and verification. The author describes how certain fundamental abstraction mechanisms for hardware verification can be formalised in logic and used to express assertions about design correctness and the relative accuracy of models of hardware behaviour. His approach is pragmatic and driven by examples. He also includes an introduction to higher-order logic, which is a widely used formalism in this subject, and describes how that formalism is actually used for hardware verification. The book is based in part on the author's own research as well as on graduate teaching. Thus it can be used to accompany courses on hardware verification and as a resource for research workers.
Del 11 - Cambridge Tracts in Theoretical Computer Science
A Unifying Framework for Structured Analysis and Design Models
An Approach Using Initial Algebra Semantics and Category Theory
AvT. H. Tse
Häftad, Engelska, 2009
560 kr
Skickas inom 10-15 vardagar
Structured methodologies are a popular and powerful tool in information systems development. Many different ones exist, each employing a number of models and so a specification must be converted from one form to another during the development process. To solve this problem, Dr Tse proposes in this 1991 book a unifying framework behind popular structured models. He approaches the problem from the viewpoints of algebra and category theory. He not only develops the frameworks but also illustrates their practical and theoretical usefulness. Thus this book will provide insight for software engineers into how methodologies can be formalised and will open up a range of applications and problems for theoretical computer scientists.
Del 21 - Cambridge Tracts in Theoretical Computer Science
The Clausal Theory of Types
AvD. A. Wolfram
Häftad, Engelska, 2009
408 kr
Skickas inom 10-15 vardagar
Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality, known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds in higher-order equational theories and uses higher-order rewriting. The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.
Del 15 - Cambridge Tracts in Theoretical Computer Science
Design Theory and Computer Science
AvSubrata Dasgupta
Häftad, Engelska, 2009
932 kr
Skickas inom 10-15 vardagar
The logic and methodology of design is examined in this book from the perspective of computer science. Computers provide the context for this examination both by discussion of the design process for hardware and software systems and by consideration of the role of computers in design in general. The central question posed by the author is whether or not we can construct a theory of design. This book concentrates upon the relationship between design, mathematics and science and thus its audience must include designers and software designers as well as computer scientists.
Del 54 - Cambridge Tracts in Theoretical Computer Science
Concurrency Verification
Introduction to Compositional and Non-compositional Methods
AvWillem-Paul de Roever,Frank de Boerm. fl.
Häftad, Engelska, 2012
1 098 kr
Skickas inom 10-15 vardagar
This is a systematic and comprehensive introduction both to compositional proof methods for the state-based verification of concurrent programs, such as the assumption-commitment and rely-guarantee paradigms, and to noncompositional methods, whose presentation culminates in an exposition of the communication-closed-layers (CCL) paradigm for verifying network protocols. Compositional concurrency verification methods reduce the verification of a concurrent program to the independent verification of its parts. If those parts are tightly coupled, one additionally needs verification methods based on the causal order between events. These are presented using CCL. The semantic approach followed here allows a systematic presentation of all these concepts in a unified framework which highlights essential concepts. This 2001 book is self-contained, guiding the reader from advanced undergraduate level. Every method is illustrated by examples, and a picture gallery of some of the subject's key figures complements the text.
Del 12 - Cambridge Tracts in Theoretical Computer Science
Nonmonotonic Reasoning
Logical Foundations of Commonsense
AvGerhard Brewka
Häftad, Engelska, 2012
601 kr
Skickas inom 10-15 vardagar
In this 1991 book the author gives a broad overview of different areas of research in nonmonotonic reasoning, and presents some results and ideas based on his research. The guiding principles are: clarification of the different research activities in the area, which have sometimes been undertaken independently of each other, and appreciation of the fact that these research activities often represent different means to the same ends, namely sound theoretical foundations and efficient computation. The book begins with a discussion of the various types of nonmonotonic reasoning, their applications and their logics. Theorem proving techniques for these logics are also described. There then follow chapters dealing with formulations of nonmonotonic inheritance, and nonmonotonic reasoning based on nonmonotonic rules. The final chapter discusses the achievements in the field in the light of the famous Yale shooting example. The book will be welcomed by researchers in theoretical computer science and artificial intelligence.
Del 12 - Cambridge Tracts in Theoretical Computer Science
Nonmonotonic Reasoning
Logical Foundations of Commonsense
AvGerhard Brewka
Inbunden, Engelska, 1991
988 kr
Skickas inom 10-15 vardagar
In this 1991 book the author gives a broad overview of different areas of research in nonmonotonic reasoning, and presents some results and ideas based on his research. The guiding principles are: clarification of the different research activities in the area, which have sometimes been undertaken independently of each other, and appreciation of the fact that these research activities often represent different means to the same ends, namely sound theoretical foundations and efficient computation. The book begins with a discussion of the various types of nonmonotonic reasoning, their applications and their logics. Theorem proving techniques for these logics are also described. There then follow chapters dealing with formulations of nonmonotonic inheritance, and nonmonotonic reasoning based on nonmonotonic rules. The final chapter discusses the achievements in the field in the light of the famous Yale shooting example. The book will be welcomed by researchers in theoretical computer science and artificial intelligence.
Del 15 - Cambridge Tracts in Theoretical Computer Science
Design Theory and Computer Science
AvSubrata Dasgupta
Inbunden, Engelska, 1991
2 217 kr
Skickas inom 10-15 vardagar
The logic and methodology of design is examined in this book from the perspective of computer science. Computers provide the context for this examination both by discussion of the design process for hardware and software systems and by consideration of the role of computers in design in general. The central question posed by the author is whether or not we can construct a theory of design. This book concentrates upon the relationship between design, mathematics and science and thus its audience must include designers and software designers as well as computer scientists.
Del 55 - Cambridge Tracts in Theoretical Computer Science
Term Rewriting Systems
AvTerese
Inbunden, Engelska, 2003
2 949 kr
Skickas inom 10-15 vardagar
Term rewriting systems developed out of mathematical logic and are an important part of theoretical computer science. They consist of sequences of discrete transformation steps where one term is replaced with another and have applications in many areas, from functional programming to automatic theorem proving and computer algebra. This 2003 book starts at an elementary level with the earlier chapters providing a foundation for the rest of the work. Much of the advanced material appeared here for the first time in book form. Subjects treated include orthogonality, termination, completion, lambda calculus, higher-order rewriting, infinitary rewriting and term graph rewriting. Many exercises are included with selected solutions provided on the web. A comprehensive bibliography makes this book ideal both for teaching and research. A chapter is included presenting applications of term rewriting systems, with many pointers to actual implementations.
Del 11 - Cambridge Tracts in Theoretical Computer Science
A Unifying Framework for Structured Analysis and Design Models
An Approach Using Initial Algebra Semantics and Category Theory
AvT. H. Tse
Inbunden, Engelska, 1991
1 609 kr
Skickas inom 10-15 vardagar
Structured methodologies are a popular and powerful tool in information systems development. Many different ones exist, each employing a number of models and so a specification must be converted from one form to another during the development process. To solve this problem, Dr Tse proposes in this 1991 book a unifying framework behind popular structured models. He approaches the problem from the viewpoints of algebra and category theory. He not only develops the frameworks but also illustrates their practical and theoretical usefulness. Thus this book will provide insight for software engineers into how methodologies can be formalised and will open up a range of applications and problems for theoretical computer scientists.
Del 21 - Cambridge Tracts in Theoretical Computer Science
The Clausal Theory of Types
AvD. A. Wolfram
Inbunden, Engelska, 1993
891 kr
Skickas inom 10-15 vardagar
Logic programming was based on first-order logic. Higher-order logics can also lead to theories of theorem-proving. This book introduces just such a theory, based on a lambda-calculus formulation of a clausal logic with equality, known as the Clausal Theory of Types. By restricting this logic to Horn clauses, a concise form of logic programming that incorporates functional programming is achieved. The book begins by reviewing the fundamental Skolem-Herbrand-Gödel Theorem and resolution, which are then extrapolated to a higher-order setting; this requires introducing higher-order equational unification which builds in higher-order equational theories and uses higher-order rewriting. The logic programming language derived has the unique property of being sound and complete with respect to Henkin-Andrews general models, and consequently of treating equivalent terms as identical. First published in 1993, the book can be used for graduate courses in theorem-proving, but will be of interest to all working in declarative programming.
Del 2 - Cambridge Tracts in Theoretical Computer Science
Logic and Computation
Interactive Proof with Cambridge LCF
AvLawrence C. Paulson,C. J. Van Rijsbergenm. fl.
Häftad, Engelska, 1990
745 kr
Skickas inom 10-15 vardagar
This book is concerned with techniques for formal theorem-proving, with particular reference to Cambridge LCF (Logic for Computable Functions). Cambridge LCF is a computer program for reasoning about computation. It combines the methods of mathematical logic with domain theory, the basis of the denotational approach to specifying the meaning of program statements. Cambridge LCF is based on an earlier theorem-proving system, Edinburgh LCF, which introduced a design that gives the user flexibility to use and extend the system. A goal of this book is to explain the design, which has been adopted in several other systems. The book consists of two parts. Part I outlines the mathematical preliminaries, elementary logic and domain theory, and explains them at an intuitive level, giving reference to more advanced reading; Part II provides sufficient detail to serve as a reference manual for Cambridge LCF. It will also be a useful guide for implementors of other programs based on the LCF approach.
Del 23 - Cambridge Tracts in Theoretical Computer Science
Nets, Terms and Formulas
Three Views of Concurrent Processes and their Relationship
AvE. -R. Olderog
Inbunden, Engelska, 1991
1 609 kr
Skickas inom 10-15 vardagar
The author presents a theory of concurrent processes where three different semantic description methods that are usually studied in isolation are brought together. Petri nets describe processes as concurrent and interacting machines; algebraic process terms describe processes as abstract concurrent processes; and logical formulas specify the intended communication behaviour of processes. At the heart of this theory are two sets of transformation rules for the top-down design of concurrent processes. The first set can be used to transform stepwise logical formulas into process terms, whilst process terms can be transformed into Petri nets by the second set. These rules are based on novel techniques for the operational and denotational semantics of concurrent processes. Various results and relationships between nets, terms and formulas starting with formulas and illustrated by examples. The use of transformations is demonstrated in a series of case studies, and the author also identifies directions for research.

Cambridge Tracts in Theoretical Computer Science – serie

Programs, Recursion and Unbounded Choice

Nets, Terms and Formulas

Two-Level Functional Languages

Extensions of First-Order Logic

Free Choice Petri Nets

The Logic of Typed Feature Structures

Deductive and Declarative Programming

The Uncertain Reasoner's Companion

Understanding Z

Basic Simple Type Theory

Domains and Lambda-Calculi

Mathematical Theory of Domains

Information Flow

Algebraic Specification of Communication Protocols

Data Refinement

Hybrid Graph Theory and Network Analysis

Lambda-calculus, Combinators and Functional Programming

Higher Order Logic and Hardware Verification

A Unifying Framework for Structured Analysis and Design Models

The Clausal Theory of Types

Design Theory and Computer Science

Concurrency Verification

Nonmonotonic Reasoning

Nonmonotonic Reasoning

Design Theory and Computer Science

Term Rewriting Systems

A Unifying Framework for Structured Analysis and Design Models

The Clausal Theory of Types

Logic and Computation

Nets, Terms and Formulas