The Coq mailing list

[Christoph Benzmueller <chris AT ags.uni-sb.de>]

The LPAR 2005 Workshop on
------------------------------------------------------------------------
     Empirically Successful Automated Reasoning
     in Higher-Order Logics (ESHOL)

will be held at

     Wexford Hotel, Montego Bay, Jamaica
     December 2nd 2005

     (http://www.ags.uni-sb.de/~chris/ESHOL-05/ ;)
------------------------------------------------------------------------

This workshop brings together practioners and researchers who are 
involved in the everyday aspects of logical systems based on 
higher-order logic. We hope to create a friendly and highly interactive 
setting for discussions around the following four topics. Implementation 
and development of proof assistants based on any notion of 
impredicativity, automated theorem proving tools for higher-order logic 
reasoning systems, logical framework technology for the representation 
of proofs in higher-order logic, formal digital libraries for storing, 
maintaining and querying databases of proofs. We solicit paper 
submissions within or related to the following two areas.

Systems
* Tactic-based proof assistants. Heuristics.
* Automated theorem proving. Proof search. Resolution. Equational theories.
* Implementation. Higher-order unification. Term-indexing.
* Logical frameworks. Meta-languages for logical formulas and proofs.
* Formal digital libraries of mathematical proof. Database technology. 
Query languages.
* Integration of Reasoning Systems.

Applications
* Comparative analysis of higher-order reasoning techniques.
* Experience reports. Integration and cooperations with their logics, 
contraint solvers, model generators, and model checkers.
* Special purpose reasoning techniques for practical applications.
* User interfaces.
* Practical results of proof representation and compression.
* Logic morphisms.
* Digital libraries. Benchmark problems. Challenge problems.

We envision attendees that are interested in fostering the development 
and visibility of reasoning systems for higher-order logics. We are 
particularly interested in a discusssion on the development of a 
higher-order version of the TPTP and in comparisons of the practical 
strengths of automated higher-order reasoning systems.

Additionally, the workshop will include *system and application 
demonstrations*. Demonstrations of systems and applications described in 
paper presentations, and demonstrations of systems and applications 
without an accompanying paper, are both encouraged.

ESHOL is the successor of the ESCAR  and ESFOR  workshops held at CADE 
2005 and IJCAR 2004.

------------------------------------------------------------------------
*Organization*

Structure of the Workshop
The workshop will be a 1 day workshop organized as follows:
* Presentation sessions, system demonstrations
* Invited talk
* Panel Discussion (or similarly organized event): How can we built-up a 
higher-order TPTP to foster the improvement of automated higher-order 
reasoning systems and their comparison with first-order theorem provers?

Programme Committee
Peter Andrews     Carnegie Mellon University, USA
Michael Beeson    San Jose State University, USA
Chad Brown        Saarland University, Germany
Gilles Dowek      École Polytechnique, France
Christoph Kreitz  Potsdam University, Germany
Larry Paulson     Cambridge University, UK
Frank Pfenning    Carnegie Mellon University, USA
Geoff Sutcliffe   University of Miami, USA
Volker Sorge      University of Birmingham, UK
Freek Wiedijk     Nijmegen University, Netherlands

Organizers and PC Chairs
Christoph Benzmüller  Saarland University, Germany
John Harrison         Intel Corporation, USA
Carsten Schürmann     Yale University, USA

If you have any questions about the workshop, please email the 
organizers <mailto:eshol05 AT ags.uni-sb.de>.

------------------------------------------------------------------------
*Submission*

Submission of papers for presentation at the workshop, and proposals for 
system and application demonstrations at the workshop, are now invited. 
Submissions will be reviewed, and a balanced program of high-quality 
contributions will be selected. Submissions can be in PDF or Postscript, 
and must conform to the format produced by LaTeX with this template. 
There is a 20 page limit. Long listings of problems or computer output 
should be relegated to a referenced WWW site.

Proposals for system and application demonstrations must include:

* System name, developers names and contact details.
* A system description, or associated paper submission.
* Screen shots or information for online access.
* Details of hardware and software that will have to be provided by the 
organizers if the demonstration is approved.

Those who submit proposals are encouraged to provide evidence that the 
system or application is empirically successful.
Submission is via EasyChair (thanks to Andrei Voronkov).

Important Dates
* Submission deadline - September 15th
* Notification of acceptance - October 15th
* Camera ready versions due - November 1st
* Workshop - December 2nd

------------------------------------------------------------------------
*Journal Publication*

The Journal of Applied Logic has agreed to a special issue on 
empirically successful higher-order automated reasoning. Authors of 
ESHOL papers will be able to submit extended versions of their workshop 
papers for this special issue. All papers submitted for the special 
issue will be reviewed according to the journal's standards.
------------------------------------------------------------------------