14. TPHOLs 2001: Edinburgh, Scotland, UK

Invited Talks

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

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