********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 6 decembre 1996 **** 14h00 ***************************** Se'minaire annule', reporte' au 13 decembre 1996, le se'minaire initialement pre'vu le 13 decembre 1996 e'tant reporte' au 24 janvier 1997. *** Vendredi 13 decembre 1996 **** 14h00 **************************** Infinite observable behavior in the denotational semantics for concurrent languages Sven-Olof NYSTROM (Uppsala University & ENS) Re'sume' : What is the observable behavior of a concurrent process? Most semantic models for concurrent programming assume that only the finite behavior of a process is observable. I argue that the opposite view should be taken; there are good reasons to also allow the observation of infinite computations. A consequence of considering infinite observations is that it is no longer possible to give a fully abstract fixpoint semantics; in fact, I show that even if one considers, for example, a denotational semantics using non-continuous functions it is still not possible to give a fully abstract fixpoint semantics. This result can be extended to a wide range of semantic domains. I also give a fixpoint semantics (though not fully abstract) for a concurrent programming language (CCP) and sketch a proof of correctness. *** Vendredi 20 decembre 1996 *************************************** Rela^che, soutenance de these de Paul-Andre Mellies, voir l'annonce ci-dessous. *** Vendredi 28 decembre 1996 *************************************** Rela^che ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.ens.fr/~cousot/annonceseminaire.html ********************************************************************* ----------------------------------------------------------------------------- Je soutiendrai ma these intitulee: Description abstraite des systemes de reecriture le vendredi 20 decembre 1996 a 14h30 en salle W a l'Ecole Normale Superieure, 45 rue d'Ulm, 75005 PARIS. Vous etes cordialement invites a la soutenance ainsi qu'au pot qui suivra. Paul-Andre Mellies Resume: ------ Les systemes de reecriture permettent de decrire formellement ce qu'est un calcul pour en comprendre les proprietes. Le plus connu de ces systemes de reecriture, le lambda-calcul, a ouvert par son analyse la conception ulterieure des langages de programmation dits fonctionnels, des familles LISP ou ML. D'autres systemes de reecriture sont apparus depuis pour decrire des paradigmes de programmation differents, ou mieux refleter le comportement des compilateurs. Dans cette these, nous proposons de redemontrer les resultats syntaxiques fondamentaux du lambda-calcul: developpements finis, standardisation, normalisation, a` partir d'axiomes sur les structures du calcul: termes, reductions, re'sidus, emboitements, paires critiques. Parce qu'elle evite le traitement explicite de toute syntaxe, cette description abstraite des systemes de reecriture peut etre applique'e a une gamme etendue de calculs, ce qui evite de repeter constructions et preuves pour chaque langage particulier. Plus encore, ces axiomes capturent dans la syntaxe certaines notions semantiques comme la stabilite. En marge de cette reappropriation d'une tradition syntaxique, nous presentons un contre-exemple a la normalisation forte du lambda-sigma-calcul type, un lambda-calcul avec substitutions explicites. Nous appliquons ensuite nos constructions abstraites pour demontrer que les strategies externes ou necessaires du lambda-sigma-calcul (non type) sont normalisantes. Mots clefs: reecriture, lambda-calcul, confluence, standardisation, normalisation, concurrence, pi-calcul, logique lineaire. Ma these est disponible en: http://www.dcs.ed.ac.uk/home/paulm/ Summary: Rewriting systems can describe formally what is a calculus in order to understand its properties. The analysis of the lambda-calculus, this famous rewriting system, opened the later conception of functional programming languages like LISP or ML. Other rewriting systems have appeared since, in order to describe alternative programming paradigms, or reflect compiler's behaviours. In this thesis, we prove another time the fundamental syntactical results of the lambda-calcul: finite developpements, standardisation, normalisation, from axioms on the structure of the calculus: terms, reductions, residuals, nesting orderings, critical pairs. Because it avoids the explicit treatment of any syntax, this abstract description can be applied to aq wide range of calculi, this avoiding to repeat constructions and proofs for every particular language. Furthermore, these axioms capture inside syntax some semantical notions like stability. Apart from this reappropriation of a syntactical tradition, we present a counter-example to the strong normalisation of the typed lambda-sigma-calcul, a lambda-calcul with explicit substitutions. Then we apply our abstract constructions and show that every external or needed strategy of the (untyped) lambda-sigma-calculus is normalising. My PhD is available at http://www.dcs.ed.ac.uk/home/paulm/ -----------------------------------------------------------------------------