A gentle introduction to categorical models of dependent type theory. As a warm up, Richard will explain the interpretation in locally cartesian closed categories (LCCCs), and why it necessarily leads to extensional models of type theory. Then, he will, rather informally, try to explain why models of intensional type theory should look like weak omega categories (read the ordinal ``omega'').
La complexité de l'étude formelle des protocoles cryptographique se situe à plusieurs niveaux. Il faut d'abord modéliser les communications qui ont lieu entre les participants, puis définir précisément les propriétés que l'on souhaite vérifier. Celles-ci peuvent être assez simples à exprimer, comme les propriétés de secret, ou très complexes, comme les propriétés de résistance à la coercition dans les protocoles de vote. Le pi-calcul appliqué est de plus en plus utilisé pour formaliser des protocoles cryptographiques. Il étend le pi-calcul traditionnel en permettant aux processus de manipuler aisément des termes dotés d'une théorie équationnelle. On peut par exemple y inclure des primitives pour le chiffrement ou la signature de message, la création de paires de clés privées/publiques, ou toute autre fonction utile pour le protocole à formaliser. Différentes équivalences permettent ensuite de comparer les processus, dont l'équivalence statique qui, intuitivement, exprime ce qu'un attaquant peut déduire d'un protocole à une étape donnée de son exécution. Pour écrire les propriétés à vérifier sur ces protocoles, on a usuellement recours à différentes logiques, telles que les logiques de Hennessy Milner, de Cardelli-Gordon, et de Caires. L'une de ces logiques est la logique spatiale, qui permet de décrire non seulement les communications dont est capable un processus, mais aussi leur localisation au sein de celui-ci. Ceci permet par exemple de distinguer les différents participants d'un protocole. Cette logique apparaît donc comme un point de départ pertinent pour l'étude de protocoles cryptographique. Le but de ce travail était d'adapter la logique spatiale au traitement du pi-calcul appliqué et d'étudier son expressivité, notamment en termes de propriétés de secrets, sécurité, déductibilité, etc. Nous introduirons tout d'abord la logique spatiale du pi-calcul appliqué que nous avons définie, avant de présenter les résultats théoriques d'expressivité obtenus dans ce nouveau cadre (intensionalité, élimination des quantificateurs, ...), qui rejoignent ceux déjà connus pour le pi-calcul. Enfin, nous donnerons quelques intuitions concernant les propriétés de sécurité et de secret qu'il est possible d'exprimer au sein de la logique, notamment en donnant des formules qui caractérisent l'équivalence statique.
Dans cet exposé, nous démontrerons le résultat d'indécidabilité obtenu par R. Berger en 1964 sur les pavages : savoir, étant donné un jeu fini de tuiles de Wang, s'il existe un pavage valide du plan par ces tuiles est indécidable. Après une brève discussion sur différentes façons de définir des jeux de tuiles et les pavages du plan engendrés, nous nous intéresserons à la problématique de l'apériodicité, introduite par H. Wang. Dans l'esprit des constructions originelles de R. Berger et R. M. Robinson, nous construirons un jeu de tuiles apériodique et nous montrerons comment ce jeu de tuiles peut être étendu pour générer les pavages limites de n'importe quelle substitution 2x2. Fort de cette construction, nous pourrons calculer dans les pavages et obtenir les résultats d'indécidabilité annoncés.
In this talk, I will present our work in which we are trying to make a connection between formal and natural languages. We aim to develop tools and resources capable of translating between natural languages and formal languages. I will present our attempts in translating mathematical proofs written in natural language into formal proofs. The implementation of our work is based on the Grammatical Framework (GF). GF is a grammar formalism based on type theory, which provides a special purpose language for defining grammars, and a compiler for this language. Further I will give an overview of the future work i.e. Checking formal software specifications with the specifications written in a natural language and to validate whether they correspond to each other or not. I will also argue that it is a very hard problem to generate a good quality text from a formalism. A natural motivation for this work is the fact that it is a normal practice in industry to write specifications in natural language. In a similar way, all the standards such as RFCs, ISO, ANSI, patents are written in plain natural language. Therefore this resource has an immediate usability in the industry. It will help to overcome the difficulties that prevent software designers & engineers to use formal methods. This Project has its usefulness in formal methods, Human computer interaction, natural language technology and Mathematical teaching.
Inspired by the unanswered question: why eukariotic DNA has a so large non-coding fraction, we try computer simulations with an evolutionary toy model based on Turing machines. This lead us to describe how the fitness of an ``organism'' and the evolution rate relate to the coding/non-coding ratio. The evolutionary advantage of having a large reservoir of non-coding states is emphasised.
En 2004, G. Gonthier a achevé la preuve formelle du théorèmes de quatre couleurs dans l'assistant à la preuve Coq. L'une des clefs de cette réussite est une utilisation intensive de techniques dites de ``réflexion à petite échelle'', soutenues par une extension du langage de tactiques de Coq. Cette extension, ainsi qu'une partie des bibliothèques développées pour la preuve, sont actuellement utilisées comme point de départ pour le projet de formalisation d'une somme substantielle de théorie des groupes finis, dans l'équipe Composants Mathématiques du centre commun INRIA MSR. Il s'agit cette fois de construire une preuve formelle du théorème de Feit-Thompson (1963), qui constitue un passage a l'échelle significatif pour les contributions issues de la preuve du théorèmes des quatre couleurs. Le but de cette expérience est de comprendre comment mener à bien le développement de bibliothèques de mathématiques formalisées, réutilisables et combinables. Nous tenterons d'abord de dégager les difficultés que présente la réalisation de telles bibliothèques, puis de présenter les solutions qui se dégagent de la preuve du théorème des quatre couleurs, et en particulier le langage de tactiques ssreflect. Enfin, si le temps le permet, nous présenterons brièvement les nouvelles questions soulevées par la formalisation de théorie des groupes finis, ainsi que l'état actuel de cette construction.
Pierre Hyvernat (LAMA) prendra environ 1/2h pour poser une question sur laquelle il bute actuellement. Ensuite, séance lecture sur le papier de Krivine et Legrandgérard, téléchargeable ici:
http://www.pps.jussieu.fr/ krivine/articles/Network.pdf.
Résumé du papier: On décrit une relation remarquable entre la notion de formule valide du calcul des prédicats et la spécification de protocoles réseau. On donne des exemples comme l'acquittement d'un ou plusieurs paquets.
Nous proposons une extension du lambda-calcul traditionel dans lequel les termes sont utilisés pour manipuler un artefact de calcul externe (bits quantiques, brins d'ADN etc.). Nous introduisons deux nouveaux lieurs de noms : $nu$ et $rho$. $new x.M$ dénote un terme dans lequel $x$ est une référence abstraite, alors que dans $rho y.M$, $y$ est une référence conrète. Nous montrons les différences de ces deux lieurs par rapport au $lambda$ en termes d'$alpha$ équivalence, d'extrusion, de garbage collection etc. Nous illustrons l'intérêt de ces nouveaux lieurs en développant un langage de programmation quantique typé dans lequel la duplication de qbits abstrait est permise alors que la duplication de qbits concrets est interdite. Cela permet un langage plus expressif que ceux proposés dans la littérature actuelle.
Urdu is a challenging language because of, first, its Perso-Arabic script and second, its morphological system having inherent grammatical forms and vocabulary of Arabic, Persian and the native languages of South Asia. This paper describes an implementation of the Urdu language as a software API, and we deal with orthography, morphology and the extraction of the lexicon. The morphology is implemented in a toolkit called Functional Morphology, which is based on the idea of dealing grammars as software libraries. Therefore this implementation could be reused in applications such as intelligent search of keywords, language training and infrastructure for syntax. We also present an implementation of a small part of Urdu syntax to demonstrate this re-usability.
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.
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.