Email Gateway (Aug 18 2022 at 10:35): Email Gateway (Aug 18 2022 at 10:35):From: Klaus Schneider <Klaus.Schneider@informatik.uni-kl.de>
========================
Call for Participation
========================
International Conference on Theorem Proving in Higher Order Logics
Kaiserslautern, Germany, September 10-13, 2007
http://rsg.informatik.uni-kl.de/TPHOLs-2007
TPHOLs 2007 is the twentieth international conference on theorem proving
in higher order logics. Topics presented at TPHOLs conferences typically
cover all aspects of theorem proving in higher order logics, all kinds of
applications of interactive theorem provers of higher order logics like
specification and verification of hardware and software systems or
reasoning about the semantics of different kinds of languages.
The conference programme consists of 26 regular presentations and several
work-in-progress presentations. We are proud to further present three
invited talks given by Constance L. Heitmeyer (Naval Research Laboratory,
Washington, DC, USA), Xavier Leroy (INRIA, Paris-Rocquencourt, France),
and Peter Liggesmeyer (Fraunhofer IESE, Kaiserslautern, Germany).
Moreover, the first workshop on formal verification of adaptive systems
(VerAS) is co-lated with TPHOLs and is held on September 14, 2007.
The conference takes place at the Fraunhofer Centre Kaiserslautern,
home of the Fraunhofer IESE and ITWM.
Registration for the conference should be done as described on the TPHOLs
web pages http://rsg.informatik.uni-kl.de/TPHOLs-2007/registration.html
until July 27th, 2007 (early registration).
Links:
* regular presentations at the conference:
http://rsg.informatik.uni-kl.de/TPHOLs-2007/papers.html
* registration information
http://rsg.informatik.uni-kl.de/TPHOLs-2007/registration.html
------------------------
Conference Programme
------------------------
Invited Talks:
* Constance L. Heitmeyer:
On the Utility of Formal Methods in the Development and
Certification of Software
* Xavier Leroy:
Formal Verification of an Optimizing Compiler
* Peter Liggesmeyer:
Formal Techniques in Software Engineering: Correct Software
and Safe Systems
Regular Talks:
* A formally verified prover for the ALC description logic
(María-José Hidalgo, José-Antonio Alonso, Joaquín Borrego-Díaz,
Francisco-Jesus Martin-Mateos and José-Luis Ruiz-Reina)
* Proof Pearl: Looping around the Orbit
(Steven Obua)
* Finding Lexicographic Orders for Termination Proofs in
Isabelle/HOL
(Lukas Bulwahn, Alexander Krauss and Tobias Nipkow)
* Separation Locic for Small-step Cminor
(Andrew Appel and Sandrine Blazy)
* A monad-based modeling and verification toolbox with application
to security protocols
(Christoph Sprenger and David Basin)
* Verified Decision Procedures on Context-Free Grammars
(Yasuhiko Minamide)
* Source-Level Proof Reconstruction for Interactive Theorem Proving
(Lawrence Paulson and Kong Woei Susanto)
* Proof Pearl: The power of higher-order encodings in the logical
framework LF
(Brigitte Pientka)
* Formalising Generalised Substitutions
(Jeremy Dawson)
* Proof Pearl: de Bruijn terms really do work
(Michael Norrish and Rene Vestergaard)
* Mizar's Soft Type System
(Freek Wiedijk)
* Primality Proving with Elliptic Curves
(Laurent Théry and Guillaume Hanrot)
* Automatically translating type and function definitions from HOL
to ACL2
(James Reynolds)
* Formalising Java's Data-Race-Free Guarantee
(David Aspinall and Jaroslav Sevcik)
* Simple Types, deep and shallow
(Benjamin Werner)
* Program verification: operational semantics, concurrency and weak
memory models
(Tom Ridge)
* A modular formalisation of finite group theory
(Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi
and Laurent Théry)
* Building Formal Method Tools in the Isabelle/Isar Framework
(Makarius Wenzel and Burkhart Wolff)
* Verification of Expectation Properties for Discrete Random
Variables in HOL
(Osman Hasan and Sofiene Tahar)
* HOL2P - A System of Classical Higher Order Logic with Second
Order Polymorphism
(Norbert Voelker)
* Using XCAP to Certify Realistic System Code: Machine Context
Management
(Zhaozhong Ni, Dachuan Yu and Zhong Shao)
* Extracting Purely Functional Contents from Logical Inductive Types
(David Delahaye, Catherine Dubois and Jean-Frédéric Étienne)
* Verifying nonlinear real formulas via sums of squares
(John Harrison)
* Proof Pearl: The Termination Analysis of TERMINATOR
(Joe Hurd)
* Proof Pearl: Wellfounded Induction on the Ordinals up to Epsilon-0
(Konrad Slind and Matt Kaufmann)
* Improving the Usability of HOL through Controlled Automation
Tactics
(Eunsuk Kang and Mark Aagaard)
Last updated: Nov 21 2024 at 12:39 UTC