14. TPHOLs 2001:
Edinburgh, Scotland, UK
Richard J. Boulton, Paul B. Jackson (Eds.):
Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings.
Lecture Notes in Computer Science 2152 Springer 2001, ISBN 3-540-42525-X 
Invited Talks
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
Last update Sat May 18 19:51:45 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
