Essays in Honour of Gilles Kahn
Gäller alla köp över 299 kr, t.o.m. 7 juni. Villkor
De som köpt den här boken har ofta också köpt Tomorrow, And Tomorrow, And Tomorrow av Gabrielle Zevin (häftad).Köp båda 2 för 1714 kr
A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.
Yves Bertot is a Senior Researcher and Project Leader at the French National Institute for Research in Computer Science and Control (INRIA), Sophia Antipolis. Born in 1964, he received his Ph.D. from the University of Nice in 1991 and is co-author (with Pierre Castran) of Coq'Art: The Calculus of Inductive Constructions (2004). Grard Huet is a Director of Research at the French National Institute for Research in Computer Science and Control (INRIA), Rocquencourt. Jean-Jacques Lvy is a Director of Research at the French National Institute for Research in Computer Science and Control (INRIA), Rocquencourt. Gordon Plotkin is a Professor in the School of Informatics at the University of Edinburgh.
Preface; List of contributors; 1. Determinacy in a synchronous -calculus Roberto Amadio and Mehdi Dogguy; 2. Classical coordination mechanisms in the chemical model Jean-Pierre Bantre, Pascal Fradet and Yann Radenac; 3. Sequential algorithms as bistable maps Pierre-Louis Curien; 4. The semantics of dataflow with firing Edward A. Lee and Eleftherios Matsikoudis; 5. Kahn networks at the dawn of functional programming David B. MacQueen; 6. A simple type-theoretic language: mini-TT Thierry Coquand, Yoshiki Kinoshita, Bengt Nordstrm, and Makoto Takeyama; 7. Program semantics and infinite regular terms Bruno Courcelle; 8. Algorithms for equivalence and reduction to minimal form for a class of simple recursive equations Bruno Courcelle, Gilles Kahn, and Jean Vuillemin; 9. Generalized finite developments Jean-Jacques Lvy; 10. Semantics of program representation graphs G. Ramalingam and Thomas Reps; 11. Tribute to a great meta-technologist - from centaur to the meta-environment Paul Klint; 12. Towards a theory of document structure Bengt Nordstrm; 13. Grammars as software libraries Aarne Ranta; 14. The Leordo computation system Erik Sandewall; 15. Theorem proving support in programming language semantics Yves Bertot; 16. Nominal verification of algorithm W Christian Urban and Tobias Nipkow; 17. A constructive denotational semantics for Kahn networks in Coq Christine Paulin-Mohring; 18. Asclepios: a research project-team at INRIA for the analysis and simulation of biomedical images Nicholas Ayache, Olivier Clatz, Herv Delingette, Grgoire Malandain, Xavier Pennec and Maxime Sermesant; 19. Proxy caching in split TCP: dynamics, stability and tail asymptotics Franois Baccelli, Giovanna Carofiglio, and Serguei Foss; 20. Two-by-two static, evolutionary, and dynamic games Pierre Bernhard and Frdric Hamelin; 21. Reversal strategies for adjoint algorithms Laurent Hascot; 22. Reflections on INRIA and the role of Gilles Kahn Alain Bensoussan; 23. Can a systems biologist fix a tamagotchi? Luca Cardelli; 24. Computational science: a new frontier for computing Andrew Herbert; 25. The descendants of centaur: a personal view on Gilles Kahn's work Emmanuel Ledinot; 26. The tower of informatic models Robin Milner.