Searcharxiv⌕ Search

arXiv subjects

Yoan Géran

Publications and source records attributed to Yoan Géran.

2 recordsLinked to original sources

Encoding impredicative hierarchy of type universes with variables

Logical frameworks can be used to translate proofs from a proof system to another one. For this purpose, we should be able to encode the theory of the proof system in the logical framework. The Lambda Pi calculus modulo theory is one of these logical frameworks. Powerful theories such as pure type systems with an infinite hierarchy of universes have been encoded, leading to partial encodings of proof systems such as Coq, Matita or Agda. In order to fully represent systems such as Coq and Lean, we introduce a representation of an infinite universe hierarchy with an impredicative universe and universe variables where universe equivalence is equality, and implement it as a terminating and confluent rewrite system.

cs.LO↗

Keyboards as a new model of computation

We introduce a new formalisation of languages, called keyboards. We consider a set of elementary operations (writing/erasing a letter, going to the right or to the left,...) and we define a keyboard as a set of finite sequences of such operations, called keys. The corresponding language is the set of words obtained by applying some sequence of those keys. Unlike classical models of computation, every key can be applied anytime. We define various classes of languages based on different sets of elementary operations, and compare their expressive powers. We also compare them to well-known classes of languages (Chomsky hierarchy). We obtain a strict hierarchy of languages, whose expressivity is orthogonal to the one of the aforementionned classical models. -- Nous introduisons une nouvelle représentation de langages, les claviers. On se munit d'un ensemble d'opérations élémentaires (ajout, effacement d'une lettre, déplacement à droite, à gauche, ...), et on définit un clavier comme un ensemble de suites finies d'opérations élémentaires, appelées touches. Son langage sera l'ensemble des mots obtenus en appliquant une suite quelconque de touches. Contrairement à des modèles de calcul classiques, toutes les touches peuvent être appliquées à tout moment. En premier lieu nous définissons différentes classes de claviers en faisant varier l'ensemble des opérations élémentaires autorisées, et nous comparons l'expressivité des classes de langages obtenues. Nous comparons également ces classes à la hiérarchie de Chomsky. Nous obtenons que toutes les classes étudiées sont différentes, et nous caractérisons les classes inclues dans les rationnels et les algébriques. L'expressivité des claviers semble orthogonale à celle des modèles évoqués précédemment.

cs.FL↗