TPHOLs 2005 Oxford, UK 22-25 August 2005 http://web.comlab.ox.ac.uk/TPHOLs2005/
	home conference history bid call for papers accepted papers
	advance program registration accommodation travel to oxford tphols 2006
	proceedings business meeting tphols 2007

Accepted Papers

Mature Work

Invited Talks

Alpha-Structural Recursion and Induction (Extended Abstract)
Andrew Pitts

Regular Papers

Mechanized Metatheory for the Masses: The PoplMark Challenge
Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich and Steve Zdancewic

A Structured Set of Higher-Order Problems
Christoph Benzmüller and Chad Brown

Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
Néstor Cataño

Proving Equalities in a Commutative Ring Done Right in Coq
Benjamin Grégoire and Assia Mahboubi

A HOL theory of Euclidean space
John Harrison

A Design Structure for Higher Order Quotients
Peter Homeier

Axiomatic Constructor Classes in Isabelle/HOLCF
Brian Huffman, John Matthews and Peter White

Meta Reasoning in ACL2
Warren Hunt, Matt Kaufmann, Robert Krug, J Moore and Eric Smith

Reasoning on Java programs with aliasing and frame conditions
Claude Marche and Christine Paulin-Mohring

Real Number Calculations and Theorem Proving
César Muñoz and David Lester

Verifying a Secure Information Flow Analyzer
David Naumann

Proving Bounds for Real Linear Programs in Isabelle/HOL
Steven Obua

Essential Incompleteness of Arithmetic Verified by Coq
Russell O'Connor

Verification of BDD Normalization
Veronika Ortner and Norbert Schirmer

Extensionality in the Calculus of Constructions
Nicolas Oury

A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Tom Ridge and James Margetson

A Generic Network on Chip Model
Julien Schmaltz and Dominique Borrione

Formal Verification of a SHA-1 Circuit Core using ACL2
Diana Toma and Dominique Borrione

From PSL to LTL: A Formal Validation in HOL
Thomas Türk and Klaus Schneider

Proof Pearls

Proof Pearl: Dijkstra's Shortest Path Algorithm Verified with ACL2
J Moore and Qiang Zhang

Proof Pearl: Defining Functions Over Finite Sets
Tobias Nipkow and Lawrence Paulson

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof
Michael Norrish and Konrad Slind

Emerging Trends

Quantitative Temporal Logic mechanized in HOL
Orieta Celiku

Embedding a fair CCS in Isabelle/HOL
Michael Compton

What can be Learned from Failed Proofs of Non-Theorems?
Louise A. Dennis and Pablo Nogueira

A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic
Mike Gordon, Juliano Iyoda, Scott Owens and Konrad Slind

A PVS Implementation of Stream Calculus for Signal Flow Graphs
Hanne Gottliebsen

Formal Verification of Chess Endgame Databases
Joe Hurd

Exploring New OO-Paradigms with HOL: Aspects and Collaborations
Florian Kammuller

Formalization of Hensel's Lemma
Hidetune Kobayashi, Hideo Suzuki and Yoko Ono

Tactic-based Optimized Compilation of Functional Programs
Thomas Meyer and Burkhart Wolff

Optimizing Proof for Replay
Malcolm Newey, Aditi Barthwal, Michael Norrish

A HOL implementation of the ARM FP Co-processor programmer's model
James Reynolds

Teaching a HOL Course: Experience Report
Konrad Slind, Steven Barrus, Seungkeol Choe, Chris Condrat, Jianjun Duan, Sivaram Gopalakrishnan, Aaron Knoll, Hiro Kuwahara, Guodong Li, Scott Little, Lei Liu, Steanie Moore, Robert Palmer, Claurissa Tuttle, Sean Walton, Yu Yang and Junxing Zhang

Using a SAT Solver as a Fast Decision Procedure for Propositional Logic in an LCF-style Theorem Prover
Tjark Weber

Liveness Proof of an Elevator Control System
Huabing Yang, Xingyuan Zhang and Yuanyuan Wang

Verification of Euclid's Algorithm for Finding Multiplicative Inverses
Junxing Zhang and Konrad Slind

Liveness Reasoning for Inductive Protocol Verification
Xingyuan Zhang, Huabing Yang and Yuanyuan Wang