Je présente la preuve de Prawitz de la faible normalisation de l'élimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction. On déduit ensuite la propriété de la sous-formule et la décidabilité de ce système. Il s'agit du travail fait lors de mon stage M1.
On présentera (il s'agit d'un travail commun avec Olivier Laurent) une version "pure" (au sens du lambda-calcul "pur") des réseaux d'interaction différentiels avec connecteurs multiplicatifs et exponentiels, et on donnera une traduction dans ces réseaux du pi-calcul privé - de la somme - de la récursion - de la réplication - du match et du mismatch On verra que cette traduction respecte, en un certain sens, la dynamique du pi-calcul.
Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. La preuve que cette représentation satisfait les propriétés de base de la substitution - dictées par la théorie de catégories - n'est pas triviale et un travail assez récent (pour Coq, c'était fait par Adams). On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite. Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont pas offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique. Heureusement, la vérification entière des propriétés de base était abordable dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet.
Le lambda-mu-&-or-calcul est une extension du lambda-calcul associée à la déduction naturelle classique où sont considérés tous les connecteurs. Les principaux résultats de cette thèse sont : - La standardisation, la confluence et une extension de la machine de J.-L. Krivine en lambda-mu-&-or-calcul. - Une preuve sémantique de la forte normalisation du théorème d'élimination des coupures. - Une sémantique de réalisabilité pour le lambda-mu-&-or-calcul qui permet de caractériser le comportement calculatoire de certains termes typés et clos. - Un théorème de complétude pour le lambda-mu-calcul simplement typé. - Une introduction à un lambda-mu-&-or-calcul par valeur confluent.
Call-by-name lambda-mu-calculus was proved observationally incomplete by David and Py. Still, Saurin showed that an apparently inoffensive extension of the reduction rules allows to recover Böhm completeness back. We show that this extension corresponds to adding a simple form of exception handler that is commonly called control delimiter. Control operators with delimiters have been studied by Felleisen and by Danvy and Filinski. Typically, Filinski showed that all concrete monads (e.g. references, exceptions, non-determinism, ...) are expressible in call-by-value lambda-calculus with delimited control. This result translates to the case of call-by-value lambda-mu-calculus and suggests that side-effects could be smoothly integrated to the Curry-Howard correspondence.
Language designers for object-oriented languages have tended to use classes as the main modularity boundaries for code. While Java includes packages, they were not particularly well thought-out and have many flaws. However, the designers got very few complaints for the weak design because programmers don't use them very effectively. In this talk we describe some useful properties of modularity and information-hiding mechanisms in object-oriented languages and and present a language design that supports these properties.
This talk considers logical formulas built on the single binary connector of implication and a finite number of variables. When the number of variables becomes large, we prove the following quantitative results: {\em asymptotically, all classical tautologies are \textit{simple tautologies}}. It follows that {\em asymptotically, all classical tautologies are intuitionistic}. We investigate the proportion between the number of formulas of size $n$ that are tautologies against the number of all formulas of size $n$. After isolating the special class of formulas called simple tautologies, of density $1/k+O(1/k2)$, we exhibit some families of non-tautologies whose cumulated density is $1-1/k-O(1/k2)$. It follows that the fraction of tautologies, for large $k$, is very close to the lower bound determined by simple tautologies. A consequence is that classical and intuitionistic logics are close to each other when the number of propositional variables is large.
This talk presents numerous results from the area of quantitative investigations in logic and type theory. For the given logical calculus (or type theory) we investigate the proportion of the number of distinguished set of formulas (or types) $A$ of a certain length $n$ to the number of all formulas of such length. We are especially interested in asymptotic behavior of this fraction when $n$ tends to infinity. The limit $\mu(A)$ if exists, is an asymptotic probability of finding formula from the class $A$ among all formulas or the asymptotic density of the set $A$. Often the set $A$ stands for all tautologies of the given logical calculus (or all inhabited types in type theory). In this case we call the asymptotic of $\mu(A)$ the \emph{density of truth}. Most of this research is concern with classical logic and sometimes with its intuitionistic fragments but there are also some attempts to examine modal logics. To do that we use methods based on combinatorics, generating functions and analytic functions of complex variable with the special attention given to singularities regarded as a key determinant to asymptotic behavior.
Nous nous intéressons dans cet exposé au problème suivant : nous considérons une triangulation T_n qui converge au sens de Hausdorff et en normales vers une surface S régulière de classe C^2. Sur chaque triangulation T_n nous considérons une courbe géodésique C_n qui converge vers une courbe C de S. Il est alors naturel de se demander si C est une géodésique de S. Dans le cas où C_n est un plus court chemin, il est connu que C est aussi un plus court chemin. Nous allons montrer que ce résultat ne tient plus si l'on suppose que C_n est une géodésique sans être un plus court chemin. Cependant, en faisant des hypothèses supplémentaires sur la vitesse de convergence des normales et sur les longueurs des arêtes, il est possible de garantir que la courbe limite C est une géodésique. Ce travail peut ensuite s'appliquer à certains schémas de subdivision. Il permet ainsi de valider un algorithme existant de V. Pham-Trong et al. en 2001, qui permet de calculer des géodésiques (qui ne sont pas forcément des plus court chemins) sur une suite de surfaces de subdivision.
In this talk we try to attack the problem of programming Graphical User Interfaces in a manageable way. User interfaces are an area where traditional, imperative programming techniques lead to unstructured and error prone code. As an antidote for that, many alternative computation models have been proposed, of which the synchronous dataflow model will be our theme. We present a functional GUI toolkit, based on the above model, which does not have many of the drawbacks of traditional toolkits. The toolkit is implemented in Haskell, a functional language which provides a handy base for creating domain-specific languages.
Proof General is a generic proof development environment which has been in use for almost 10 years, providing interface support for interactive theorem prover systems such as Isabelle, LEGO, Coq and PhoX. Recently, a new version has been introduced, called Proof General Kit, which is based on a component framework that is designed to enable much richer interactions, including special manipulations for "Proof Engineering". We see the challenge of Proof Engineering as being necessary to take interactive theorem proving to the next level. Proof Engineering, like Software Engineering, considers the lifecycle of large proof developments. It will provide facilities for the construction, maintenance, and comprehension of large proofs. We want to provide foundations and tools to support Proof Engineering at a generic level, within the Proof General Kit framework. This talk will introduce the Proof General Kit and Proof Engineering. I will explain some of the research problems and early solution ideas for our research programme and explain how they relate to underlying proof assistant engines. The presentation will be at a high level and not overly technical.
Adverbial inferences, such as that from "he ran quickly" to "he ran", have raised serious problems for the semantics of natural language. Traditionally -- at any rate since Davidson's work -- these inferences have been handled with a first-order formalisation using individual events. This is not without problems: there is, for example, very little consensus about conditions of identity for events. I propose an alternative, higher order semantics, using two categories, and I will discuss its implications for the semantics of such sentences.
I report on work in progress concerning the development of a natural language parser. On the one hand I discuss how a call-by-value lambda-mu-calculus endowed with labels can be used to provide a Montague semantics for natural language and how events can be exploited in order to deal with linguistic phenomena such as adverbs. On the other hand I explain how a type-driven parser can be obtained by enriching the type system with morphosyntactic and grammatical features.
Les automates cellulaires sont souvent construits et étudiés pour adopter un comportement précis. On adopte ici un point de vue opposé en s'intéressant aux comportements typiques parmi l'ensemble des AC ou de manière équivalente au comportement des AC aléatoires. A l'aide de méthodes combinatoires variées, et de la complexité de Kolmogorov, on obtient des résultats sur la probabilité de certaines propriétés dynamiques des AC.
Comessatti a démontré qu'une surface rationnelle réelle est soit non orientable, soit difféomorphe à une sphère ou un tore. Réciproquement, si S est une surface non orientable ou difféomorphe à une sphère ou un tore, il existe une surface rationnelle réelle X difféomorphe à S. Dans cet exposé on démontre que si Y est une autre surface rationnelle réelle difféomorphe à S, alors X et Y sont biregulièrement isomorphes. Autrement dit, les surfaces non orientables, la sphère et le tore ont exactement un seul modèle algébrique rationnel réel à isomorphisme birégulier près.
Le travail présenté introduit une nouvelle approche pour la composition automatique de buts en planification en considérant les buts comme des fonctions de leur contexte (i.e., à partir de structures de connaissances sur le domaine). Etant donné un but global et une situation initiale, le modèle de planification peut être généré directement à partir d'un ensemble de buts primitifs via la connaissance du domaine et le raisonnement sur les types de buts. La connaissance sur le domaine est extraite d'une ontologie locale, sélectionnant les entités disponibles et leurs relations. Un processus de raisonnement valide ces informations via un theorem prover en théorie intuitionniste des types (ITT). L'approche proposée bénéficie de l'efficacité du theorem prover à travers ITT combinée à l'expressivité sémantique des ontologies. La representation des connaissances utilise les types d'enregistrements dépendants pour décrire à la fois les types de contextes du domaine et des structures intentionnelles décrivant une action, le but à réaliser et ses effets. Les types d'enregistrements dépendants capturent une connaissance partielle du domaine et possèdent un impact computationnel immédiat.
Cet exposé traitera de l'existence de solutions fortes pour Navier-Stokes compressible isotherme dans des espaces de Besov critiques pour le scaling du système. On montrera notamment l'existence de solutions fortes pour des données à indices de régularité négatifs. De plus cet exposé fera un lien avec le système de type Korteweg c'est à dire avec un terme de capillarité.
On borne le nombre de points fixes d'un automorphisme d'une courbe algébrique réelle en fonction du genre de la courbe et du nombre de composantes connexes de la partie réelle de la courbe. On utilise cette borne pour calculer l'ordre maximum de certains groupes d'automorphismes de courbes algébriques réelles.