Email Gateway (Aug 18 2022 at 11:34): Email Gateway (Aug 18 2022 at 11:34):From: Christoph Benzmueller <chris@ags.uni-sb.de>
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>.
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
Last updated: May 03 2024 at 12:27 UTC