[TYPES/announce] CfP: Proof-Search in Type Theories (PSTT'10)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Papers PSTT 2010: International Workshop on Proof Search in Type Theories Edinburgh, Scotland July 15, 2010 http://www.lix.polytechnique.fr/~lengrand/Events/PSTT10/ Affiliated with FLOC, Edinburgh, Scotland IMPORTANT DATES Title + short abstract submission: April 10 Paper / long abstract submission: April 15 Notification: April 30 Final papers due: May 15 Workshop: July 15 DESCRIPTION: The PSTT workshop resumes a series of workshops on Proof Search in Type Theoretic Languages, in light of the progress that has been made over the last decade in e.g. the development of proof assistants or our understanding of proof theory. The declarative approach to programming has evolved two paradigms that are based on different aspects of the theories of proofs and types: Proof normalisation provides a foundation for functional programming and type systems --on which numerous proof assistants are based, while proof search provides a foundation for logic programming and other areas of automated deduction. On the one hand, proof search mechanisms and their automation are decisive features of proof assitants that have much to gain from a proper understanding and formalisation. On the other hand, the framework of logic programming has also extended to more expressive logics and more complex data structures, e.g. with bindings. Better specifying the proof search mechanisms in type theories is thus a key concern that brings both approaches forward, and closer together. This concern involves a wide range of issues and techniques (some of which directly arising from implementation) that both approaches share --or could share, and that form the scope of this workshop. TOPICS: Papers are solicited on topics including, but not limited to: - proof search strategies and tactics, complexity & completeness, - tactics specification language, - properties of inference systems, invertibility, polarity of connectives, - focusing, normal forms for proofs, - proof-term representation, - meta-variables, representation of partial proofs, - searching for proofs by induction, search for invariants, - unification, - variable binding, scoping management and freshness - logic programming and other paradigms based on proof search, termination & computational expressivity, - deduction-modulo, deduction vs. computation during search, - using failure in proof search, - model checking as deduction, - user interaction and interfaces, - systems implementing any of the above. SUBMISSIONS: Authors can submit either detailed and technical accounts of new research or work in progress. System descriptions are also welcome, with a demonstration on the day of the workshop. Surveys and comparative papers are also strongly encouraged. Papers / long abstracts are to be submitted electronically and are subject to a 12-page limit in LNCS format, including bibliography. They can be shorter. Authors are required to submit a title and a short abstract a few days before submitting the paper (see the dates section). At least one author of an accepted paper is expected to present that paper at the workshop. Informal proceedings will be distributed at the workshop. The possibility of having a special issue dedicated to the themes of this workshop is under consideration. For further information and submission instructions, see the PSTT web page: http://www.lix.polytechnique.fr/~lengrand/Events/PSTT10/. PROGRAM COMMITTEE: Claudio Sacerdoti Coen (Universita di Bologna) Stephane Lengrand (CNRS, Ecole Polytechnique) James McKinna (Radboud University, Nijmegen) Gopalan Nadathur (University of Minnesota)
[TYPES/announce] CfP: Proof-Search in Type Theories (PSTT'10)
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Call for Papers PSTT 2010: International Workshop on Proof Search in Type Theories Edinburgh, Scotland July 15, 2010 http://www.lix.polytechnique.fr/~lengrand/Events/PSTT10/ Affiliated with FLOC, Edinburgh, Scotland IMPORTANT DATES Title + short abstract submission: April 10 Paper / long abstract submission: April 15 Notification: April 30 Final papers due: May 15 Workshop: July 15 DESCRIPTION: The PSTT workshop resumes a series of workshops on Proof Search in Type Theoretic Languages, in light of the progress that has been made over the last decade in e.g. the development of proof assistants or our understanding of proof theory. The declarative approach to programming has evolved two paradigms that are based on different aspects of the theories of proofs and types: Proof normalisation provides a foundation for functional programming and type systems --on which numerous proof assistants are based, while proof search provides a foundation for logic programming and other areas of automated deduction. On the one hand, proof search mechanisms and their automation are decisive features of proof assitants that have much to gain from a proper understanding and formalisation. On the other hand, the framework of logic programming has also extended to more expressive logics and more complex data structures, e.g. with bindings. Better specifying the proof search mechanisms in type theories is thus a key concern that brings both approaches forward, and closer together. This concern involves a wide range of issues and techniques (some of which directly arising from implementation) that both approaches share --or could share, and that form the scope of this workshop. TOPICS: Papers are solicited on topics including, but not limited to: - proof search strategies and tactics, complexity & completeness, - tactics specification language, - properties of inference systems, invertibility, polarity of connectives, - focusing, normal forms for proofs, - proof-term representation, - meta-variables, representation of partial proofs, - searching for proofs by induction, search for invariants, - unification, - variable binding, scoping management and freshness - logic programming and other paradigms based on proof search, termination & computational expressivity, - deduction-modulo, deduction vs. computation during search, - using failure in proof search, - model checking as deduction, - user interaction and interfaces, - systems implementing any of the above. SUBMISSIONS: Authors can submit either detailed and technical accounts of new research or work in progress. System descriptions are also welcome, with a demonstration on the day of the workshop. Surveys and comparative papers are also strongly encouraged. Papers / long abstracts are to be submitted electronically and are subject to a 12-page limit in LNCS format, including bibliography. They can be shorter. Authors are required to submit a title and a short abstract a few days before submitting the paper (see the dates section). At least one author of an accepted paper is expected to present that paper at the workshop. Informal proceedings will be distributed at the workshop. The possibility of having a special issue dedicated to the themes of this workshop is under consideration. For further information and submission instructions, see the PSTT web page: http://www.lix.polytechnique.fr/~lengrand/Events/PSTT10/. PROGRAM COMMITTEE: Claudio Sacerdoti Coen (Universita di Bologna) Stephane Lengrand (CNRS, Ecole Polytechnique) Gopalan Nadathur (University of Minnesota)