From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id C2FE0BBAF for ; Fri, 13 Mar 2009 07:28:20 +0100 (CET) X-IronPort-AV: E=Sophos;i="4.38,355,1233529200"; d="scan'208";a="24263572" Received: from tu140033.ip.tsinghua.edu.cn (HELO [192.168.1.12]) ([166.111.140.33]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 13 Mar 2009 07:28:19 +0100 Message-ID: <49B9FD00.3020401@inria.fr> Date: Fri, 13 Mar 2009 14:28:16 +0800 From: Frederic Blanqui User-Agent: Thunderbird 2.0.0.19 (X11/20090105) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Call for paper - 10th Intl. Workshop on Termination - WST 2009 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; compiler:01 inference:01 wiki:01 haskell:01 ocaml:01 ocaml:01 dagstuhl:01 aachen:01 rewriting:01 intl:98 2009:98 intl:98 2009:98 valencia:98 terminate:01 Dear all, the 10th Intl. Workshop on Termination welcomes contributions from the functional programming community. See the general call for papers below, and let me add a few words here. The typical functional (compiler) programmer needs - termination of programs - termination of program transformations (rules) - termination of program analysis (type checking/inference) So I'm sure the workshop topic is highly relevant, and we are looking for *your* contributions. Also, we have an annual competition for automated termination provers, http://termination-portal.org/wiki/Termination_Competition and since 2007 it contains a Haskell category but no OCaml category yet. The problems there are taken directly from the Standard Library. So if you have some kind of (OCaml) source code analyzer that knows something about termination (perhaps only internally), then you're welcome turn it into a termination prover and submit it to this competition. (Details will be discussed at the workshop.) Best regards, Frederic Blanqui. ..................................................................... 10th International Workshop on Termination (WST 2009) Leipzig, Germany, June 3-5, 2009 http://www.imn.htwk-leipzig.de/wst09/ Termination is a fundamental topic in computer science. Classical undecidability results show that termination is difficult. On the other hand, programs are usually required to terminate. So methods are needed that prove termination and non-termination automatically for a wide range of programs. Termination proofs are essential not only for program verification, but also as components of program transformation systems. The topic is challenging both in theory (mathematical logic, proof theory) and practice (software development, formal methods), and many interesting ramifications are yet to be explored. The 10th International Workshop on Termination will delve into all aspects of termination of processes. It will continue the sequence of successful workshops held in St. Andrews (1993), La Bresse (1995), Ede (1997), Dagstuhl (1999), Utrecht (2001), Valencia (2003), Aachen (2004), Seattle (2006), and Paris (2007). It will attain the same friendly atmosphere as those past workshops. The intent is to bring together, in an informal setting, researchers interested in all aspects of termination, whether this interest be practical or theoretical, primary or derived. The workshop shall help exchange ideas from term rewriting and from the various programming language communities. Contributions from the imperative, constraint, functional, and logic programming communities, and papers investigating new applications of termination are particularly welcome. Program Committee: Frederic Blanqui, INRIA, FR and Tsinghua University, CN Byron Cook, Microsoft Corporation, US Alfons Geser, HTWK Leipzig, DE (chair) Michael Hanus, Universität Kiel, DE Janis Voigtlander, Technische Universität Dresden, DE Local organization: Johannes Waldmann, HTWK Leipzig, DE Important Dates: Paper submission 19 April 2009 Notification 26 April 2009 Final Paper Version 3 May 2009 Conference Venue: The workshop will be held in the city of Leipzig, at the conference center Mediencampus Villa Ida. Hosting institution: Hochschule fur Technik, Wirtschaft und Kultur Leipzig, in cooperation with Leipzig School of Media and Medienstiftung der Sparkasse Leipzig.