Published: 21st December 2010
DOI: 10.4204/EPTCS.43
ISSN: 2075-2180

EPTCS 43

Proceedings Workshop on
Partiality and Recursion in Interactive Theorem Provers
Edinburgh, UK, 15th July 2010

Edited by: Ana Bove, Ekaterina Komendantskaya and Milad Niqui

Preface
Ana Bove, Ekaterina Komendantskaya and Milad Niqui
Invited Presentation: Recursive Definitions of Monadic Functions
Alexander Krauss
1
MiniAgda: Integrating Sized and Dependent Types
Andreas Abel
14
Beating the Productivity Checker Using Embedded Languages
Nils Anders Danielsson
29
Rewriting and Well-Definedness within a Proof System
Issam Maamria and Michael Butler
49
General Recursion and Formal Topology
Claudio Sacerdoti Coen and Silvio Valentini
65
Termination Casts: A Flexible Approach to Termination with General Recursion
Aaron Stump, Vilhelm Sjöberg and Stephanie Weirich
76

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

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.

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.

Ana Bove
Ekaterina Komendantskaya
Milad Niqui
Göteborg, Dundee and Amsterdam, 16th of November 2010