Email Gateway (Aug 18 2022 at 11:57): Email Gateway (Aug 18 2022 at 11:57):From: Otmane Ait Mohamed <ait@encs.concordia.ca>
FIRST CALL FOR PARTICIPATION
21st International Conference on Theorem Proving in
Higher Order Logics
(TPHOLs 2008)
http://www.ece.concordia.ca/TPHOLs2008
tphols08@ece.concordia.ca
August 18-21, 2008, Montreal, Quebec, Canada
The 2008 International Conference on Theorem Proving in Higher Order
Logics will be the 21st in a series that dates back to 1988. The
conference will be held in Montreal, Quebec, Canada, on 18-21 August 2008.
REGISTRATION
Registration is now open. Please visit the TPHOLs 2008 web site,
http://www.ece.concordia.ca/TPHOLs2008/, to register.
INVITED SPEAKERS
Mike Gordon, University of Cambridge, UK.
Twenty Years of Theorem Proving for HOLs
Steve Miller, Advanced Technology Center, Rockwell Collins, USA
Will This Be Formal?
INVITED TUTORIALS
Konrad Slind. A Brief Overview of HOL4
Sam Owre. A Brief Overview of PVS
Makarius Wenzel. The Isabelle Framework
Yves Bertot. A short presentation of Coq
Matt Kaufmann. An ACL2 Tutorial
ACCOMMODATION
Information on accommodation is available on the TPHOLs 2008
web site (click on the registration tab).
RELATED EVENTS
On Friday 22 August, the day after TPHOLs 2008 finishes, the UITP
Workshop on User Interfaces for Theorem Proving will take place.
Further information on the UITP workshop
can be found at http://www.informatik.uni-bremen.de/~cxl/uitp/
SPONSORS
TPHOLs 2008 is sponsored by the following organizations:
o ENCS
o NIA
o Intel
o RESMIQ
o Concordia University
CONTACT
Enquiries concerning the conference should be emailed to
tphols08@ece.concordia.ca
OUTLINE PROGRAMME
Monday 18th, Tuesday 19th: Technical sessions.
Wednesday 20th: Technical sessions; excursion; conference dinner.
Thursday 21st: Technical sessions.
Friday 22nd : UITP workshop.
The preliminary programme is available on the conference web site.
VENUE
TPHOLs'08 will be be held at the new 19-storey (two underground floors)
Concordia Engineering & Computer Science building, home of the Engenering
and Computer Science faculty. The building is located in downtown
Montreal, an irresistible blend of European charm and
North American effervescence, Montreal's architecture enchants the visitor
with its harmonious contrast of old and new. With some 3.7 million inhabitants
and 80 distinct ethnic cultures, Montal is a resolutely international city.
A world leader in a wide range of industries, including aeronautics,
information technology and biotechnologies, the city is also renowned for innovation
in medicine, multimedia and arts. Getting around the city on a day-to-day basis is hassle-free.
Its streets, underground pedestrian network and subway system are safe and easy to navigate.
Montalers are naturally charming and quite often multilingual, always ready to strike up a
conversation and share a moment of friendship. This spontaneous hospitality has made Montal
the site of many exciting international festivals, which - much like the city and its
inhabitants - are a manifestation of pure passion!
(http://www.concordia.ca/about/whereweare/montreal/)
ACCEPTED REGULAR PAPERS
Klaus Aehlig, Florian Haftmann and Tobias Nipkow.
A Compiled Implementation of Normalization by Evaluation
Daniel Wasserrab and Andreas Lochbihler.
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
Ana Bove and Venanzio Capretta.
A Type of Partial Recursive Functions
Sascha Bhme, Rustan Leino and Burkhart Wolff.
HOL-Boogie --- An Interactive Prover for the Boogie Program-Verifier
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkok and John Matthews.
Imperative Functional Programming with Isabelle/HOL
David Cock, Gerwin Klein and Thomas Sewell.
Secure Microkernels, State Monads and Scalable Refinement
David Lester.
Real Number Calculations and Theorem Proving: Validation and Use of an Exact Arithmetic
Holger Gast.
Lightweight Separation
Hasan Amjad.
LCF-style Propositional Simplification With BDDs and SAT Solvers
Jens Brandt and Klaus Schneider.
Formal Reasoning about Causality Analysis
Pierre Courtieu, Julien Forest and Xavier Urbain.
Certifying a Termination Criterion Based on Graphs, without Graphs
Matthieu Sozeau and Nicolas Oury.
First-Class Type Classes
Yves Bertot, Georges Gonthier, Sidi Ould Biha and Ioana Pasca.
Canonical Big Operators
Stefan Berghofer and Christian Urban.
Nominal Inversion Principles
Polyvios Pratikakis, Jeff Foster, Michael Hicks and Iulian Neamtiu.
Formalizing Soundness of Contextual Effects
Laurent Thery.
Proof Pearl: Revisiting the Mini-Rubik in Coq
Russell O'Connor.
Certified Exact Transcendental Real Number Computation in Coq
Sayan Mitra and K. Mani Chandy.
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
Last updated: Nov 21 2024 at 12:39 UTC