[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
------------------------------------------------------------------------------- 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 -------------------------------------------------------------------------------