[TYPES/announce] Call for abstracts/participation: LIX Colloquium 2013

[Kaustuv Chaudhuri]

LIX Colloquium on
THE THEORY AND APPLICATION OF FORMAL PROOFS

http://www.lix.polytechnique.fr/colloquium2013/

5-7 November 2013, Ecole Polytechnique, Palaiseau, France
In association with: PSATTT, 8 Nov 2013.


This three day colloquium will be composed of a number of hour long
talks by invited speakers and 30 minute talks based on contributed
abstracts. It is meant as a venue for the exchange of ideas. No
proceedings are planned apart from a simple collection of short
abstracts of all talks.

The colloquium will be followed by the workshop: Proof Search in
Axiomatic Theories and Type Theories (PSATTT) 2013.


THEME

  Formal proofs are becoming increasingly important in a number of
  domains in computer science and mathematics. The topic of the
  colloquium is structural proof theory, broadly construed. The
  following are some examples of relevant topics (not exhaustive):

  STRUCTURE OF PROOFS
    sequential and parallel structures in proofs; sharing and
    duplication of subproofs; permutations of proof steps; canonical
    forms; focusing and polarities; graphical proof syntax; proof
    complexity

  CHECKING PROOFS
    generating, transmitting, translating, and checking proof objects;
    universal proof languages; proof certificates; proof compression;
    cut-introduction; certification of high-performance systems (SMT,
    resolution, etc.)

  PROOF SEARCH
    automated and interactive proof search in constrained logics
    (linear, temporal, bunched, probabilistic, etc.); combining
    deduction and computation in search; reasoning about inductive and
    co-inductive fixpoints; cyclic proofs; computational
    interpretations of proof search

  COMPUTING WITH PROOFS
    cut-elimination strategies; cut-elimination by resolution (CERes);
    Curry-Howard correspondence


INVITED SPEAKERS

    Chad E. Brown, Saarland University
    Agata Ciabattoni, TU Vienna
    David Delahaye, CNAM, invited by PSATTT
    Alessio Guglielmi, University of Bath
    Dominic Hughes, Stanford University
    Sara Negri, University of Helsinki
    Claudio Sacerdoti Coen, University of Bologna
    Alex Simpson, University of Edinburgh
      [More to be confirmed]


CALL FOR ABSTRACTS AND PARTICIPATION

The colloquium is free and open to all, but registration is requested.
If you would like to attend, please send a mail to Kaustuv Chaudhuri
<kaustuv at lix.polytechnique.fr>.

If you would like to contribute a 30 minute presentation related to the
themes of the colloquium, please submit a 1-2 page abstract (as
PDF) via EasyChair at

    https://www.easychair.org/conferences/?conf=tafp2013

The deadline for submissions is 1 October 2013. Decisions on
submissions will be made before 8 October 2013.


VENUE

The colloquium and the PSATTT workshop will take place in the
Laboratoire d'Informatique (LIX) of the Ecole Polytechnique. The
Polytechnique is situated in the southern suburbs of Paris, about
40 minutes from central Paris by regional train. LIX is co-located
with INRIA Saclay.


ORGANIZERS

Dale Miller, Lutz Strassburger, Stéphane Graham-Lengrand, Assia
Mahboubi, Kaustuv Chaudhuri


SUPPORT

  * Laboratoire d’Informatique (LIX) of the Ecole Polytechnique
    http://www.lix.polytechnique.fr/

  * ERC Advanced Grant ProofCert
    https://team.inria.fr/parsifal/proofcert/


SEE ALSO

  * PSATTT Workshop 2013
    http://www.lix.polytechnique.fr/~lengrand/Events/PSATTT13/

  * Travelling to LIX/Ecole Polytechnique
    https://team.inria.fr/parsifal/meetings/directions/