default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID18th TPHOLs 2005: Oxford, UK
- Joe Hurd, Thomas F. Melham:
Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings. Lecture Notes in Computer Science 3603, Springer 2005, ISBN 3-540-28372-2
Invited Papers
- Mauro Gargano, Mark A. Hillebrand, Dirk Leinenbach, Wolfgang J. Paul:
On the Correctness of Operating System Kernels. 1-16 - Andrew M. Pitts:
Alpha-Structural Recursion and Induction. 17-34
Regular Papers
- Hasan Amjad:
Shallow Lazy Proofs. 35-49 - Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell
, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic:
Mechanized Metatheory for the Masses: The PoplMark Challenge. 50-65 - Christoph Benzmüller, Chad E. Brown:
A Structured Set of Higher-Order Problems. 66-81 - Néstor Cataño:
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS. 82-97 - Benjamin Grégoire, Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq. 98-113 - John Harrison:
A HOL Theory of Euclidean Space. 114-129 - Peter V. Homeier:
A Design Structure for Higher Order Quotients. 130-146 - Brian Huffman, John Matthews, Peter White:
Axiomatic Constructor Classes in Isabelle/HOLCF. 147-162 - Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith:
Meta Reasoning in ACL2. 163-178 - Claude Marché, Christine Paulin-Mohring:
Reasoning About Java Programs with Aliasing and Frame Conditions. 179-194 - César A. Muñoz, David R. Lester:
Real Number Calculations and Theorem Proving. 195-210 - David A. Naumann:
Verifying a Secure Information Flow Analyzer. 211-226 - Steven Obua:
Proving Bounds for Real Linear Programs in Isabelle/HOL. 227-244 - Russell O'Connor:
Essential Incompleteness of Arithmetic Verified by Coq. 245-260 - Veronika Ortner, Norbert Schirmer:
Verification of BDD Normalization. 261-277 - Nicolas Oury:
Extensionality in the Calculus of Constructions. 278-293 - Tom Ridge, James Margetson:
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. 294-309 - Julien Schmaltz, Dominique Borrione:
A Generic Network on Chip Model. 310-325 - Diana Toma, Dominique Borrione:
Formal Verification of a SHA-1 Circuit Core Using ACL2. 326-341 - Thomas Tuerk, Klaus Schneider:
From PSL to LTL: A Formal Validation in HOL. 342-357
Proof Pearls
- Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo:
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2. 358-372 - J Strother Moore, Qiang Zhang:
Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2. 373-384 - Tobias Nipkow, Lawrence C. Paulson:
Proof Pearl: Defining Functions over Finite Sets. 385-396 - Michael Norrish, Konrad Slind:
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. 397-408
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-01-23 20:39 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:
