Conferences in DBLP
Behzad Akbarpour , Sofiène Tahar Error Analysis of Digital Filters Using Theorem Proving. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:1-17 [Conf ] Penny Anderson , Frank Pfenning Verifying Uniqueness in a Logical Framework. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:18-33 [Conf ] David Aspinall , Lennart Beringer , Martin Hofmann , Hans-Wolfgang Loidl , Alberto Momigliano A Program Logic for Resource Verification. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:34-49 [Conf ] Olivier Boite Proof Reuse with Extended Inductive Types. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:50-65 [Conf ] Luís Cruz-Filipe , Freek Wiedijk Hierarchical Reflection. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:66-81 [Conf ] Al Davis Correct Embedded Computing Futures. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:82- [Conf ] Lucas Dixon , Jacques D. Fleuriot Higher Order Rippling in IsaPlanner. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:83-98 [Conf ] Ruben Gamboa , John Cowles A Mechanical Proof of the Cook-Levin Theorem. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:99-116 [Conf ] Thomas C. Hales Formalizing the Proof of the Kepler Conjecture. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:117- [Conf ] Nadeem Abdul Hamid , Zhong Shao Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:118-135 [Conf ] Jason Hickey , Aleksey Nogin Extensible Hierarchical Tactic Construction in a Logical Framework. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:136-151 [Conf ] Einar Broch Johnsen , Christoph Lüth Theorem Reuse by Proof Term Transformation. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:152-167 [Conf ] Michael Jones , Aaron Benson , Dan Delorey Proving Compatibility Using Refinement. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:168-183 [Conf ] Hanbing Liu , J. Strother Moore Java Program Verification via a JVM Deep Embedding in ACL2. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:184-200 [Conf ] John Longley , Randy Pollack Reasoning About CBV Functional Programs in Isabelle/HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:201-216 [Conf ] Jean-François Monin Proof Pearl: From Concrete to Functional Unparsing. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:217-224 [Conf ] Julien Narboux A Decision Procedure for Geometry in Coq. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:225-240 [Conf ] Michael Norrish Recursive Function Definition for Types with Binders. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:241-256 [Conf ] Lee Pike , Jeffrey Maddalon , Paul S. Miner , Alfons Geser Abstractions for Fault-Tolerant Distributed System Verification. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:257-270 [Conf ] Stefan Richter Formalizing Integration Theory with an Application to Probabilistic Algorithms. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:271-286 [Conf ] Tian-jun Zuo , Jun-gang Han , Ping Chen Formalizing Java Dynamic Loading in HOL. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:287-304 [Conf ] Martin Wildmoser , Tobias Nipkow Certifying Machine Code Safety: Shallow Versus Deep Embedding. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:305-320 [Conf ] Ting Zhang , Henny B. Sipma , Zohar Manna Term Algebras with Length Function and Bounded Quantifier Alternation. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:321-336 [Conf ]