axiom-math
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-math] address@hidden: TPHOLs 2005 2nd Call for Papers]


From: root
Subject: [Axiom-math] address@hidden: TPHOLs 2005 2nd Call for Papers]
Date: Thu, 20 Jan 2005 15:34:44 -0500

fyi.....


------- Start of forwarded message -------
Date: Thu, 20 Jan 2005 09:42:19 -0600
From: Matt Kaufmann <address@hidden>
To: address@hidden
Subject: TPHOLs 2005 2nd Call for Papers


            ********************************************
            *               TPHOLs 2005                *
            *                                          *
            *  Theorem Proving in Higher Order Logics  *
            *                                          *
            *           2nd Call for Papers            *
            ********************************************

TPHOLs 2005
Oxford, UK
22-25 August 2005
http://web.comlab.ox.ac.uk/TPHOLs2005/

SECOND CALL FOR PAPERS

TOPICS

The program committee welcomes submissions on all aspects of theorem
proving in higher order logics, on related topics in theorem proving
and verification, and on relevant applications. The topics include,
but are not limited to, the following:

 * Specification and verification of hardware: microprocessors, memory
   systems, buses, pipelines, etc; formal semantics of hardware design
   languages; synthesis; formal design flows.

 * Specification and verification of software: program verification,
   refinement, and synthesis for functional, declarative and
   imperative languages; formal semantics of programming languages;
   proof carrying code.

 * Industrial application of theorem provers.

 * Formalization of mathematical theories.

 * Advances in theorem prover technology: proof automation and
   decision procedures, induction, combination of deductive and
   algorithmic approaches, incorporation of theorem provers into
   larger systems, combination of theorem provers with other provers
   and tools.

 * Other topics, including: security algorithms, properties, and
   policies; specification and requirements analysis of systems; user
   interfaces for theorem provers; development and extension of higher
   order logics.

 * Proof Pearls: concise and elegant presentations of interesting
   examples.

Relevant research involving interactive first-order systems, such as
ACL2 and Mizar, is also welcome. All authors are reminded that their
work should be presented in a way that users of other systems can
understand.

SUBMISSIONS

Submissions are invited in the following categories: Mature Work and
Emerging Trends.

                          Mature Work               Emerging Trends
Submission deadline       Friday 18 February 2005   Friday 27 May 2005
Acceptance notification   Friday 15 April 2005      Friday 13 June 2005
Camera-ready copy due     Friday 13 May 2005        Friday 15 July 2005

Submissions under Mature Work will be fully refereed, and the accepted
papers will be published in a volume of Springer's Lecture Notes in
Computer Science series, which will be available at the conference.
Authors of accepted papers are expected to present their work at the
conference.

Submissions under Emerging Trends will not be formally refereed, but
their content and relevance will be reviewed. Those submissions
accepted will be published in a University of Oxford technical report,
which will be available at the conference. Authors of accepted papers
are expected to present a brief outline of their work at the
conference and to prepare a poster for display at the conference
venue. Unless otherwise requested, submissions rejected under Mature
Work will also be considered for inclusion under Emerging Trends.

Papers should be no more than 16 pages in length and should be written
using LaTeX2e and the LNCS style file. Instructions on how to submit
papers will be made available on the conference web site. For all
enquiries concerning the conference, please use the email address
address@hidden

PROGRAM COMMITTEE

Mark Aagaard (Waterloo)
Clark Barrett (NYU)
David Basin (ETH Zurich)
Yves Bertot (INRIA)
Ching-Tsun Chou (Intel)
Thierry Coquand (Chalmers)
Amy Felty (Ottawa)
Jean-Christophe Filliatre (Paris Sud)
Jacques Fleuriot (Edinburgh)
Jim Grundy (Intel)
Elsa Gunter (UIUC)
John Harrison (Intel)
Jason Hickey (Caltech)
Peter Homeier (US DoD)
Joe Hurd (Oxford) (PC Chair)
Paul Jackson (Edinburgh)
Thomas Kropf (Tubingen & Bosch)
Pete Manolios (Georgia Tech)
John Matthews (Galois)
Cesar Munoz (National Institute of Aerospace)
Tobias Nipkow (Muenchen)
Sam Owre (SRI)
Christine Paulin-Mohring (Paris Sud)
Lawrence Paulson (Cambridge)
Frank Pfenning (CMU)
Konrad Slind (Utah)
Sofiene Tahar (Concordia)
Burkhart Wolff (ETH Zurich)
- ------- End of forwarded message -------
------- End of forwarded message -------




reply via email to

[Prev in Thread] Current Thread [Next in Thread]