Skip to Content.
Sympa Menu

coq-club - [Coq-Club] New conference replacing RTA-TLCA

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] New conference replacing RTA-TLCA


Chronological Thread 
  • From: Luca Paolini <paolini AT di.unito.it>
  • Cc: agda AT lists.chalmers.se, agents AT cs.umbc.edu, aiia AT dis.uniroma1.it, ", aila" AT unicam.it, alg.announce AT catalyse.net, alp-diffusion AT univ-lille1.fr, ", apng-all" AT apng.org, appsem AT tcs.informatik.uni-muenchen.de, ", asl" AT vassar.edu, cade AT itu.dk, caml-list AT inria.fr, categories AT mta.ca, ", ccl" AT ps.uni-sb.de, clean-list AT science.ru.nl, clp AT comp.nus.edu.sg, ", comlab" AT comlab.ox.ac.uk, complog AT cs.nmsu.edu, comprox AT doc.ic.ac.uk, ", compulognet-parimp" AT dia.fi.upm.es, concurrency AT cwi.nl, coq-club AT inria.fr, ", cphc-conf" AT jiscmail.ac.uk, csd AT lists.ut.ee, curry AT lists.rwth-aachen.de, ", dmanet" AT zpr.uni-koeln.de, elsnet-list AT let.uu.nl, ", fg214" AT informatik.uni-kiel.de, finite-model-theory AT lists.rwth-aachen.de, ", fmics" AT inrialpes.fr, fom AT cs.nyu.edu, gdr.gpl AT imag.fr, gdr-im AT gdr-im.fr, ", haskell" AT haskell.org, hol-info AT lists.sourceforge.net, kgs-list AT logic.at, ", ki-inf" AT uni-koblenz.de, kr AT kr.org, lfcs-interest AT dcs.ed.ac.uk, ", lics" AT informatik.hu-berlin.de, linear AT cs.stanford.edu, ", loco" AT csc.liv.ac.uk, logic AT cs.stanford.edu, logic AT math.uni-bonn.de, ", logic-list" AT helsinki.fi, logik AT math02.mathematik.uni-muenchen.de, ", logik" AT math.uni-freiburg.de, lprolog AT cs.umn.edu, math.logik AT gmx.net, ", Maude-users" AT cs.uiuc.edu, mercury-users AT cs.mu.OZ.AU, ", moca-announce" AT list.it.uu.se, meta-announce AT cwi.nl, ", newsletter" AT aarinc.org, nvti-list AT cwi.nl, om-announce AT openmath.org, ", pept" AT yl.is.s.u-tokyo.ac.jp, pmt6sbc AT leeds.ac.uk, prog-lang AT diku.dk, ", prole" AT babel.ls.fi.upm.es, proof-complexity AT math.cas.cz, ", puml-list" AT cs.york.ac.uk, pvs AT csl.sri.com, relmics-l AT McMaster.CA, ", rewriting" AT listes.ens-lyon.fr, rewriting AT outlook-nameast.office365.com, ", rewriting-request" AT listes.ens-lyon.fr, sicstus-users-request AT sics.se, ", softtech" AT cs.uu.nl, spin_list AT research.bell-labs.com, ", theorem-provers" AT ai.mit.edu, theory AT cl.cam.ac.uk, ", theory-logic" AT cs.cmu.edu, types-announce AT lists.seas.upenn.edu, ", vki-list" AT dfki.de
  • Subject: [Coq-Club] New conference replacing RTA-TLCA
  • Date: Wed, 03 Jun 2015 12:16:43 +0200
  • Dkim-filter: OpenDKIM Filter v2.10.1 mail.di.unito.it t53AGjIv019652

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




  • [Coq-Club] New conference replacing RTA-TLCA, Luca Paolini, 06/03/2015

Archive powered by MHonArc 2.6.18.

Top of Page