default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID14th TPHOLs 2001: Edinburgh, Scotland, UK
- Richard J. Boulton, Paul B. Jackson:
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
- 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 W. 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
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-23 19:40 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
