TPHOLs 2007 Proceedings

Category A: Full Research Papers

TPHOLs 2007 proceedings are published as Volume 4732 of Springer-Verlag's Lecture Notes in Computer Science. You can access all papers online through the SpringerLink website. Titles and abstracts are also listed here.

Category B: Emerging Trends

TPHOLs 2007 Emerging trends proceedings are published as Internal Report 364/07 of the Department of Computer Science of the University of Kaiserslautern, which is available through its open access platform. You can also download all papers here:

0. Preface and Table of Contents.
1. Sa'ed Abed, Otmane Ait Mohammed, Ghiath Al Sammane. A High Level Reachability Analysis using Multiway Decision Graph in the HOL Theorem Prover.
2. Hasan Amjad. Propositional Simplification With BDDs and SAT Solvers.
3. Christoph Benzmueller. Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic.
4. Achim D. Bruckner, Burkhart Wolff. Extensible Object-Oriented Data Models in Isabelle/HOL.
5. Pierre Corbineau. A Declarative Language for the Coq Proof Assistant.
6. Jeremy Dawson. Isabelle Theories for Machine Words.
7. Holger Gast. An Architecture for Extensible Click'n Prove Interfaces.
8. Hanne Gottliebsen. Coinductive Proofs for Streams in PVS.
9. Florian Haftmann, Tobias Nipkow. A Code Generator Framework for Isabelle/HOL.
10. Florian Kammueller. CSP Revisited.
11. Stephane Le Roux. Acyclicity and Finite Linear Extendability: a Formal and Constructive Equivalence.
12. Magnus Myreen, Michael Gordon. Verification of Machine Code Implementations of Arithmetic Functions for Cryptography.
13. Paolo Torrini, Christoph Lueth, Christian Maeder, Till Mossakowski. Translating Haskell to Isabelle.
14. Jinshuang Wang, Xingyuan Zhang, Yusen Zhang, Huabing Yang. A Probabilistic Model for Parametric Fairness in Isabelle/HOL.
15. Stephen Westfold. Integrating Isabelle/HOL with Specware.
16. Author Index.

Bibliographical Information

@techreport{tphols2007b,
  title = {Theorem Proving in Higher Order Logics: Emerging Trends Proceedings},
  editor = {Klaus Schneider and Jens Brandt},
  month = 08,
  year = 2007,
  institution = {Department of Computer Science, University of Kaiserslautern},
  number = {364/07}
}