PAR-10: Editor's Preface

This volume contains a preliminary version of the proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR'10) which will take place on July 15 in Edinburgh, UK. This workshop will be held as a satellite workshop of the International Conference on Interactive Theorem Proving (ITP 2010), itself part of the Federated Logic Conference 2010 (FLoC 2010).

PAR'10 is a venue for researchers working on new approaches to cope with partial functions and terminating general (co)recursion in theorem provers.

Theorem provers based on type theory 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. Submissions on all aspects of partiality and termination of general (co)recursive functions in a logical framework were invited.

The programme committee of PAR'10 consisted of

• Andreas Abel (Ludwig Maximilians University Munich, Germany),
• Yves Bertot (INRIA Sophia-Antipolis, France),
• Ana Bove (Chalmers University of Technology, Sweden),
• Ekaterina Komendantskaya (University of Dundee, UK),
• Ralph Matthes (IRIT Toulouse, France),
• Milad Niqui (CWI, The Netherlands),
• Anton Setzer (Swansea University, UK).

The workshop's programme includes two invited talks, five contributed articles and three informal presentations.

The invited talks, given by specialists in the area, are the following:

• Alexander Krauss, on Recursive Definitions of Monadic Functions,
• Conor McBride, on Djinn, monotonic.

The contributed articles were selected by the programme committee--- with the help of external referees--- following a review process which guaranteed at least three reviewers for each article, and a discussion period among the committee members. The five contributions, which were selected from a total of seven submissions, are as follows:

• Andreas Abel, on Integrating Sized and Dependent Types,
• Nils Anders Danielsson, on Beating the Productivity Checker Using Embedded Languages,
• Issam Maamria and Michael Butler, on Rewriting and Well-Definedness within a Proof System,
• Claudio Sacerdoti Coen and Silvio Valentini, on General Recursion and Formal Topology,
• Aaron Stump, Vilhelm Söoberg and Stephanie Weirich, on Termination Casts: A Flexible Approach to Termination with General Recursion.

The three informal presentations fit into the programme following a call for informal discussion of ongoing research on the topic of the workshop. The informal presentations are:

• Thorsten Altenkirch and Nils Anders Danielsson, on Termination Checking in the Presence of Nested Inductive and Coinductive Types,
• Gavin Mendel-Gleason and Geoff Hamilton, on Cyclic Proofs and Coinductive Principles,
• Tarmo Uustalu, on Antifounded Coinduction in Type Theory.

The formal proceedings of PAR'10 will be published as an issue of the Electronic Proceedings in Theoretical Computer Science (EPTCS) and will contain the five contributed articles and the invited articles.

We thank the programme committee members for their effort. We thank the external referees, Guillaume Burel, Peter Chapman, Roy Dyckhoff, Vladimir Komendantsky, Jorge Luis Sacchini and Tarmo Uustalu, for their help. We would like to thank FLoC 2010 and ITP 2010 organisers for giving us the opportunity to hold this workshop as an affiliated event and for taking care of the organisational matters. Handling of the submissions and the discussion was done using EasyChair, whose developers are gratefully acknowledged.