The 14th International Conference on Theorem Proving in Higher Order Logics
3-6 September 2001, Edinburgh, Scotland
[Home Page][Conference History][Call for Papers][Guide for Authors][Programme]
[Related Events][How to Get There][Weather and Tourism][Registration][Accommodation]
[Sponsors][Student Bursaries][Proceedings][Photos][Business Meeting][TPHOLs 2002]
TPHOLs 2001 List of Presentations
Invited Speakers
- Bart Jacobs,
University of Nijmegen
- JavaCard Program Verification
- Steven D. Johnson,
Indiana University
- View from the Fringe of the Fringe
(Joint with CHARME 2001)
- Natarajan Shankar,
SRI International
- Using Decision Procedures with a Higher-Order Logic
Accepted Category A (Full Research) Papers
- Computer Algebra Meets Automated Theorem Proving: Integrating Maple and
PVS
- Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey,
Ursula Martin, and Sam Owre
- An Irrational Construction of R from Z
- Rob D. Arthan
- HELM and the Semantic Math-Web
- Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, and Irene Schena
- Calculational Reasoning Revisited (An Isabelle/Isar Experience)
- Gertrud Bauer and Markus Wenzel
- Mechanical Proofs about a Non-repudiation Protocol
- Giampaolo Bella and Lawrence C. Paulson
- Proving Hybrid Protocols Correct
- Mark Bickford, Christoph Kreitz, Robbert van Renesse, and Xiaoming Liu
- Nested General Recursion and Partiality in Type Theory
- Ana Bove and Venanzio Capretta
- A Higher-Order Calculus for Categories
- Mario Cáccamo and Glynn Winskel
- Certifying the Fast Fourier Transform with Coq
- Venanzio Capretta
- A Generic Library for Floating-Point Numbers and its Application to
Exact Computing
- Marc Daumas, Laurence Rideau, and Laurent Théry
- Ordinal Arithmetic: A Case Study for Rippling in a Higher Order
Domain
- Louise A. Dennis and Alan Smaill
- Abstraction and Refinement in Higher Order Logic
- Matt Fairtlough, Michael Mendler, and Xiaochun Cheng
- A Framework for the Formalisation of Pi Calculus Type Systems in
Isabelle/HOL
- Simon J. Gay
- Representing Hierarchical Automata in Interactive Theorem Provers
- Steffen Helke and Florian Kammüller
- Refinement Calculus for Logic Programming in Isabelle/HOL
- David Hemer, Ian Hayes, and Paul Strooper
- Predicate Subtyping with Predicate Sets
- Joe Hurd
- A Structural Embedding of Ocsid in PVS
- Pertti Kellomäki
- A Certified Polynomial-Based Decision Procedure for Propositional
Logic
- Inmaculada Medina-Bulo, Francisco Palomo-Lozano, and
José A. Alonso-Jiménez
- Finite Set Theory in ACL2
- J Strother Moore
- The HOL/NuPRL Proof Translator
(A Practical Approach to Formal Interoperability)
- Pavel Naumov, Mark-Oliver Stehr, and José Meseguer
- Formalizing Convex Hull Algorithms
- David Pichardie and Yves Bertot
- Experiments with Finite Tree Automata in Coq
- Xavier Rival and Jean Goubault-Larrecq
- Mizar Light for HOL Light
- Freek Wiedijk
Accepted Category B (Work-in-Progress) Papers
- Hierarchical Verification of the Implementation of the
IEEE-754 Table-Driven Floating-Point Exponential Function using HOL
- Amr T. Abdel-Hamid, Sofiène Tahar, and John Harrison
- BDD Representation Judgements in HOL: A Performance Evaluation
- Hasan Amjad
- Toward a Verified Generic Prooftool
- Pieter Audenaert
- Some Tools for Computer-Assisted Theorem Proving in
Martin-Löf Type Theory
- Marcin Benke
- A Lost Proof
- Christoph Benzmüller and Manfred Kerber
- Executing Higher Order Logic
- Stefan Berghofer and Tobias Nipkow
- Proving Type Soundness of a Simply Typed ML-Like Language
with References
- Olivier Boite and Catherine Dubois
- B vs. Coq to Prove a Garbage Collector
- L. Burdy
- Towards a Generic Tool for Reasoning about Labeled
Transition Systems
- Pierre Castéran and Davy Rouillard
- Transformational Reasoning with Incomplete Information
- O. Celiku and J. von Wright
- A User Model for Avoiding Design Induced Errors in Soft-Key
Interactive Systems
- Paul Curzon and Ann Blandford
- Constructing Isabelle Proofs in a Proof Refinement Calculus
- Christophe Depasse
- Representing Component States in Higher-Order Logic
- Sidi O. Ehmety and Lawrence C. Paulson
- Complex Quantifier Elimination in HOL
- John Harrison
- The Implementation of an Unusual Higher-Order Logic
- M. Randall Holmes
- Quotient Types
- Peter V. Homeier
- A Proof of the Church-Rosser Theorem for the Lambda Calculus
in Higher Order Logic
- Peter V. Homeier
- Verification of the Miller-Rabin Probabilistic Primality
Test
- Joe Hurd
- Formal Verification of a Theory of IEEE Rounding
- Christian Jacobi
- A PVS Theory of Symbolic Transition Systems
- Savi Maharaj
- A Comparison of Formalizations of the Meta-Theory of a
Language with Variable Bindings in Isabelle
- A. Momigliano, S. J. Ambler, and R. L. Crole
- Certification of Matrix Multiplication Algorithms:
Strassen's Algorithm in ACL2
- Francisco Palomo-Lozano, Inmaculada Medina-Bulo, and
José A. Alonso-Jiménez
- Quotients in the CIC
- Loïc Pottier
- Proof for Optimization: Programming Logic Support for Java
JIT Compilers
- Claire L. Quigley
- An Inductive Approach to Formalizing Notions of Number
Theory Proofs
- Thomas Marthedal Rasmussen
- Verifying that Invariants are Context-Inductive
- Vlad Rusu
- Tactics in Modern Proof-Assistants: The Bad Habit of
Overkilling
- Claudio Sacerdoti Coen
- Mechanizing in Higher-Order Logic Proofs of Correctness and
Completeness for a Set of RTL Transformations
- Elena Teica and Ranga Vemuri
- Proving Existential Theorems when Importing Results from MDG
to HOL
- Haiyan Xiong, Paul Curzon, Sofiène Tahar, and Ann Blandford
- Translating HOL to Specifications for the Model Checker SMV
- Dan Zhou and Paul E. Black