13. TPHOLs 2000: Portland, Oregon, USA
Mark Aagaard, John Harrison (Eds.): Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Springer 2000 Lecture Notes in Computer Science ISBN 3-540-67863-8- Bruno Barras: Programming and Computing in HOL. 17-37
- Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic: Routing Information Protocol in HOL/SPIN. 53-72
- Venanzio Capretta: Recursive Families of Inductive Types. 73-89
- Victor Carreño, César A. Muñoz: Aircraft Trajectory Modeling and Altering Algorithm Verification. 90-105
- Robert P. Colwell, Bob Brennan: Intel's Formal Verification Experience on the Willamette Development. 106-107
- Ewen Denney: A Prototype Proof Translator from HOL to Coq. 108-125
- Catherine Dubois: Proving ML Type Soundness Within Coq. 126-144
- Jacques D. Fleuriot: On the Mechanization of Real Analysis in Isabelle/HOL. 145-161
- Michael J. C. Gordon: Reachability Programming in HOL98 Using BDDs. 179-196
- Hanne Gottliebsen: Transcendental Functions and Continuity Checking in PVS. 197-214
- Jim Grundy: Verified Optimizations for the Intel IA-64 Architecture. 215-232
- John Harrison: Formal Verification of IA-64 Division Algorithms. 233-251
- Martin Hofmann, Francis Tang: Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. 268-282
- M. Randall Holmes: A Strong and Mechanizable Grand Logic. 283-300
- Paul B. Jackson: Total-Correctness Refinement for Sequential Reactive Systems. 320-337
- Roope Kaivola, Mark Aagaard: Divider Circuit Verification with Model Checking and Theorem Proving. 338-355
- Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin: Specification and Verification of a Steam-Boiler with Signal-Coq. 356-371
- Stephan Merz: Weak Alternating Automata in Isabelle/HOL. 424-441
- Robin Milner: Graphical Theories of Interactive Systems: Can a Proof Assistant Help? 442
- Robert Pollack: Dependently Typed Records for Representing Mathematical Structure. 462-479
- Konrad Slind: Another Look at Nested Recursion. 498-518
- Larry Wos: Appendix: Conjectures Concerning Proof, Design, and Verification. 526-533
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-17T203624 by the dblp team