14. TPHOLs 2001: Edinburgh, Scotland, UK

@proceedings{DBLP:conf/tphol/2001,
  editor    = {Richard J. Boulton and
               Paul B. Jackson},
  title     = {Theorem Proving in Higher Order Logics, 14th International Conference,
               TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2152},
  year      = {2001},
  isbn      = {3-540-42525-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Invited Talks

• Bart Jacobs:
  JavaCard Program Verification. 1-3
  Electronic Edition (Springer LINK) BibTeX
• Steven D. Johnson:
  View from the Fringe of the Fringe (Joint with CHARME 2001). 4
  Electronic Edition (Springer LINK) BibTeX
• Natarajan Shankar:
  Using Decision Procedures with a Higher-Order Logic. 5-26
  Electronic Edition (Springer LINK) BibTeX

Regular Contributions

• Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre:
  Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. 27-42
  Electronic Edition (Springer LINK) BibTeX
• R. D. Arthan:
  An Irrational Construction of R from Z. 43-58
  Electronic Edition (Springer LINK) BibTeX
• Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena:
  HELM and the Semantic Math-Web. 59-74
  Electronic Edition (Springer LINK) BibTeX
• Gertrud Bauer, Markus Wenzel:
  Calculational Reasoning Revisited (An Isabelle/Isar Experience). 75-90
  Electronic Edition (Springer LINK) BibTeX
• Giampaolo Bella, Lawrence C. Paulson:
  Mechanical Proofs about a Non-repudiation Protocol. 91-104
  Electronic Edition (Springer LINK) BibTeX
• Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu:
  Proving Hybrid Protocols Correct. 105-120
  Electronic Edition (Springer LINK) BibTeX
• Ana Bove, Venanzio Capretta:
  Nested General Recursion and Partiality in Type Theory. 121-135
  Electronic Edition (Springer LINK) BibTeX
• Mario Cáccamo, Glynn Winskel:
  A Higher-Order Calculus for Categories. 136-153
  Electronic Edition (Springer LINK) BibTeX
• Venanzio Capretta:
  Certifying the Fast Fourier Transform with Coq. 154-168
  Electronic Edition (Springer LINK) BibTeX
• Marc Daumas, Laurence Rideau, Laurent Théry:
  A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. 169-184
  Electronic Edition (Springer LINK) BibTeX
• Louise A. Dennis, Alan Smaill:
  Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. 185-200
  Electronic Edition (Springer LINK) BibTeX
• Matt Fairtlough, Michael Mendler, Xiaochun Cheng:
  Abstraction and Refinement in Higher Order Logic. 201-216
  Electronic Edition (Springer LINK) BibTeX
• Simon J. Gay:
  A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. 217-232
  Electronic Edition (Springer LINK) BibTeX
• Steffen Helke, Florian Kammüller:
  Representing Hierarchical Automata in Interactive Theorem Provers. 233-248
  Electronic Edition (Springer LINK) BibTeX
• David Hemer, Ian J. Hayes, Paul A. Strooper:
  Refinement Calculus for Logic Programming in Isabelle/HOL. 249-264
  Electronic Edition (Springer LINK) BibTeX
• Joe Hurd:
  Predicate Subtyping with Predicate Sets. 265-280
  Electronic Edition (Springer LINK) BibTeX
• Pertti Kellomäki:
  A Structural Embedding of Ocsid in PVS. 281-296
  Electronic Edition (Springer LINK) BibTeX
• Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez:
  A Certified Polynomial-Based Decision Procedure for Propositional Logic. 297-312
  Electronic Edition (Springer LINK) BibTeX
• J. Strother Moore:
  Finite Set Theory in ACL2. 313-328
  Electronic Edition (Springer LINK) BibTeX
• Pavel Naumov, Mark-Oliver Stehr, José Meseguer:
  The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). 329-345
  Electronic Edition (Springer LINK) BibTeX
• David Pichardie, Yves Bertot:
  Formalizing Convex Hull Algorithms. 346-361
  Electronic Edition (Springer LINK) BibTeX
• Xavier Rival, Jean Goubault-Larrecq:
  Experiments with Finite Tree Automata in Coq. 362-377
  Electronic Edition (Springer LINK) BibTeX
• Freek Wiedijk:
  Mizar Light for HOL Light. 378-394
  Electronic Edition (Springer LINK) BibTeX