From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5658 Path: news.gmane.org!not-for-mail From: Ekaterina Komendantskaya Newsgroups: gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.categories Subject: PAR'10 at FLOC'10: -- Final CFP Date: Thu, 25 Mar 2010 09:28:19 +0000 Message-ID: NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=0015173fe8620139b004829cac90 X-Trace: dough.gmane.org 1269509338 5109 80.91.229.12 (25 Mar 2010 09:28:58 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 25 Mar 2010 09:28:58 +0000 (UTC) To: coq-club@inria.fr, lfcs-interest@dcs.ed.ac.uk, stp@macs.hw.ac.uk, SPLS , blc@cs.nott.ac.uk, hamming-members@inf.ed.ac.uk, categories@mta.ca Original-X-From: coq-club-owner@inria.fr Thu Mar 25 10:28:52 2010 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1NujMv-0006Px-Bh for gsmlcc-coq-club@gmane.org; Thu, 25 Mar 2010 10:28:49 +0100 X-IronPort-AV: E=Sophos;i="4.51,306,1267398000"; d="scan'208";a="47761424" Original-Received: from walapai.inria.fr ([128.93.30.24]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 25 Mar 2010 10:28:48 +0100 Original-Received: from walapai.inria.fr (localhost [127.0.0.1]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id o2P9Sll7021665; Thu, 25 Mar 2010 10:28:47 +0100 Original-Received: (from sympa@localhost) by walapai.inria.fr (8.13.6/8.12.10/Submit) id o2P9SkVp021648; Thu, 25 Mar 2010 10:28:46 +0100 X-Authentication-Warning: walapai.inria.fr: sympa set sender to coq-club-owner@inria.fr using -f Original-Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id o2P9SiIg021642 for ; Thu, 25 Mar 2010 10:28:44 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtsDAPbJqkvRVdzXimdsb2JhbACBRI9KigoIFQEBAQoJDAcRBR+uG4FohTsuiEsBAQMFhHcEigGERw X-IronPort-AV: E=Sophos;i="4.51,306,1267398000"; d="scan'208";a="59674104" Original-Received: from mail-fx0-f215.google.com ([209.85.220.215]) by mail4-smtp-sop.national.inria.fr with ESMTP; 25 Mar 2010 10:28:39 +0100 Original-Received: by fxm7 with SMTP id 7so4775460fxm.17 for ; Thu, 25 Mar 2010 02:28:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:from:date:message-id :subject:to:content-type; bh=WsMZ19PYXyX/6Lpb7LOH28NnatHsXkhLJNC5R8bE9Y0=; b=Y31BLIYMzBbwrVHIJB3v+WIa44FR6lKV7ThVLsGaL9bQ03UTj3KUynWusFaidel2ee 4REw0ZWxYmdcHcLtlNQDp3AxOijF4Wu7iZ8c7Nk+GHv82lkXqUGN3bFr+M82xCHpxLOz HufKmZACUCa6evns6tM1eajPTBhkQYuRuLlCY= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=Dc9CxknqmlD+l869S25CmtpQZV3lMr6uRH7F37mH6zZiBfLAW/NlMyQmgnLqcapXiO L9RrJ1l7Ro9Z2S7x+zOcc+6sAOwSJo/mgus9iQslIQqztRl1zGizu4g1JJ27IUF76vdx nJERU0oo/0vEdIKQLtQ/vPIm+9aYI7xuWAzqI= Original-Received: by 10.223.5.81 with SMTP id 17mr422851fau.3.1269509319112; Thu, 25 Mar 2010 02:28:39 -0700 (PDT) X-Loop: coq-club@inria.fr X-Sequence: 375 Errors-to: coq-club-owner@inria.fr Precedence: list X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: X-Gmane-Expiry: 2010-04-08 Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:4673 gmane.science.mathematics.categories:5658 Archived-At: --0015173fe8620139b004829cac90 Content-Type: text/plain; charset=ISO-8859-1 ** Submission deadline on Monday 29th of March ** If you need a few days extension please send an email to Ana Bove 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 ======================================================================== 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 (). The web-based system EasyChair will be used for submission (). 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 ________________________________ --0015173fe8620139b004829cac90 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

** Submiss= ion deadline on Monday 29th of March **

If you need a few days exten= sion please send an email to Ana Bove
<= bove@chalmers.se> with the request. =A0A title and the abstract will= still
be required by the 29th of March.



=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 Final Call for Papers

=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0PAR 2010
=A0Workshop on Partiality And Recursion in Interactive Theorem Prover= s
=A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 Edinburgh, UK, 15 July 2010 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 (satellite workshop of ITP'10)
= =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 a mid-FLoC 2010 workshop
=A0 =A0 =A0 =A0 =A0 =A0 =A0<http://www= .cs.st-andrews.ac.uk/~ek/PAR-10/>

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

PAR'10 workshop is a venue for researchers working on new appr= oaches to
cope with partial functions and terminating general (co)recurs= ion in
theorem provers.

Theorem provers with inductive types provide a rest= ricted programming
language together with a formal meta-theory for reaso= ning about the
language. =A0When propositions are represented as types a= nd proofs as
programs, non-terminating proofs are disallowed for consistency and
deci= dability of type checking. =A0As a result, there is no trivial way to
re= present partial functions, and termination is syntactically ensured by
imposing that the recursive calls must be made on structurally smaller
a= rguments. 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 aspec= ts 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
= =A0provers;

* specialised type systems for general (co)recursion;
* syntactical tests to guarantee termination of general recursive
=A0functions;

* syntactical tests to guarantee productivity of functions on infinite<= br>=A0objects;

* methods to ensure termination of special classes of= recursion
=A0definitions, eg nested recursion, simultaneous inductive-r= ecursive data
types and functions;

* semantic approaches to termination and produc= tivity, eg based on
=A0domain theory and topology;

* categorical = approaches to termination and productivity;

* algebra of programming= with partial functions and general
=A0(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 P= rogram Committee for
publication in the proceedings of the workshop. =A0In accordance with
FL= oC'10 requirements, PAR'10 proceedings will be published in an
e= lectronic collection available online and maintained by
EasyChair. The U= SB 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. Detail= s on how and when to produce the
post-workshop version of the articles w= ill be communicated after the
workshop to the authors of the accepted papers.

The articles must co= ntain original contributions, be clearly written, and
include appropriat= e reference to and comparison with related work.
Submissions should pref= erably not exceed 16 pages (excluding
bibliography). Submissions must be prepared in LaTeX using the
EasyChair= latex package (<http://www.easychair.org/e= asychair.zip>).

The web-based system EasyChair will be used for submission
(<http://www.easychair.org/conferences/?= conf=3Dpar10>).


Important dates
---------------
* 29 March 2010: Submission d= eadline
* 29 April 2010: Notification of acceptance
* 18 May 2010: Fi= nal version of accepted papers (Notice the slight change
compared to pre= vious announcements)
* 15 July 2010: the workshop

Invited Speakers
----------------* Conor McBride (University of Strathclyde)
* Alexander Krauss (Technic= al University of Munich)

Programme Committee
-------------------<= br> Andreas Abel (Ludwig Maximilians University Munich, D)
Yves Bertot (INRI= A Sophia-Antipolis, FR)
Ana Bove (Chalmers University of Technology, SE)=
Ekaterina Komendantskaya (University of St Andrews, UK)
Ralph Matthe= s (IRIT Toulouse, FR)
Milad Niqui (CWI, NL)
Anton Setzer (Swansea University, UK)

Organ= isers
----------
Ana Bove
Ekaterina Komendantskaya
Milad Niqui
________________________________

=

--0015173fe8620139b004829cac90--