18. TPHOLs 2005:
Oxford,
UK
Joe Hurd, Thomas F. Melham (Eds.):
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 BibTeX
Invited Papers
Regular Papers
- Hasan Amjad:
Shallow Lazy Proofs.
35-49
Electronic Edition (link) BibTeX
- 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
Electronic Edition (link) BibTeX
- Christoph Benzmüller, Chad E. Brown:
A Structured Set of Higher-Order Problems.
66-81
Electronic Edition (link) BibTeX
- Néstor Cataño:
Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS.
82-97
Electronic Edition (link) BibTeX
- Benjamin Grégoire, Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq.
98-113
Electronic Edition (link) BibTeX
- John Harrison:
A HOL Theory of Euclidean Space.
114-129
Electronic Edition (link) BibTeX
- Peter V. Homeier:
A Design Structure for Higher Order Quotients.
130-146
Electronic Edition (link) BibTeX
- Brian Huffman, John Matthews, Peter White:
Axiomatic Constructor Classes in Isabelle/HOLCF.
147-162
Electronic Edition (link) BibTeX
- Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J. Strother Moore, Eric Whitman Smith:
Meta Reasoning in ACL2.
163-178
Electronic Edition (link) BibTeX
- Claude Marché, Christine Paulin-Mohring:
Reasoning About Java Programs with Aliasing and Frame Conditions.
179-194
Electronic Edition (link) BibTeX
- César Muñoz, David Lester:
Real Number Calculations and Theorem Proving.
195-210
Electronic Edition (link) BibTeX
- David A. Naumann:
Verifying a Secure Information Flow Analyzer.
211-226
Electronic Edition (link) BibTeX
- Steven Obua:
Proving Bounds for Real Linear Programs in Isabelle/HOL.
227-244
Electronic Edition (link) BibTeX
- Russell O'Connor:
Essential Incompleteness of Arithmetic Verified by Coq.
245-260
Electronic Edition (link) BibTeX
- Veronika Ortner, Norbert Schirmer:
Verification of BDD Normalization.
261-277
Electronic Edition (link) BibTeX
- Nicolas Oury:
Extensionality in the Calculus of Constructions.
278-293
Electronic Edition (link) BibTeX
- Tom Ridge, James Margetson:
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.
294-309
Electronic Edition (link) BibTeX
- Julien Schmaltz, Dominique Borrione:
A Generic Network on Chip Model.
310-325
Electronic Edition (link) BibTeX
- Diana Toma, Dominique Borrione:
Formal Verification of a SHA-1 Circuit Core Using ACL2.
326-341
Electronic Edition (link) BibTeX
- Thomas Tuerk, Klaus Schneider:
From PSL to LTL: A Formal Validation in HOL.
342-357
Electronic Edition (link) BibTeX
Proof Pearls
Copyright © Sat May 16 23:43:57 2009
by Michael Ley (ley@uni-trier.de)
