The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering focus throughout, emphasizing techniques that will help users to build, understand, and maintain large Coq developments and minimize the cost of code change over time.
Engineering has been an essential collaborator in biological research and breakthroughs in biology are often enabled by technological advances. Decoding the double helix structure of DNA, for example, only became possible after significant advances in such technologies as X-ray diffraction and gel electrophoresis. Diagnosis and treatment of tuberculosis improved as new technologies—including the stethoscope, the microscope, and the X-ray—developed.
Climate engineering—which could slow the pace of global warming by injecting reflective particles into the upper atmosphere—has emerged in recent years as an extremely controversial technology. And for good reason: it carries unknown risks and it may undermine commitments to conserving energy. Some critics also view it as an immoral human breach of the natural world. The latter objection, David Keith argues in A Scientist’s Case for Climate Engineering, is groundless; we have been using technology to alter our environment for years.
Urbanization and globalization have shaped the last hundred years. These two dominant trends are mutually reinforcing: globalization links countries through the networked communications of urban hubs. The urban population now generates more than eighty percent of global GDP. Cities account for enormous flows of energy and materials—inflows of goods and services and outflows of waste. Thus urban environmental management critically affects global sustainability.
Human survival depends on a continuing supply of energy, but the need for ever-increasing amounts of it poses a dilemma: How can we find energy sources that are sustainable and ways to convert and utilize energy that are more efficient? This widely used textbook is designed for advanced undergraduate and graduate students as well as others who have an interest in exploring energy resource options and technologies with a view toward achieving sustainability on local, national, and global scales.
Sitting on the beach on a sunny summer day, we enjoy the steady advance and retreat of the waves. In the water, enthusiastic waders jump and shriek with pleasure when a wave hits them. But where do these waves come from? How are they formed and why do they break on the shore? In Waves, Fredric Raichlen traces the evolution of waves, from their generation in the deep ocean to their effects on the coast.
In Software Abstractions Daniel Jackson introduces an approach to software design that draws on traditional formal methods but exploits automated tools to find flaws as early as possible. This approach--which Jackson calls “lightweight formal methods” or “agile modeling”--takes from formal specification the idea of a precise and expressive notation based on a tiny core of simple and robust concepts but replaces conventional analysis based on theorem proving with a fully automated analysis that gives designers immediate feedback.
Much of the difficulty in creating information technology systems that truly meet people's needs lies in the problem of pinning down system requirements. This book offers a new approach to the requirements challenge, based on modeling and analyzing the relationships among stakeholders. Although the importance of the system-environment relationship has long been recognized in the requirements engineering field, most requirements modeling techniques express the relationship in mechanistic and behavioral terms.
This text offers a comprehensive treatment of VHDL and its applications to the design and simulation of real, industry-standard circuits. It focuses on the use of VHDL rather than solely on the language, showing why and how certain types of circuits are inferred from the language constructs and how any of the four simulation categories can be implemented. It makes a rigorous distinction between VHDL for synthesis and VHDL for simulation.
Color for the Sciences is the first book on colorimetry to offer an account that emphasizes conceptual and formal issues rather than applications. Jan Koenderink's introductory text treats colorimetry—literally, "color measurement"—as a science, freeing the topic from the usual fixation on conventional praxis and how to get the "right" result. Readers of Color for the Sciences will learn to rethink concepts from the roots in order to reach a broader, conceptual understanding.