*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle U/V, etage -2                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************


*** Vendredi 5 decembre 2003 **** 14h00 *****************************

Alan MYCROFT (University of Cambridge)

Linear Types for Packet Processing

Re'sume': We present PacLang: an imperative, concurrent, linearly-typed
language designed for expressing packet processing applications. 
PacLang's linear type system ensures that no packet is referenced by
more than one thread, but allows multiple references to a packet  within
a thread. We argue
(i) that this property greatly simplifies compilation of high-level
    programs to the distributed memory architectures of modern Network
    Processors; and
(ii) that PacLang's type system captures that style in which imperative
     packet processing programs are already written.
Claim (ii) is justified by means of a case-study: we describe a PacLang
implementation of the IPv4 unicast packet forwarding algorithm.

PacLang is formalised by means of an operational semantics and a Unique
Ownership theorem formalises its correctness with respect to the type
system.

Joint work with Robert Ennals and Richard Sharp.

*** Vendredi 12 decembre 2003 **** 13h00 Salle R *********************
                                   ------------- <- inhabituel!

Nachum DERSHOWITZ (Tel Aviv University)

The Four Sons of Penrose

Re'sume': We analyze Penrose's argument against the "strong artificial
intelligence'' premiss, as well as its logical alternatives.  We
then clarify the different positions one can take in answer to the
question raised by the argument, skirting the issue of introspection
per se. 

*********************************************************************
Pour recevoir l'annonce par courrier electronique: 
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************