Conferences in DBLP

International Conference on Theorem Proving in Higher Order Logics (tphol)
2000 (conf/tphol/2000)

1. Antonia Balaa, Yves Bertot
   Fix-Point Equations for Well-Founded Recursion in Type Theory. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:1-16 [Conf]
   
2. Bruno Barras
   Programming and Computing in HOL. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:17-37 [Conf]
   
3. Stefan Berghofer, Tobias Nipkow
   Proof Terms for Simply Typed Higher Order Logic. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:38-52 [Conf]
   
4. Karthikeyan Bhargavan, Carl A. Gunter, Davor Obradovic
   Routing Information Protocol in HOL/SPIN. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:53-72 [Conf]
   
5. Venanzio Capretta
   Recursive Families of Inductive Types. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:73-89 [Conf]
   
6. Victor Carreño, César Muñoz
   Aircraft Trajectory Modeling and Altering Algorithm Verification. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:90-105 [Conf]
   
7. Robert P. Colwell, Bob Brennan
   Intel's Formal Verification Experience on the Willamette Development. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:106-107 [Conf]
   
8. Ewen Denney
   A Prototype Proof Translator from HOL to Coq. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:108-125 [Conf]
   
9. Catherine Dubois
   Proving ML Type Soundness Within Coq. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2000, pp:126-144 [Conf]
   
10. Jacques D. Fleuriot
    On the Mechanization of Real Analysis in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:145-161 [Conf]
    
11. Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
    Equational Reasoning via Partial Reflection. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:162-178 [Conf]
    
12. Michael J. C. Gordon
    Reachability Programming in HOL98 Using BDDs. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:179-196 [Conf]
    
13. Hanne Gottliebsen
    Transcendental Functions and Continuity Checking in PVS. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:197-214 [Conf]
    
14. Jim Grundy
    Verified Optimizations for the Intel IA-64 Architecture. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:215-232 [Conf]
    
15. John Harrison
    Formal Verification of IA-64 Division Algorithms. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:233-251 [Conf]
    
16. Jason Hickey, Aleksey Nogin
    Fast Tactic-Based Theorem Proving. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:252-267 [Conf]
    
17. Martin Hofmann, Francis Tang
    Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:268-282 [Conf]
    
18. M. Randall Holmes
    A Strong and Mechanizable Grand Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:283-300 [Conf]
    
19. Marieke Huisman, Bart Jacobs
    Inheritance in Higher Order Logic: Modeling and Reasoning. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:301-319 [Conf]
    
20. Paul B. Jackson
    Total-Correctness Refinement for Sequential Reactive Systems. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:320-337 [Conf]
    
21. Roope Kaivola, Mark Aagaard
    Divider Circuit Verification with Model Checking and Theorem Proving. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:338-355 [Conf]
    
22. Mickaël Kerboeuf, David Nowak, Jean-Pierre Talpin
    Specification and Verification of a Steam-Boiler with Signal-Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:356-371 [Conf]
    
23. Linas Laibinis, Joakim von Wright
    Functional Procedures in Higher-Order Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:372-387 [Conf]
    
24. Pierre Letouzey, Laurent Théry
    Formalizing Stålmarck's Algorithm in Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:388-405 [Conf]
    
25. Christoph Lüth, Burkhart Wolff
    TAS - A Generic Window Inference System. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:406-423 [Conf]
    
26. Stephan Merz
    Weak Alternating Automata in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:424-441 [Conf]
    
27. Robin Milner
    Graphical Theories of Interactive Systems: Can a Proof Assistant Help? [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:442- [Conf]
    
28. Abdel Mokkedem, Tim Leonard
    Formal Verification of the Alpha 21364 Network Protocol. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:443-461 [Conf]
    
29. Robert Pollack
    Dependently Typed Records for Representing Mathematical Structure. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:462-479 [Conf]
    
30. Bernhard Reus, Tatjana Hein
    Towards a Machine-Checked Java Specification Book. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:480-497 [Conf]
    
31. Konrad Slind
    Another Look at Nested Recursion. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:498-518 [Conf]
    
32. Larry Wos, Branden Fitelson
    Automating the Search for Answers to Open Questions. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:519-525 [Conf]
    
33. Larry Wos
    Appendix: Conjectures Concerning Proof, Design, and Verification. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2000, pp:526-533 [Conf]