Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Didier.Remy@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Para - 18/5/99 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                        Salle de conference du Bat 8

                            Mardi 18 mai, 10h30

                               --------------
                               Peter Selinger
                               --------------

                           University of Michigan

                       ==============================
                       Control Categories and Duality
                       ==============================

In this talk, I will describe a direct categorical semantics for a
simple language with sequential control operators, namely Parigot's
lambda mu calculus. The semantics generalizes the well-known
interpretation of the simply-typed lambda calculus in a
cartesian-closed category.  I will introduce the class of "control
categories", which are based on Power and Robinson's premonoidal
categories and closely related to Thielecke's tensor-not categories.
I will prove, via a categorical structure theorem, that the
categorical semantics is equivalent to a CPS semantics in the style of
Hofmann and Streicher. I will show that the call-by-name
lambda-mu-calculus forms an internal language for control
categories. Moreover, the call-by-value lambda-mu-calculus forms an
internal language for the dual co-control categories.  As a
consequence, one obtains a syntactic, isomorphic translation between
call-by-name and call-by-value which preserves the operational
semantics, answering a question of Streicher and Reus. Thus, in this
setting one can make precise the duality between demand-driven and
value-driven computation.

Internal language results are encouraging: they give us a "syntax-free"
way of studying languages. For instance, the lambda-mu-calculus is
just one internal language for control categories - Felleisen's C and
Thielecke's CPS calculus are others. Thus, these languages are
equivalent in a sense. Since Thielecke's CPS calculus coincides with
the sequential fragment of the join calculus, it is an interesting
question whether its semantics can be generalized to get direct models
of concurrent calculi.