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