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.
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.
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.
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.
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.
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é.
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.
Je présenterai d'abord un développement formel à propos des fondements de la géométrie. Celui-ci consiste en la formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie. Ensuite, je décrirai l'implantation en Coq d'une procédure de décision pour la géométrie affine plane: la méthode des aires de Chou, Gao et Zhang. Dans la troisième partie, nous nous intéresserons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof (http://home.gna.org/geoproof/). GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq. Enfin, je presenterai un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.
Nous savons maintenant qu'il existe dans la nature des modèles de la logique classique qui sont aux catégories ce que les algèbres de Boole sont aux ensembles ordonnés. Durant des années on a cru que de tels êtres ne pouvaient exister, étant donné le célèbre 171 paradoxe de Joyal 187 : une catégorie cartésienne fermée ne peut être équipée d'une négation symétrique. Les premiers exemples étaient des catégories de réseaux de démonstrations. Nous avons ensuite construit des sémantiques dénotationnelles pour la logique classique qui ressemblent beaucoup aux espaces cohérents. L'exposé se concentrera sur les propriétés essentielles que tous ces modèles possèdent, en d'autres termes sur les raisons pour quoi ça marche. Ces modèles nous mènent à nous poser des questions sur l'universalité de l'isomorphisme de Curry-Howard : il existe des façons de dénoter des preuves en logique classique pour lesquelles le processus de normalisation ne correspond pas au calcul en programmation fonctionnelle. Les connaissances en théorie des catégories que nous supposons de la part de l'autitoire sont absolument minimales : les définitions de catégorie, foncteur et transformation naturelle.