Conferences in DBLP
Bart Jacobs JavaCard Program Verification. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:1-3 [Conf ] Steven D. Johnson View from the Fringe of the Fringe (Joint with CHARME 2001). [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:4- [Conf ] Natarajan Shankar Using Decision Procedures with a Higher-Order Logic. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:5-26 [Conf ] 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 ] R. D. Arthan An Irrational Construction of R from Z. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:43-58 [Conf ] 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 ] Gertrud Bauer , Markus Wenzel Calculational Reasoning Revisited (An Isabelle/Isar Experience). [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:75-90 [Conf ] Giampaolo Bella , Lawrence C. Paulson Mechanical Proofs about a Non-repudiation Protocol. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:91-104 [Conf ] 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 ] Ana Bove , Venanzio Capretta Nested General Recursion and Partiality in Type Theory. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:121-135 [Conf ] Mario Cáccamo , Glynn Winskel A Higher-Order Calculus for Categories. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:136-153 [Conf ] Venanzio Capretta Certifying the Fast Fourier Transform with Coq. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:154-168 [Conf ] 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 ] 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 ] Matt Fairtlough , Michael Mendler , Xiaochun Cheng Abstraction and Refinement in Higher Order Logic. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:201-216 [Conf ] 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 ] Steffen Helke , Florian Kammüller Representing Hierarchical Automata in Interactive Theorem Provers. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:233-248 [Conf ] 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 ] Joe Hurd Predicate Subtyping with Predicate Sets. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:265-280 [Conf ] Pertti Kellomäki A Structural Embedding of Ocsid in PVS. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:281-296 [Conf ] 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 ] J. Strother Moore Finite Set Theory in ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:313-328 [Conf ] 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 ] David Pichardie , Yves Bertot Formalizing Convex Hull Algorithms. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:346-361 [Conf ] Xavier Rival , Jean Goubault-Larrecq Experiments with Finite Tree Automata in Coq. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:362-377 [Conf ] Freek Wiedijk Mizar Light for HOL Light. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2001, pp:378-394 [Conf ]