From: Milad Niqui <M.Niqui@cwi.nl>
Submission deadline on Monday 29th of March
If you need a few days extension please send an email to Ana Bove
<bove@chalmers.se> with the request. A title and the abstract will still
be required by the 29th of March.
========================================================================
Final 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 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 (<http://www.easychair.org/easychair.zip>).
The web-based system EasyChair will be used for submission
(<http://www.easychair.org/conferences/?conf=par10>).
Important dates
18 May 2010: Final version of accepted papers (Notice the slight change
compared to previous announcements)
15 July 2010: the workshop
Invited Speakers
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
Last updated: Nov 21 2024 at 12:39 UTC