[TYPES/announce] Call for papers: ESHOL workshop at IJCAR 2008

[Florian Rabe]

-------------------------------------------------------------------------------
                          Call for papers: ESHOL'08

The workshop

                *Evaluation of Systems for Higher Order Logic*

will be held as part of the 4th International Joint Conference on Automated
Reasoning (IJCAR'08) in Sydney, Australia.

Workshop website:     http://www.cs.miami.edu/~geoff/Conferences/ESHOL/
Workshop dates:       10/11 August 2008
Subsmission deadline: 19 May 2008 (abstract) / 26 May 2008 (full paper)

-------------------------------------------------------------------------------

This workshop brings together practitioners and researchers who are involved
in the development of reasoning systems based on higher-order logic. The
workshop will stimulate and foster the build-up of an infrastructure that
supports research, development, and deployment of higher-order reasoning
systems. A particular focus is on means to evaluate higher-order reasoning
systems.  Advances in these aspects of reasoning in higher-order logic will
make higher-order reasoning system easier to use in applications, e.g.,
hardware and software verification, knowledge based reasoning, and computer
aided mathematics. The workshop's notion of higher-order includes, but is not
limited to, ramified type theory, simple type theory, intuitionistic and
constructive type theory, and logical frameworks. The workshop's notion of
reasoning systems includes automated and semi-automated provers, model
generators, as well as proof and model checkers. The workshop will have three
parts:

  *Evaluation of Higher-Order Reasoning Systems*
          o Frameworks and tools for evaluation
          o Collections of test problems
          o Problem representation languages
          o Evaluation of automated higher-order reasoning systems, in
            particular, higher-order theorem provers
          o Evaluation of interactive higher-order reasoning systems
          o Evaluation of systems working for different higher-order
            logics and varying semantics

  *Descriptions of Successful Higher-Order Reasoning Systems*
          o Logical frameworks
          o Higher-order automated theorem provers
          o Interactive proof assistants supporting the partial
            automation of higher-order logic
          o Higher-order model checkers and higher-order model generators
          o Systems that automate natural fragments of higher-order
            logic, such as monadic second-order logic
      Due to the evaluative character of the workshop, descriptions of both
      existing and novel systems are welcomed. Descriptions of existing
      systems should stress successful applications and evaluations.

  *System Demonstration and System Competition*
      The systems described in the second part will be demonstrated. Moreover,
      a first competition "happening" for automated theorem provers for simple
      type theory is planned. This competition will be similar to the CASC
      competition for first-order reasoning systems. It will exploit and test
      the TPTP problem representation language for simple type theory, which
      was recently developed by the organizers.

We envision attendees that are interested in fostering the development and
visibility of reasoning systems for higher-order logics, and the connection
between research on the various flavors of higher-order logic. We are
particularly interested in comparisons of the practical strengths of higher-
order reasoning systems and in a discusssion on the development of a higher-
order version of the TPTP. Due to the intricate nature of higher-order logic,
we are also interested in a discussion on what practical strength means in
the context of higher-order logic and how it can be measured.

*Program Committee*

  Peter Andrews   Andrea Asperti Michael Beeson Christoph Benzmuller (Co-Chair)
  Chad Brown      Gilles Dowek   Viktor Kuncak  Dale Miller
  Michael Norrish Larry Paulson  Florian Rabe (Co-Chair)
  Sandip Ray      Carsten Schurmann (Co-Chair)  Natarajan Shankar
  Geoff Sutcliffe (Co-Chair)     Josef Urban

*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. There is a 20 page limit. Long listings
of problems or computer output should be relegated to a referenced WWW site.

Submission is via EasyChair (thanks to Andrei Voronkov). The selected
contributions will be printed as workshop proceedings, and will also be
published as CEUR Workshop Proceedings <http://ceur-ws.org>.

*Journal Publication*

The Journal of Applied Logic has agreed to a special issue around the topic of the ESHOL workshop, provided there are sufficiently many strong submissions. The special issue will target ESHOL participants, but will also also accept submissions from the broader community.

*Important dates*

    * Abstract submission deadline - 19th May
    * Submission deadline - 26rd May
    * Papers distributed to PC - 30th May
    * Reviews due in from PC - 23rd June
    * Notification of acceptance - 27th June
    * Final versions due - 14th July
    * Workshop - 10-11th August
-------------------------------------------------------------------------------