La conjecture de Nivat dit que toute configuration (coloration de la grille Z^2) de faible complexité (qui contient moins de mn motifs rectangulaires de taille mxn) est nécessairement périodique. Autrement dit, il est impossible des créer des configuration non périodique avec trop peu peu de motifs différents. En 2015, Michal Szabados et Jarkko Kari ont présenté une nouvelle manière d'approcher cette conjecture à l'aide d'outils algébriques. En représentant les configurations comme des séries formelles, ils parviennent à exploiter la structure de certains idéaux polynomiaux pour obtenir des résultats se rapprochant beaucoup de la conjecture de Nivat. Dans cet exposé je présenterai leur approche et leurs résultats, ainsi que les travaux que j'ai effectué avec Jarkko Kari dans la continuation de ceux de Michal Szabados. En particulier, je présenterai la preuve (ou au moins les grandes lignes) que la conjecture est vraie dans le cas de certains sous-shifts, ainsi que pour les configurations uniformément récurrentes (c'est à dire celles n'ayant pas de motifs isolés).
The speculative ambition of replacing the old theory of program approximation based on syntactic continuity with the theory of resource consumption based on Taylor expansion and originating from the differential λ-calculus is nowadays at hand. Using this resource sensitive theory, we provide simple proofs of important results in λ-calculus that are usually demonstrated by exploiting Scott’s continuity, Berry’s stability or Kahn and Plotkin’s sequentiality theory. A paradigmatic example is given by the Perpendicular Lines Lemma for the Böhm tree semantics, which is proved here simply by induction, but relying on the main properties of resource approximants: strong normalization, confluence and linearity.
TBA
(Joint work with P. LeFanu Lumsdaine.)
Lawvere theories and (coloured) operads provide particularly nice representations for suitable algebraic theories with a given set of sorts, as monoids in certain categories of collections.
We extend this to dependent type theories: For an inverse category C, we show how suitable “C-sorted type theories” may be viewed (1) as monoids in a category of collections, and (2) as generalised Lawvere theories in the sense of Berger–Melliès–Weber. Moreover, (essentially) every dependent type theory arises in this way.
Inverse categories are known from homotopy theory, where they (or their opposite categories) provide a good notion of a category of ``cells''. Examples are the category of semi-simplices, the category of globes, the category of opetopes, etc.
Hypergroups are objects like groups but with addition taking possibly many values. Likewise, hyperrings and hyperfields are objects similar to rings and fields, but with multivalued addition. Hyperfields provide a convenient tool in axiomatizing the algebraic theory of quadratic forms and in this talk we shall focus on three such applications. Firstly, we shall show how Witt equivalence of fields can be conveniently expressed in the language of hyperfields and will present some recent results on Witt equivalence of function fields over global and local fields. Secondly, we shall show how orderings of higher level can be defined for hyperrings and hyperfields, and, consequently, how they can be used to provide an axiomatic framework to study forms of higher order. Finally, we shall define the category of, so called, presentable fields and define their Witt rings, thus providing yet another machinery to study quadratic forms over fields. The results presented in this talk were obtained jointly with Murray Marshall and Krzysztof Worytkiewicz.
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pur et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.
The μ-calculus with atoms, or nominal μ-calculus, is a temporal logic for reasoning about transition systems that operate on data atoms coming from an infinite domain and comparable only for equality. It is, however, not expressive enough to define some properties that are of interest from the perspective of system verification. To rectify this, we extend the calculus with tests for atom freshness with respect to the global history of transitions. Since global histories can grow arbitrarily large, it is not clear whether model checking for the extended calculus is decidable. We prove that it is, by showing that one can restrict attention only to locally relevant parts of the history.
L'exposé se fera en deux temps. Dans la première partie (accessible à tous les membres de l'équipe), je présenterai le lambda-mu-calcul (pure et typé) de Parigot ainsi que ses propriétés et ses défauts. J'introduirai ensuite le lambda-mu-mu'-calcul (version De Groote) et je vous présenterai ses multiples propriétés de normalisation (sans rentrer dans les détails techniques). Dans la deuxième partie, je reprendrai quelques résultats techniques pour présenter les méthodes que nous avons utilisées pour les démontrer.
TBA
L’objectif de ce travail est l’étude algébrique, arithmétique et combinatoire des paires de conjugués des séries à coefficients dans un corps fini, qui sont situés en dehors du cercle unité dont tous les autres conjugués sont á l’intérieur. On s’intéresse principalement à décrire le lien entre les paires des séries de Pisot et leurs constructions. Nous avons montré que les polynômes P(Y) =Yd+Ad−1Yd−1+. . .+A0 ∈ Fq[X][Y] tel que deg(Ad−2)>deg(Ai) pour tout i différent de d−2 et deg(Ad−2)<2 deg(Ad−1) où q différent 2r (r≥1) admet une paire des séries de Laurent. En effet, on étudie la relation entre les polynômes irréductibles, on va prendre à titre d’exemple, le cas des paires des séries des Pisot (ou bien les séries 2-Pisot) tout en déterminant le cardinal de l’ensemble de ces éléments en fonction du degré et de la hauteur logarithmique. Par conséquent, on donne une minoration du nombre des polynômes irréductibles à deux variables sur un corps fini Fq.
This talk will explain the each word in the title separately, and then how they can be combined together. Our problem is how to make coinductive equivalence proofs easier, and in particular how to prove sound enhancements of the bisimulation proof technique (also called up-to techniques). The lingua franca of this talk will be the lambda-calculus.