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. Springer 2005 Lecture Notes in Computer Science 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
- 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
- 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
- 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
- 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
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
- Michael Norrish, Konrad Slind: Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. 397-408
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-18T211851 by the dblp team