This monograph details several important advances in the area known
as the proofs-as-programs paradigm, a set of approaches to
developing programs from proofs in constructive logic. It serves
the dual purpose of providing a state-of-the-art overview of the
field and detailing tools and techniques to stimulate further
research.
One of the booka (TM)s central themes is a general, abstract
framework for developing new systems of program synthesis by
adapting proofs-as-programs to new contexts, which the authors call
the Curry--Howard Protocol. This protocol is used to provide two
novel applications for industrial-scale, complex software
engineering: contractual imperative program synthesis and
structured software synthesis. These applications constitute an
exemplary justification for the applicability of the protocol to
different contexts.
The book is intended for graduate students in computer science
or mathematics who wish to extend their background in logic and
type theory as well as gain experience working with logical
frameworks and practical proof systems. In addition, the
proofs-as-programs research community, and the wider computational
logic, formal methods and software engineering communities will
benefit. The applications given in the book should be of interest
for researchers working in the target problem domains.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!