[TYPES/announce] Call for abstracts/participation: LIX Colloquium 2013: The Theory and Application of Formal Proofs

[Dale Miller]

LIX Colloquium 2013 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

    James Brotherston            [University College London]
    Chad E. Brown                [Saarland University]
    Agata Ciabattoni             [TU Vienna]
    David Delahaye               [CNAM, invited by PSATTT]
    Herman Geuvers               [Radboud University Nijmegen]
    Alessio Guglielmi            [University of Bath]
    Dominic Hughes               [Stanford University]
    Cezary Kaliszyk              [University of Innsbruck]
    Sara Negri                   [University of Helsinki]
    Claudio Sacerdoti Coen       [University of Bologna]
    Alex Simpson                 [University of Edinburgh]


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 one of the organizers.

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              <dale at lix.polytechnique.fr>
   Lutz Strassburger        <lutz at lix.polytechnique.fr>
   Stéphane Graham-Lengrand <graham-lengrand at lix.polytechnique.fr>
   Assia Mahboubi           <assia at lix.polytechnique.fr>
   Kaustuv Chaudhuri        <kaustuv at lix.polytechnique.fr>


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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20130909/5c79e2b4/attachment.html>