coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CL&C - Call for participation

From: Ulrich Berger <U.Berger AT swansea.ac.uk>
To: cs-staff AT swansea.ac.uk, cs-research AT swansea.ac.uk, mathematics AT swansea.ac.uk, cca-l AT lists.uct.ac.za, Constructive Mathematics <conmat AT mathematik.uni-muenchen.de>, coq-club AT pauillac.inria.fr, Foundations of Mathematics <fom AT cs.nyu.edu>, isabelle-users AT cl.cam.ac.uk, kgs AT logic.at, Map AT mozart.ujf-grenoble.fr, nuprllist AT CS.Cornell.EDU, pvs AT csl.sri.com, types-announce AT lists.seas.upenn.edu, "[LOGIC] Mailing List" <logic AT math.uni-bonn.de>, theory AT cl.cam.ac.uk, theory-logic AT cs.cmu.edu, loginf AT lat.inf.tu-dresden.de, logik AT math.uni-freiburg.de, logik AT mathematik.uni-muenchen.de, logik AT math.uni-muenster.de, logic AT cs.stanford.edu
Subject: [Coq-Club] CL&C - Call for participation
Date: Mon, 09 Jun 2008 10:36:23 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: UWS

                      CALL FOR PARTICIPATION

                               CL&C

                     International Workshop on
                  Classical Logic and Computation
                http://www.doc.ic.ac.uk/~svb/CLaC08

                     Sunday, July 13, 2008
                      Reykjavik, Iceland

           Affiliated workshop of ICALP, July 6-13, 2008

CL&C'08 is the second of a new conference series on "Classical Logic
and Computation". It intends to cover all work aiming to explore
computational aspects of classical logic and mathematics.

INVITED SPEAKERS

   Helmut Schwichtenberg        LMU Munich

   Stephane Lengrand            LIX Polytechnique

CONTRIBUTED TALKS

   Dan Hernest and Trifon Trifonov:
   Light Dialectica Revisited

   Stefan Hetzl, Alexander Leitsch, Daniel Weller and
   Bruno Woltzenlogel  Paleo:
   Herbrand Sequent Extraction

   Richard McKinley:
   Herbrand expansion proofs and proof identity

   Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa and Hiroshi Nakano:
   Inhabitance of Existential Types is Decidable in
   Negation-Product Fragment

   Steffen van Bakel, Luca Cardelli and Maria Grazia Vigliotti:
   From X to pi; Representing the Classical Sequent Calculus
   in the `p-calculus

INFORMAL PRESENTATIONS

   James Brotherston and Cristiano Calcagno:
   Classical Logic of Bunched Implications

   Willem Heijltjes:
   Proof Forests with Cut-Elimination Based on Herbrand's Theorem

   Ozan Kahramanogullari:
   Ingredients of a Deep Inference Theorem Prover

   Diana Ratiu:
   An Application of the Refined A-Translation for a Variant of
   the Infinite PHP

   Alexander Summers:
   A Curry-Howard Correspondence for a Canonical Classical
   Natural Deduction

PROGRAMME COMMITTEE

   Steffen van Bakel            Imperial College London
   Ulrich Berger                Swansea, chair
   Stefano Berardi              Turin
   Paola Bruscoli               Bath
   Thierry Coquand              Chalmers
   Fernando Ferreira            Lisbon
   Michel Parigot               Paris VII
   Aldo Ursini                  Siena

REGISTRATION   Follow the link on the workshop web page
               http://www.doc.ic.ac.uk/~svb/CLaC08

CONTACT
u.berger AT swansea.ac.uk

Kind regards,
Ulrich Berger

[Coq-Club] CL&C - Call for participation, Ulrich Berger