PAR'10 workshop is a venue for researchers working on new approaches to cope with partial functions and terminating general (co)recursion in theorem provers.
Theorem provers with inductive types provide a restricted programming language together with a formal meta-theory for reasoning about the language. When propositions are represented as types and proofs as programs, non-terminating proofs are disallowed for consistency and decidability of type checking. As a result, there is no trivial way to represent partial functions, and termination is syntactically ensured by imposing that the recursive calls must be made on structurally smaller arguments. Similar issues exist for productivity of functions on infinite objects where syntactic methods are used to ensure an infinite flow of data. The workshop aims to address these issues and various approaches for dealing with them.
We invite submissions on all aspects of partiality and termination of general (co)recursive functions in a logical framework.The topics of this workshop include but are not limited to:
The articles will be evaluated by the Program Committee for publication in the proceedings of the workshop. In accordance with FLoC'10 requirements, PAR'10 proceedings will be published in an electronic collection available online and maintained by EasyChair. The USB memory sticks with accepted papers will be distributed during the workshop.
The post-proceedings of PAR'10 will be published after the workshop as a special issue of EPTCS. Details on how and when to produce the post-workshop version of the articles will be communicated after the workshop to the authors of the accepted papers.
The articles must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Submissions should preferably not exceed 16 pages (excluding bibliography). Submissions must be prepared in LaTeX using the easychair latex package.
The web-based system EasyChair will be used for submission.