Dans le cadre du pi calcul, la bisimulation ouverte est une notion d'équivalence attractive car elle offre de bonnes propriétés de congruence et est assez facile à implémenter. Nous proposons une généralisation de cette notion dans le cadre du spi calcul, une extension du pi calcul permettant de raisonner sur les protocoles cryptographiques.
When enriching the lambda-calculus with rewriting, union types may be needed to type all strongly normalizing terms. However, with rewriting, the elimination rule (UE) of union types may also allow to type non normalizing terms (in which case we say that (UE) is unsafe). This occurs in particular with non-determinism, but also with some confluent systems. It appears that studying the safety of (UE) amounts to the characterization, in a term, of safe interactions between some of its subterms. We study the safety of (UE) for an extension of the lambda- calculus with simple rewrite rules. We prove that the union and intersection type discipline without (UE) is complete w.r.t. strong normalization. This allows to show that (UE) is safe if and only if an interpretation of types based on biorthogonals is sound for it.
Une session de travail les 29, 30 Mai au sein du groupe ModCan (Modélisation Cancer) avec Bordeaux (T. Colin, O. Saut), Chambery, Grenoble (Claude Verdier), Lyon (F. Billy, Emmanuel Grenier, Benjamin Ribba), Turin (D. Ambrosi, L. Preziosi) est organisee au LAMA.
Une classe effective dans une variété symplectique de dimension quatre est une classe d'homologie de degré deux qui est réalisée par une courbe J-holomorphe (éventuellement réductible) pour toute structure presque complexe positive sur la forme symplectique. Je montrerai que les classes effectives sont orthogonales aux tores lagrangiens pour la forme d'intersection.
Nous montrerons comment un langage similaire à ML, peut être transformé de manière très simple et minimaliste en un système de déduction où les preuves sont des programmes.
On considère l'équation de Boltzmann pour un gaz à deux composantes lorque le nombre de Knudsen devient petit. Une des 2 composantes satisfait à des conditions de bord de type données aux bords rentrantes et l'autre composante satisfait à des conditions de bord de type Maxwell diffuses. La solution du problème est alors rechechée sous la forme d'un développement asymptotique de type Hilbert avec un reste contrôlé.
Soit W -> X une variété projective non singulière réelle de dimension 3 fibrée en courbes rationnelles. On suppose que W(R) est orientable. Soit M une composante connexe de W(R). D'après Kollár, M est alors essentiellement une variété de Seifert ou une somme connexe d'espaces lenticulaires. Soit n un entier définit de la façon suivante : Si g : M -> F est une fibration de Seifert, on note n le nombre de fibres multiples de g. Si M est une somme connexe d'espaces lenticulaires, on note n le nombre d'espaces lenticulaires.
Théorème
Lorsque X est une surface géometriquement rationnelle, n est majoré par 4.
Ce résultat répond par l'affirmative à une question de Kollár qui avait montré en 1999 que n était majoré par 6. On déduit ce théorème d'une analyse fine de certaines surface de Del Pezzo singulières avec singularités Du Val.
Considérez la suite (ordonnée) de fractions suivante: 17/91 78/85 19/51 23/38 29/33 77/29 95/23 77/19 1/17 11/13 13/11 15/2 1/7 55/1. Partez de l'entier 2 et à chaque étape multipliez l'entier courant par la première fraction pour laquelle le produit est entier et répétez le processus. Les puissances de 2 que vous obtenez sont exactement les 2^p où p est premier. C'est un simple exemple de programme d'un langage de programmation universel: FRACTRAN. Après avoir expliqué en quoi FRACTRAN est une présentation originale et concise de modèles de calculs bien connus, nous montrerons deux résultats d'indécidabilité sur les problèmes de Collatz généralisés qui sont des corollaires faciles de l'universalité de FRACTRAN. Tout ces résultats sont tirés d'un article de Conway de 86.
On connaît les homomorphismes de monoïdes, de groupes, mais qu'est-ce qu'un homomorphisme de logiques ? Pour répondre à cette question, nous avons introduit avec Christian Lair en 2002 la notion de "propagateur", qui est définie de façon très simple à partir des "esquisses" de Charles Ehresmann. Le but de l'exposé est de présenter les esquisses et les propagateurs, et de montrer comment un propagateur définit une "logique", avec des modèles et un système de preuves, apparentée aux "doctrines" de William Lawvere. La définition des homomorphismes de logiques est alors évidente. Je parlerai aussi d'une application à la sémantique des effets de bord dans les langages de programmation, qui constitue ma motivation initiale pour ces travaux. Les quelques notions de théorie des catégories nécessaires à la compréhension de tout cela seront rappelées dans l'exposé.
Un polytope convexe d'un espace euclidien est régulier si son groupe d'isométries agit transitivement sur l'ensemble de ses drapeaux. Depuis Schläfli (1901), on sait classifier ces polytopes réguliers. Si on suppose que le polytope est à sommets entiers, ou plus généralement sur un réseau, on peut définir les polytopes réguliers relativement au groupe préservant ce réseau (les polytopes Z-réguliers). Récemment Karpenkov a donné une classification de ces polytopes Z-réguliers utilisant la classification de Schläfli. Dans un travail en commun avec Pierre-Louis Montagard, nous retrouvons ce résultat en associant à chaque polytope Z-régulier un système de racines.
In this talk, I will present an intersection type system for Curien Herbelin symmetric lambda calculus, that has been developed in the joint work with Dan Dougherty and Pierre Lescanne. The system completely characterizes strong normalization of the free (unrestricted) reduction. The proof uses a technique based on fixed points. The system enjoys subject reduction and subject expansion.
Http://www.cmap.polytechnique.fr/ mechkour/