From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 87D8F7EE7D; Wed, 3 Jun 2015 12:40:08 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of paolini@di.unito.it) identity=pra; client-ip=130.192.156.1; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paolini@di.unito.it"; x-sender="paolini@di.unito.it"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of paolini@di.unito.it designates 130.192.156.1 as permitted sender) identity=mailfrom; client-ip=130.192.156.1; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paolini@di.unito.it"; x-sender="paolini@di.unito.it"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail.di.unito.it) identity=helo; client-ip=130.192.156.1; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="paolini@di.unito.it"; x-sender="postmaster@mail.di.unito.it"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0ATAgAR2W5VmQGcwIJbFoNOXgGDHaoaknUKhXcCKIFaEAEBAQEBAQERAQEBAQEICwsHIS6EGgkBAQQBAiAPAQUIAQEmCwUBAQ8lAgUTAwsCAgkDAgECAUUTAQcBARCFXYI8DbU6cIRkAQWfFgELARkGgSGKIoUGB4JoD4E2i1yHe4N5glOFfo5ahn6BBIMZbQGCRgEBBQ X-IPAS-Result: A0ATAgAR2W5VmQGcwIJbFoNOXgGDHaoaknUKhXcCKIFaEAEBAQEBAQERAQEBAQEICwsHIS6EGgkBAQQBAiAPAQUIAQEmCwUBAQ8lAgUTAwsCAgkDAgECAUUTAQcBARCFXYI8DbU6cIRkAQWfFgELARkGgSGKIoUGB4JoD4E2i1yHe4N5glOFfo5ahn6BBIMZbQGCRgEBBQ X-IronPort-AV: E=Sophos;i="5.13,546,1427752800"; d="scan'208";a="133486013" Received: from pianeta.di.unito.it (HELO mail.di.unito.it) ([130.192.156.1]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 03 Jun 2015 12:40:06 +0200 X-MailScanner-From: paolini@di.unito.it X-SpamCheck: not spam, SpamAssassin (not cached, score=-86.998, required 3, autolearn=not spam, AUTHENTICATEDUSER -100.00, AWL 14.39, BAYES_00 -1.90, MISSING_FROM 1.00, MISSING_HEADERS 1.02, RCVD_IN_DNSWL_MED -2.30, RDNS_NONE 0.79, SINGLE_HEADER_2K 0.00, SPF_PASS -0.00) X-AntiVirus: Email Clean X-dipinfo-MailScanner-ID: t53AGjIv019652 X-dipinfo-MailScanner-Information: Please contact Department of Computer Science technical staff for more information Received: from mail.di.unito.it ([130.192.156.1]) by mail.di.unito.it (INFO-DIP) with ESMTP id t53AGjIv019652 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NO AuthenticatedUser=paolini ); Wed, 3 Jun 2015 12:16:46 +0200 (CEST) DKIM-Filter: OpenDKIM Filter v2.10.1 mail.di.unito.it t53AGjIv019652 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=di.unito.it; s=dipinfo2011; t=1433326619; bh=BCQj9og0EewHXWogr3hOfUPWCH+zDu8qupXgXomI/NI=; h=Date:From:CC:Subject:References:In-Reply-To; b=NikMH1/BbYP63Cn8wFvtRf+Y9ib+uwgN3wg6G7vV5Wh4SEyVLQmb0lIdG8RUv8oU7 eIOvlSGU/UaTDKJuGG+5vT5PefYf2D8HKkrhAWRwSNE3Ap2ETFYWc14UKxc6Y79EE8 M5HKShVALGOhHSQKlN33uOFApBa+2TDZ1aqja35A= Message-ID: <556ED40B.6080907@di.unito.it> Date: Wed, 03 Jun 2015 12:16:43 +0200 From: Luca Paolini User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0 MIME-Version: 1.0 CC: agda@lists.chalmers.se, agents@cs.umbc.edu, aiia@dis.uniroma1.it, ", aila"@unicam.it, alg.announce@catalyse.net, alp-diffusion@univ-lille1.fr, ", apng-all"@apng.org, appsem@tcs.informatik.uni-muenchen.de, ", asl"@vassar.edu, cade@itu.dk, caml-list@inria.fr, categories@mta.ca, ", ccl"@ps.uni-sb.de, clean-list@science.ru.nl, clp@comp.nus.edu.sg, ", comlab"@comlab.ox.ac.uk, complog@cs.nmsu.edu, comprox@doc.ic.ac.uk, ", compulognet-parimp"@dia.fi.upm.es, concurrency@cwi.nl, coq-club@inria.fr, ", cphc-conf"@jiscmail.ac.uk, csd@lists.ut.ee, curry@lists.rwth-aachen.de, ", dmanet"@zpr.uni-koeln.de, elsnet-list@let.uu.nl, ", fg214"@informatik.uni-kiel.de, finite-model-theory@lists.rwth-aachen.de, ", fmics"@inrialpes.fr, fom@cs.nyu.edu, gdr.gpl@imag.fr, gdr-im@gdr-im.fr, ", haskell"@haskell.org, hol-info@lists.sourceforge.net, kgs-list@logic.at, ", ki-inf"@uni-koblenz.de, kr@kr.org, lfcs-interest@dcs.ed.ac.uk, ", lics"@informatik.hu-berlin.de, linear@cs.stanford.edu, ", loco"@csc.liv.ac.uk, logic@cs.stanford.edu, logic@math.uni-bonn.de, ", logic-list"@helsinki.fi, logik@math02.mathematik.uni-muenchen.de, ", logik"@math.uni-freiburg.de, lprolog@cs.umn.edu, math.logik@gmx.net, ", Maude-users"@cs.uiuc.edu, mercury-users@cs.mu.OZ.AU, ", moca-announce"@list.it.uu.se, meta-announce@cwi.nl, ", newsletter"@aarinc.org, nvti-list@cwi.nl, om-announce@openmath.org, ", pept"@yl.is.s.u-tokyo.ac.jp, pmt6sbc@leeds.ac.uk, prog-lang@diku.dk, ", prole"@babel.ls.fi.upm.es, proof-complexity@math.cas.cz, ", puml-list"@cs.york.ac.uk, pvs@csl.sri.com, relmics-l@McMaster.CA, ", rewriting"@listes.ens-lyon.fr, rewriting@outlook-nameast.office365.com, ", rewriting-request"@listes.ens-lyon.fr, sicstus-users-request@sics.se, ", softtech"@cs.uu.nl, spin_list@research.bell-labs.com, ", theorem-provers"@ai.mit.edu, theory@cl.cam.ac.uk, ", theory-logic"@cs.cmu.edu, types-announce@lists.seas.upenn.edu, ", vki-list"@dfki.de References: <543F6053.6050909@di.unito.it> In-Reply-To: <543F6053.6050909@di.unito.it> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-Validation-by: paolini@di.unito.it Subject: [Caml-list] New conference replacing RTA-TLCA Dear Everyone, As requested by the participants of the RTA-TLCA conference in Vienna 2014, the united Steering Committees of Rewriting Techniques and Applications (RTA) and Typed Lambda Calculi and Applications (TLCA) have prepared the attached proposal to replace our existing two conferences by a new one of a broader scope. As we embark on this exciting journey, we invite all members of the computer science community to provide comments, remarks, and suggestions for the new conference. All input will be passed on to the steering committee of the new conference after its constitutional general meeting on July 1st, 2015. Sincerely, Kristoffer Rose and Pawe³ Urzyczyn for the unanimous steering committees of RTA and TLCA. ===================================================================== It is our thesis that formal elegance is a prerequisite to efficient implementation. -- Gérard Huet[4] We, the communities behind the RTA[1] and TLCA[2] conferences, believe that our field has evolved and developed richer connections with many both practical and theoretical aspects of computer science and logic research since the inception of RTA in 1983 and TLCA in 1993. In particular, the scope of the two original conferences widened to include a significant overlap, and in fact the conferences have already collaborated by having most of our meetings since 2003 as the joint RDP[3] conference. We have therefore decided to propose a new conference, Formal Structures for Computation and Deduction (FSCD) which not only combines our scope but further extends it to cover all the inter-related formal areas that researchers in formal structures for computation and deduction engage in. The name of the new conference comes from an unpublished but important book by Gérard Huet[4] that was a strong influence on many researchers in our area. We are grateful to Gérard for allowing us to reuse the name. The extended scope of the conference will include all research related to formal structures for computation and deduction, in particular all areas/categories included in the attached non-exhaustive list of topics. We look very much forward to serve the scientific community with this new conference, which inherits as well as updates and modernizes the scope of the conferences it replaces. References. [1]http://rewriting.loria.fr/rta/ [2]http://www.mimuw.edu.pl/tlca/ [3]http://users.dsic.upv.es/~rdp03/ [4]http://pauillac.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz FSCD initial non-exhaustive list of topics (intended to extend the current RTA and TLCA scope, and expected to evolve over time): 1. Calculi a. Lambda-calculus b. Rewriting formats (string, term, higher-order, graph, conditional, ...) c. Proof theory (natural deduction, sequent calculi, proof nets, ...) d. Strategies in computation and deduction 2. Type Theory and Logical Frameworks a. Type systems (recursive, intersection types, polymorphism, ...) b. Dependent types and homotopy type theory c. Linear logic and other constructive logics d. Implicit complexity 3. Fundamentals of Functional and Declarative Programming a. Unification and narrowing b. Tree automata c. Continuations and control operators d. Coinduction and infinitary systems 4. Semantics a. Abstract machines b. Categorical semantics c. Denotational and game semantics d. Quantitative models (timing, probabilities) 5. Algorithmic Analysis of Formal Systems a. Type inference and type checking b. Complexity analysis c. Checking termination, confluence, and related properties d. Formalisation and certification 6. Tools and Applications a. Proof assistants and interactive theorem proving b. Automated deduction (completion, constraints, equational logic...) c. Symbolic computation d. Implementation techniques for formal systems e. Case studies and applications based on formal systems