内容

目次

Eliminating the Chaff—Again: Banquet Speech at Marktoberdorf 1996.- Envoi at Marktoberdorf 1996.- 0. Designing Proofs and Programs.- Heuristics for a Very Simple Euclidean Proof (EWD1180).- Complete DAGs (EWD1204).- A Result of Rabbit Removal (EWD1208).- For the Record: Painting the Squared Plane (EWD1212).- The Marriage Agency (EWD1214).- Courtesy Dr. Birgit Schieder (EWD1215).- WLOG, or the Misery of the Unordered Pair (EWD1223).- My Simplest Theorem (EWD1232).- The Transitive Closure of a Wellfounded Relation (EWD1241).- The Formula for sin. (a + /?) (EWD1244a).- A Kind of Converse of Leibniz’s Principle (EWD1245).- The Strengths of the Academic Enterprise (EWD1175).- On a Method for the Formal Design of Multiprograms.- Foundations for Calculational Logic.- 1. Examples of Protocol Design.- Specification and Design of a Transmission Protocol by Successive Refinements Using B.- Formal Derivation of a Protocol in CSP.- 2. Languages and Models for Program Design.- Genesis of Algorithmic Languages.- Mathematical Methods in System and Software Engineering.- Unified Theories of Programming.- 3. Programming Paradigms.- On the Relationship Between Classes, Objects and Data Abstraction.- The Oz Programming Model.- A Foundation for Higher-order Concurrent Constraint Programming.- 4. Mechanical Proof Assistance.- Tool Support for Logics of Programs.- Machine-Assisted Verification Using Theorem Proving and Model Checking.