Email Gateway (Aug 17 2022 at 13:26): Email Gateway (Aug 17 2022 at 13:26):From: Joe Hurd <joe.hurd@gmail.com>
TPHOLs 2005 - FINAL CALL FOR PARTICIPATION
The 18th International Conference on
Theorem Proving in Higher Order Logics
Oxford, UK
Monday 22nd - Thursday 25th August 2005
************
* http://web.comlab.ox.ac.uk/TPHOLs2005/ * ************
The 2005 International Conference on Theorem Proving in Higher Order
Logics will be the eighteenth in a series that dates back to 1988.
The conference will be held Monday 22nd August through Thursday
25th August in central Oxford, UK.
REGISTRATION
Registration is now open. Please visit the TPHOLs 2005 web site,
http://web.comlab.ox.ac.uk/TPHOLs2005/, to register.
INVITED SPEAKERS
Wolfgang Paul, Universitat des Saarlandes
On the Correctness of Operating System Kernels
Andrew Pitts, University of Cambridge
Alpha-Structural Recursion and Induction
ACCOMMODATION
Information on accommodation is available on the TPHOLs 2005 web site.
RELATED EVENTS
On Friday 26 August, the day after TPHOLs 2005 finishes, the NETCA
Workshop on Verification and Theorem Proving for Continuous Systems
will take place in Oxford. Further information on the NETCA workshop
can be found at http://www.dcs.qmul.ac.uk/~pbo/NETCA-workshop.html
SPONSORS
TPHOLs 2005 is sponsored by the following organizations:
o Intel
o NETCA
o EPSRC
CONTACT
Enquiries concerning the conference should be emailed to
tphols2005@comlab.ox.ac.uk
OUTLINE PROGRAMME
Monday 22nd, Tuesday 23rd: Technical sessions.
Wednesday 24th: Technical sessions; excursion; conference dinner.
Thursday 25th: Technical sessions.
ACCEPTED REGULAR PAPERS
Shallow Lazy Proofs
Hasan Amjad
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
Nestor Catano
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
Cesar Munoz 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
ACCEPTED PROOF PEARLS
Proof Pearl: A Formal Proof of Higman's Lemma in ACL2
Francisco-Jesús Martín-Mateos, Jose-Antonio Alonso,
María-José Hidalgo and José-Luis Ruiz-Reina
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
Last updated: Nov 21 2024 at 12:39 UTC