default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID13th TPHOLs 2000: Portland, Oregon, USA
- Mark D. Aagaard, John Harrison:
Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings. Lecture Notes in Computer Science 1869, Springer 2000, ISBN 3-540-67863-8 - Antonia Balaa, Yves Bertot:
Fix-Point Equations for Well-Founded Recursion in Type Theory. 1-16 - Bruno Barras:
Programming and Computing in HOL. 17-37 - Stefan Berghofer, Tobias Nipkow:
Proof Terms for Simply Typed Higher Order Logic. 38-52 - 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 - Herman Geuvers, Freek Wiedijk, Jan Zwanenburg:
Equational Reasoning via Partial Reflection. 162-178 - 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 - Jason Hickey, Aleksey Nogin:
Fast Tactic-Based Theorem Proving. 252-267 - 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 - Marieke Huisman, Bart Jacobs:
Inheritance in Higher Order Logic: Modeling and Reasoning. 301-319 - Paul B. Jackson:
Total-Correctness Refinement for Sequential Reactive Systems. 320-337 - Roope Kaivola, Mark D. 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 - Linas Laibinis, Joakim von Wright:
Functional Procedures in Higher-Order Logic. 372-387 - Pierre Letouzey, Laurent Théry:
Formalizing Stålmarck's Algorithm in Coq. 388-405 - Christoph Lüth, Burkhart Wolff:
TAS - A Generic Window Inference System. 406-423 - Stephan Merz:
Weak Alternating Automata in Isabelle/HOL. 424-441 - Robin Milner:
Graphical Theories of Interactive Systems: Can a Proof Assistant Help? 442 - Abdel Mokkedem, Tim Leonard:
Formal Verification of the Alpha 21364 Network Protocol. 443-461 - Robert Pollack:
Dependently Typed Records for Representing Mathematical Structure. 462-479 - Bernhard Reus, Tatjana Hein:
Towards a Machine-Checked Java Specification Book. 480-497 - Konrad Slind:
Another Look at Nested Recursion. 498-518 - Larry Wos, Branden Fitelson:
Automating the Search for Answers to Open Questions. 519-525 - Larry Wos:
Appendix: Conjectures Concerning Proof, Design, and Verification. 526-533
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-28 12:42 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
