The Coq mailing list

[Ekaterina Komendantskaya <komendantskaya AT gmail.com>]

Please distribute to those you might think are interested.

========================================================================
                        2nd 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/>

========================================================================

Note the changes:

Second invited speaker is now confirmed: Alexander Krauss, Munich

Pre-proceedings will be published and maintained by EasyChair

Change in the deadline for the final version (will affect only accepted papers)

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
---------------
* 29 March 2010: Submission deadline
* 29 April 2010: Notification of acceptance
* 18 May 2010: Final version of accepted papers (Notice the slight change compared to previous announcements)
* 15 July 2010: the workshop

Invited Speakers
----------------
* Conor McBride (University of Strathclyde)
* Alexander Krauss (Technical University of Munich)

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
________________________________