The LPAR 2005 Workshop on
The workshop is open for all registered LPAR attendees
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.
| 09:00-10:00 | Invited Talk |
| Joe Hurd (Oxford): | |
| First Order Proof for Higher Order Logic Theorem Provers (pdf) | |
| 10:00-10:30 | Coffee Break |
| 10:30-12:30 | Paper 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:30 | Lunch Break |
| 13:30-14:30 | Invited Talk |
| Chad Brown (Saarbrücken): | |
| Benchmarks for Higher-Order Automated Reasoning (pdf) | |
| 14:30-15:30 | Paper 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:00 | Coffee Break |
| 16:00-17:00 | System Demonstrations (15min each) |
| Michael Beeson: | |
| Otter-λ (pdf) | |
| Chad Brown: | |
| TPS (pdf) | |
| Joe Hurd: | |
| Metis (pdf) | |
| Christoph Benzmüller: | |
| LEO | |
| 17:00-18:00 | Discussion: Higher-Order TPTP – Feasible or Not? |
| Chair and Panelists: TBA | |
| 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 |
| 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
The original CFP can be found here.
This page is also available as pdf.