Proof Search in Type Theories
associated with LICS
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.
More information can be found here.