Preface

This volume contains the proceedings of the Workshop on Partiality and Recursion in Interactive Theorem Provers (PAR 2010) which took place on July 15 in Edinburgh, UK. This workshop was 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 2010 was 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.

Submissions on all aspects of partiality and termination of general (co)recursive functions in a logical framework were invited.

The programme committee of PAR 2010 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 included two invited talks, five contributed articles and three informal presentations.

The invited talks, given by specialists in the area, were 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 three informal presentations fitted into the programme following a call for informal discussion of ongoing research on the topic of the workshop.

This volume contains an article based on one of the invited talks and five regular contributed 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. Finally, we are grateful to Electronic Proceedings in Theoretical Computer Science (EPTCS) for accepting to publish this volume, and in particular Rob van Glabbeek and Benjamin Pierce for their help.