The SCEAS System
Navigation Menu

Conferences in DBLP

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

  1. Bart Jacobs
    JavaCard Program Verification. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:1-3 [Conf]
  2. Steven D. Johnson
    View from the Fringe of the Fringe (Joint with CHARME 2001). [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:4- [Conf]
  3. Natarajan Shankar
    Using Decision Procedures with a Higher-Order Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:5-26 [Conf]
  4. Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre
    Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:27-42 [Conf]
  5. R. D. Arthan
    An Irrational Construction of R from Z. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:43-58 [Conf]
  6. Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena
    HELM and the Semantic Math-Web. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:59-74 [Conf]
  7. Gertrud Bauer, Markus Wenzel
    Calculational Reasoning Revisited (An Isabelle/Isar Experience). [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:75-90 [Conf]
  8. Giampaolo Bella, Lawrence C. Paulson
    Mechanical Proofs about a Non-repudiation Protocol. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:91-104 [Conf]
  9. Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003
    Proving Hybrid Protocols Correct. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:105-120 [Conf]
  10. Ana Bove, Venanzio Capretta
    Nested General Recursion and Partiality in Type Theory. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:121-135 [Conf]
  11. Mario Cáccamo, Glynn Winskel
    A Higher-Order Calculus for Categories. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:136-153 [Conf]
  12. Venanzio Capretta
    Certifying the Fast Fourier Transform with Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:154-168 [Conf]
  13. Marc Daumas, Laurence Rideau, Laurent Théry
    A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:169-184 [Conf]
  14. Louise A. Dennis, Alan Smaill
    Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:185-200 [Conf]
  15. Matt Fairtlough, Michael Mendler, Xiaochun Cheng
    Abstraction and Refinement in Higher Order Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:201-216 [Conf]
  16. Simon J. Gay
    A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:217-232 [Conf]
  17. Steffen Helke, Florian Kammüller
    Representing Hierarchical Automata in Interactive Theorem Provers. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:233-248 [Conf]
  18. David Hemer, Ian J. Hayes, Paul A. Strooper
    Refinement Calculus for Logic Programming in Isabelle/HOL. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:249-264 [Conf]
  19. Joe Hurd
    Predicate Subtyping with Predicate Sets. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:265-280 [Conf]
  20. Pertti Kellomäki
    A Structural Embedding of Ocsid in PVS. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:281-296 [Conf]
  21. Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez
    A Certified Polynomial-Based Decision Procedure for Propositional Logic. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:297-312 [Conf]
  22. J. Strother Moore
    Finite Set Theory in ACL2. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:313-328 [Conf]
  23. Pavel Naumov, Mark-Oliver Stehr, José Meseguer
    The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:329-345 [Conf]
  24. David Pichardie, Yves Bertot
    Formalizing Convex Hull Algorithms. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:346-361 [Conf]
  25. Xavier Rival, Jean Goubault-Larrecq
    Experiments with Finite Tree Automata in Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:362-377 [Conf]
  26. Freek Wiedijk
    Mizar Light for HOL Light. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2001, pp:378-394 [Conf]
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002