The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2022, 2023, all years together.

Year 2007

Friday 21st December 2007 at 10h Dragisa Zunic (ENS Lyon),
Soutenance de thèse

Abstract: (Hide abstracts)
TBA

Thursday 20th December 2007 at 10h Projet Choco (ANR),
Journée interne projet Choco

Abstract: (Hide abstracts)
10h - 12h Samuel Mimram (PPS, Paris 7), Sémantiques de jeux asynchrones
14h - 15h30 Marc de Falco (IML, Marseille), Géometrie de l'interaction des réseaux différentiels et application à l'étude des π-termes
15h30 - 17h Auélien Pardon (LIP, ENS Lyon), Une approche algébrique et modulaire de la syntaxe avec lieurs

Abstract available as a PDF file.

Thursday 13th December 2007 at 10h15 Stefano Berardi (Turin),
A computational interpretation of classical proofs through parallel computations

Abstract: (Hide abstracts)
We argue in favor of the following thesis: there is an intric link between the computation we can unwing from classical proofs and parallel computations. We introduce a model for computations extracted from classical proofs based on parallel computations and on the concept of learning in the limit. The aim of our research is designing parallel extensions of the existing continuation languages.

Wednesday 12th December 2007 at 14h Peter Battyanyi (LAMA),
Normalization properties of symmetric logical calculi

Abstract: (Hide abstracts)
Dans les années quatre-vingt-dix, on a remarqué ce que l'isomorphisme de Curry-Howard peut être étendu à la logique classique. De nombreux calculs ont été développés pour constituer la base de cette extension. On étudie dans cette thèse quelques uns de ces calculs.
On étudie tout d’abord le lambda-mu-calcul simplement typé de Parigot. Parigot a prouvé par des méthodes sémantiques que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte de ce calcul avec la règle mu' (règle duale de mu). Cependant, si l'on ajoute au lambda-mu-mu'-calcul la règle de simplification rho, la normalisation forte est perdue. On monte que le mu-mu'-rho-calcul non-typé est faiblement normalisable et que le lambda-mu-mu'-rho-calcul typé est aussi faiblement normalisable. De plus, on examine les effets d'ajouter quelques autres règles de simplification. On établit ensuite une borne de la longueur des séquences de réduction en lambda-mu-rho-theta-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le lambda-calcul simplement typé. Enfin, on présente une preuve arithmétique de la normalisation forte du lambda-calcul symétrique de Berardi et Barbanera.

Wednesday 12th December 2007 at 10h Ralph Matthes (CNRS, IRIT),
Substitution - des solutions surprenantes avec des familles inductives

Abstract: (Hide abstracts)
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. Cette représentation satisfait les propriétés de base de la substitution, dictées par la théorie des catégories. C'est bien connu.
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 (une forme de substitution explicite). Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont 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 se fait 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. En plus, toute notre théorie axiomatique est justifiée dans le calcul des constructions inductives avec insignifiance des preuves.

Thursday 6th December 2007 at 10h15 Jacques-Olivier Lachaud (LAMA),
Estimation robuste de courbure

Abstract: (Hide abstracts)
We introduce a new curvature estimator based on global optimisation. This method called Global Min-Curvature exploits the geometric properties of digital contours by using local bounds on tangent directions defined by the maximal digital straight segments. The estimator is adapted to noisy contours by replacing maximal segments with maximal blurred digital straight segments. Experimentations on perfect and damaged digital contours are performed and in both cases, comparisons with other existing methods are presented.

Thursday 22nd November 2007 at 10h15 Francesco Zappa-Nardelli -- Annulé (INRIA Rocquencourt),
Oracle Semantics for Concurrent Separation Logic

Abstract: (Hide abstracts)
We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine.

Thursday 15th November 2007 at 10h15 Thomas Fernique (LIRMM),
Reconnaissance de plan et fractions continues

Abstract: (Hide abstracts)
Une manière de stocker de manière économe un gros objet géométrique discret (images 3D acquises expérimentalement etc.) est de le vectoriser. Une façon de procéder est de le décomposer en plans discrets (approximations de plans euclidiens). Pour cela, un problème crucial est celui de la reconnaissance de plan : déterminer si un ensemble discret est ou non inclus dans un plan discret. Nous présentons une approche originale, qui généralise une approche similaire pour le cas de la reconnaissance de droites. Plus précisément, on montre comment calculer un développement en fraction continues multi-dimensionnel du vecteur normal d'un plan discret simplement en lisant les configurations locales de ce plan. Ce procédé peut alors être étendu à des ensembles discrets plus généraux, bien qu'ils n'aient pas forcément de vecteur normal. Les développements de plans possèdent cependant des propriétés qui permettent finalement de les reconnaître.

Thursday 8th November 2007 at 11h Alexandre Miquel (PPS, Paris 7),
L'effectivité expérimentale de la preuve mathématique

Abstract: (Hide abstracts)
La correspondance de Curry-Howard permet d'interpréter chaque démonstration mathématique comme un programme réalisant une certaine spécification (déduite de la formule démontrée). Mais que se passe-t-il quand la démonstration fait appel à des hypothèses expérimentales - par exemple des lois de la physique?

Dans cet exposé, je me propose d'étudier la frontière entre le raisonnement mathématique et les hypothèses empiriques sur lesquelles reposent les sciences expérimentales. Pour cela, je partirai d'un problème soulevé par le philosophe et épistémologue Karl R. Popper lié à l'utilisation des formalismes mathématiques les plus abstraits dans un cadre empirique. Je montrerai alors comment les techniques modernes de réalisabilité permettent de résoudre ce problème, et suggèrent ainsi des pistes inédites pour combiner de manière effective le raisonnement mathématique avec les protocoles expérimentaux.

Thursday 25th October 2007 at 10h30 Richard Garner (Uppsala),
Categorical models of dependent type theory

Abstract: (Hide abstracts)
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'').

Friday 19th October 2007 at 10h30 Jules Villard (LSV (ENS Cachan)),
Une logique spatiale pour le pi-calcul appliqué

Abstract: (Hide abstracts)
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.

Thursday 18th October 2007 at 10h15 Nicolas Ollinger (LIF),
Pavages: de l'apériodicité à l'indécidabilité

Abstract: (Hide abstracts)
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.

Abstract available as a PDF file.

Monday 15th October 2007 at 10h Muhammad Humayoun (LAMA),
Certified software specifications and Mathematical Proofs in Natural Languages

Abstract: (Hide abstracts)
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.

Thursday 11th October 2007 at 10h15 Giovanni Feverati (Laboratoire d'Annecy-le-Vieux de Physique Théorique),
An evolutionary model with Turing machines

Abstract: (Hide abstracts)
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.

Friday 5th October 2007 at 10h15 Assia Mahboubi (INRIA/ Microsoft Research),
Réflexions sur les preuves formelles en Coq

Abstract: (Hide abstracts)
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.

Thursday 27th September 2007 at 10h15 Pierre Hyvernat groupe de lecture (LAMA),
Une question de Pierre + Curry-Howard et les protocoles

Abstract: (Hide abstracts)
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.

Thursday 20th September 2007 at 10h15 Frédéric Prost (LIG (équipe CAPP)),
Traitement de la non-compositionalité dans un langage de programmation fonctionel quantique

Abstract: (Hide abstracts)
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.

Thursday 12th July 2007 at 11h30 Humayoun Muhammad
Urdu Morphology, Orthography and Lexicon Extraction

Abstract: (Hide abstracts)
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.

Thursday 12th July 2007 at 10h15 Jean Quilbeuf
Elimination des coupures en déduction naturelle propositionnelle intuitionniste avec disjonction.

Abstract: (Hide abstracts)
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.

Friday 6th July 2007 at 15h Thomas Ehrhard
Traduction d'un pi-calcul finitaire et polyadique dans les réseaux d'interaction différentiels

Abstract: (Hide abstracts)
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.

Friday 6th July 2007 at 14h Ralph matthes
Substitution - des défis surprenants avec des familles inductives

Abstract: (Hide abstracts)
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.

Friday 6th July 2007 at 10h Khelifa Saber
Soutenance de sa thèse

Abstract: (Hide abstracts)
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.

Thursday 5th July 2007 at 15h Hugo Herbelin (INRIA Futurs),
The hidden exception handler of Parigot's lambda-mu-calculus and its completeness properties

Abstract: (Hide abstracts)
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.

Abstract available as a PDF file.

Thursday 5th July 2007 at 10h15 Kim Bruce (Pomona College),
Modularity and Scope in Object-Oriented Languages

Abstract: (Hide abstracts)
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.

Wednesday 4th July 2007 at 14h M Zaionc
Classical and intuitionistic logic are asymptotically identical

Abstract: (Hide abstracts)
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.

Wednesday 4th July 2007 at 10h15 M Zaionc
Asymptotic densities in logic

Abstract: (Hide abstracts)
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.

Thursday 28th June 2007 at 10h15 Michał Pałka
Functional Graphical User Interfaces 151 An Implementation based on GTK

Abstract: (Hide abstracts)
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.

Thursday 21st June 2007 at 10h15 David Aspinall
The Future of Proof Engineering with Proof General

Abstract: (Hide abstracts)
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.

Friday 15th June 2007 at 10h30 Graham White
The Semantics of Adverbial Inference

Abstract: (Hide abstracts)
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.

Friday 15th June 2007 at 09h Kurt Ranalter
Continuations, events, and natural language

Abstract: (Hide abstracts)
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.

Thursday 14th June 2007 at 10h15 Laurent Boyer
Densité de propriétés sur les automates cellulaires

Abstract: (Hide abstracts)
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.

Thursday 7th June 2007 at 14h Richard Dapoigny
Vers une planification basée sur une Théorie Constructive des Types en logique Intuitionniste. ATTENTION : C'EST A 14 H

Abstract: (Hide abstracts)
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.

Friday 1st June 2007 at 10h15 Sébastien Briais
Une bisimulation ouverte pour le spi calcul

Abstract: (Hide abstracts)
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.

Thursday 31st May 2007 at 10h15 Colin Riba (LORIA),
Strong Normalization and Union Types

Abstract: (Hide abstracts)
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.

Thursday 10th May 2007 at 10h15 Christophe Raffalli
Les preuves en PML

Abstract: (Hide abstracts)
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.

Thursday 19th April 2007 at 10h15 Guillaume Theyssier (Univ. Savoie),
Fractran

Abstract: (Hide abstracts)
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.

Thursday 5th April 2007 at 10h15 Dominique Duval (UJF),
Homomorphismes de logiques

Abstract: (Hide abstracts)
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é.

Thursday 29th March 2007 at 10h Silvia Ghilezan (University of Novi Sad),
Characterizing strong normalization in the Curien Herbelin

Abstract: (Hide abstracts)
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.

Thursday 22nd March 2007 at 10h15 Julien Narboux
Formalisation et automatisation du raisonnement géométrique en Coq

Abstract: (Hide abstracts)
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.

Thursday 15th March 2007 at 10h15 Francois Lamarche (LORIA),
Sémantiques symétriques des preuves en logique propositionnelle classique

Abstract: (Hide abstracts)
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.

Tuesday 13th March 2007 at 10h15 Lionel Vaux (IML),
λ-calcul algébrique

Abstract: (Hide abstracts)
On propose une extension naturelle du λ-calcul autorisant la formation de combinaisons linéaires de termes. Ceci reflète dans la syntaxe la sémantique quantitative du λ-calcul simplement typé dans les espaces de finitude, où les types sont interprétés par des espaces vectoriels particuliers, et les λ-termes par des fonctions entre ces espaces.
On étudie les effets de la présence de coefficients scalaires sur la réduction: après avoir étendu la β-réduction en une relation contextuelle et confluente, on s'intéresse à la cohérence du calcul et à des propriétés de normalisation dans un cadre typé.
On établit enfin une correspondance entre ce λ-calcul algébrique et le λ-calcul linéaire-algébrique d'Arrighi et Dowek en montrant qu'ils correspondent à deux stratégies de réduction (par nom et par valeur) d'une syntaxe commune.

Thursday 8th March 2007 at 10h15 Lionel Vaux
Un lambda-bar-mu calcul avec produit de convolution sur les piles

Abstract: (Hide abstracts)
On présente une extension du lambda-bar-mu calcul de Herbelin avec une opération binaire sur les piles (ou contextes), qui peut aussi être interprétée comme un opérateur de choix non déterministe. Les règles de réduction associées dotent cette opération de propriétés similaires à celles du produit de convolution sur les distributions. C'est la version lambda-calculesque d'une extension par polarisation des réseaux d'interaction différentiels d'Ehrhard-Régnier: on met ce fait en évidence grâce à une sémantique dénotationnelle dans la catégorie des ensembles et relations.

Thursday 1st March 2007 at 10h15 Alexandre Miquel
Un lambda-calcul avec constructeurs

Abstract: (Hide abstracts)
Dans cet exposé, je présenterai une extension du lambda-calcul dans laquelle le filtrage s'effectue à l'aide d'une construction "case" (analyse par cas au sens du langage Pascal) se propageant à travers les fonctions comme une substitution linéaire de tête. Je montrerai en particulier que cette présentation du filtrage permet de récupérer toute l'expressivité du filtrage à la ML (avec des constructeurs non constants) et même plus. Ensuite, je présenterai la preuve du théorème de Church-Rosser, basée sur une technique inédite de "divide and conquer" dans laquelle on détermine de manière semi-automatique l'ensemble des paires de sous-systèmes qui commutent (en considérant toutes les combinaisons possibles des 9 règles de réduction primitives). Enfin, je montrerai que le calcul vérifie une propriété de séparation (non typée) dans l'esprit du théorème de Böhm.

Thursday 22nd February 2007 at 10h Louis Mandel
Programmation réactive en Caml : Implantation de ReactiveML

Abstract: (Hide abstracts)
ReactiveML est un langage de programmation dédié à la programmation de systèmes réactifs (e.g., simulation de systèmes dynamiques, interfaces graphiques, jeux video). Il est fondé sur le modèle "réactif synchrone" introduit par F. Boussinot. Ce modèle permet de combiner les principes de la programmation synchrone (composition parallèle synchrone de processus, communication par diffusion) et des mécanismes de création dynamique. Le langage est une extension conservative de Ocaml. Il ajoute des constructions supplémentaires pour décrire les comportements temporels des systèmes. Les programmes sont statiquement typés puis traduits en Ocaml. La première partie de cet exposé sera consacrée à la présentation du langage. La seconde partie présentera son implantation.

Thursday 15th February 2007 at 14h R Kervarc
Soutenance de sa thèse

Abstract: (Hide abstracts)

Thursday 8th February 2007 GDR IM
Journées Logique, Algèbre et Calcul du GDR IM

Abstract: (Hide abstracts)
Les 8 et 9 Février 2007 auront lieu, à Chambéry, les rencontres du groupe LAC du GDR IM. Plus d'info sur la page de ces journées : www.lama.univ-savoie.fr/~david/gdr/journees.html

Thursday 8th February 2007 — Friday 09 february 2007
Groupe de Travail LAC du DGR IM

Abstract: (Hide abstracts)

Thursday 1st February 2007 at 11h Groupe de lecture topos
Sous-faisceaux dans les topologies de Grothendieck

Abstract: (Hide abstracts)
Sous-faisceaux dans les topologies de Grothendieck et si on a le temps topologies de Lawvere-Tierney

Thursday 25th January 2007 at 10h15 Pierre Lescanne
Jeux, équilibres et réseaux de régulation de gènes

Abstract: (Hide abstracts)
La théorie des jeux peut être vue comme la théorie des équilibres. Comme elle est un peu plus que cinquantenaire, il peut sembler opportun de la réexaminer. C'est ce que nous faisons en proposant une nouvelle vision plus générale que nous appelons 171jeux à conversion-préférence187, en abrégé 171jeux CP187. Ce formalisme semble s'adapter agréablement aux réseaux de régulation de gênes.

Thursday 18th January 2007 at 14h Radu Mateescu (INRIA Rhône Alpes),
MCL: A Model Checking Language for Concurrent Value-Passing Systems

Abstract: (Hide abstracts)
Model checking is a successful technique for verifying automatically temporal properties of concurrent finite-state programs represented as Labelled Transition Systems (LTSs). Among the various formalisms used for specifying properties, an outstanding candidate is the modal mu-calculus, a very powerful fixed point-based temporal logic. However, in spite of its theoretical expressiveness, standard modal mu-calculus is a too low-level formalism for end-users, making the specification of complex properties tedious and error-prone. In this talk, we propose MCL (Model Checking Language), an extension of the modal mu-calculus with high-level, data-based constructs inspired from programming languages, which substantially increase its expressive power as well as the conciseness and readability of properties. We also present an on-the-fly model checking method for verifying MCL formulas on LTSs, based upon translating the verification problem into the resolution of a boolean equation system. The MCL language and the associated verification method are supported by the EVALUATOR 4.0 model checker, developed within the CADP verification toolbox using the generic OPEN/CAESAR environment for on-the-fly exploration of LTSs.

Thursday 18th January 2007 at 10h15 Guillaume Melquiond
De l'arithmétique d'intervalles à la certification de programmes

Abstract: (Hide abstracts)
Parce que les nombres manipulés en machine ont généralement un domaine et une précision limités, il est nécessaire de certifier soigneusement que les applications les utilisant se comportent correctement. Réaliser une telle certification à la main est un travail propice à de nombreuses erreurs. Les méthodes formelles permettent de garantir l'absence de ces erreurs, mais le processus de certification est alors long, fastidieux et généralement réservé à des spécialistes. Le travail présenté dans cet exposé vise à rendre ces méthodes accessibles en automatisant leur application. L'approche adoptée s'appuie sur une arithmétique d'intervalles accompagnée d'une base de théorèmes sur les propriétés des arithmétiques approchées et d'un mécanisme de réécriture d'expressions permettant le calcul de bornes fines sur les erreurs d'arrondi. Ce travail s'est concrétisé par le développement de l'outil Gappa d'aide à la certification. Il permet de vérifier les propriétés de codes numériques qui utilisent de l'arithmétique à virgule fixe ou à virgule flottante. Cette vérification s'accompagne de la génération d'une preuve formelle de ces propriétés utilisable par l'assistant de preuves Coq. Cette preuve s'appuie sur une bibliothèque de propriétés arithmétiques et elle contient principalement des calculs entiers qui reflètent les calculs par intervalles effectués par l'outil. Cependant, pour que la preuve soit d'une taille raisonnable, Gappa élimine les lemmes inutiles et simplifie les nombres que Coq aura à manipuler. Gappa a été utilisé avec succès pour certifier la correction de fonctions dans les bibliothèques CRlibm, CGAL et FLIP par exemple.

Thursday 11th January 2007 at 10h15 G Lafitte
Du calcul à l'incomplétude

Abstract: (Hide abstracts)
Nous parlerons de calculabilités généralisées permettant de définir de nouvelles complexités à la Kolmogorov-Chaitin et de préciser les liens entre incomplétude et calcul.

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2022, 2023, all years together.