The LPAR 2005 Workshop on


The workshop is open for all registered LPAR attendees
(Proceedings in arxiv.org)

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 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 demonstrations. 
ESHOL is the successor of the ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004.

Timetable
09:00-10:00Invited Talk Joe Hurd (Oxford):  First Order Proof for Higher Order Logic Theorem Provers (pdf)10:00-10:30Coffee Break10:30-12:30Paper Session I (30min each)Michael Beeson: Implicit Typing in Lambda Logic (pdf)Christoph Benzmüller:  LEO -- A Resolution based Higher Order Theorem Prover  (pdf)Christoph Benzmüller, Volker Sorge, Mateja Jamnik and Manfred Kerber:  Combining Proofs of Higher-Order and First-Order Automated Theorem Provers  (pdf)12:30-13:30Lunch Break13:30-14:30Invited Talk Chad Brown (Saarbrücken):  Benchmarks for Higher-Order Automated Reasoning (pdf)14:30-15:30Paper Session II (30min each, chair: TBA)Jutta Eusterbrock:   Co-Synthesis of New Complex Selection Algorithms and their Human Comprehensible XML Documentation (pdf)Alwen Tiu, Gopalan Nadathur and Dale Miller:  Mixing Finite Success and Finite Failure in an Automated Prover (pdf)15:30-16:00Coffee Break16:00-17:00System Demonstrations (15min each)Michael Beeson:  Otter-λ (pdf)Chad Brown:  TPS (pdf)Joe Hurd:  Metis (pdf)Christoph Benzmüller:  LEO17:00-18:00Discussion: Higher-Order TPTP -- Feasible or Not?Chair and Panelists: TBA

Organization
Programme Committee
Peter AndrewsCarnegie Mellon University, USAMichael BeesonSan Jose State University, USAChad BrownSaarland University, GermanyGilles DowekÉcole Polytechnique, FranceChristoph KreitzPotsdam University, GermanyLarry PaulsonCambridge University, UKFrank PfenningCarnegie Mellon University, USAGeoff SutcliffeUniversity of Miami, USA Volker SorgeUniversity of Birmingham, UK Freek WiedijkNijmegen University, Netherlands
Organizers and PC Chairs
Christoph BenzmüllerSaarland University, GermanyJohn HarrisonIntel Corporation, USACarsten Schürmann Yale University, USA 
If you have any questions about the workshop, please email the organizers

The original CFP can be found here.

This page is also available as pdf.