(I am sending this on behalf of a colleague) [Papers dealing with partiality and termination using monadic programming or other functional programming techniques are welcome] Please distribute to those you might think are interested. ======================================================================== 1st Call for Papers PAR 2010 Workshop on Partiality And Recursion in Interactive Theorem Provers Edinburgh, UK, 15 July 2010 (satellite workshop of ITP'10) a mid-FLoC 2010 workshop <http://www.cs.st-andrews.ac.uk/~ek/PAR-10/> ======================================================================== 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: * partial functions and functions over partial objects in theorem provers; * specialised type systems for general (co)recursion; * syntactical tests to guarantee termination of general recursive functions; * syntactical tests to guarantee productivity of functions on infinite objects; * methods to ensure termination of special classes of recursion definitions, eg nested recursion, simultaneous inductive-recursive data types and functions; * semantic approaches to termination and productivity, eg based on domain theory and topology; * categorical approaches to termination and productivity; * algebra of programming with partial functions and general (co)recursion. Description of software tools and case studies for dealing with the issues in the scope of the workshop are welcome. Submissions ----------- The articles will be evaluated by the PC for publication in the proceedings of the workshop. The final proceedings will be published after the workshop as a special issue of EPTCS and a preliminary version will be available during the workshop. 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 EPTCS macro package <http://style.eptcs.org/>. The web-based system EasyChair will be used for submission (<http://www.easychair.org/conferences/?conf=par10>). Important dates --------------- * 29 March 2010: Submission deadline * 29 April 2010: Notification of acceptance * 24 May 2010: Final version of accepted papers * 15 July 2010: the workshop Invited Speakers ---------------- * Conor McBride (University of Strathclyde) * TBA Programme Committee ------------------- Andreas Abel (Ludwig Maximilians University Munich, D) Yves Bertot (INRIA Sophia-Antipolis, FR) Ana Bove (Chalmers University of Technology, SE) Ekaterina Komendantskaya (University of St Andrews, UK) Ralph Matthes (IRIT Toulouse, FR) Milad Niqui (CWI, NL) Anton Setzer (Swansea University, UK) Organisers ---------- Ana Bove Ekaterina Komendantskaya Milad Niqui