Tabareau, Nicolas, 1982-....
VIAF ID: 194052199 ( Personal )
Permalink: http://viaf.org/viaf/194052199
Preferred Forms
Works
Title | Sources |
---|---|
Catégories faibles et structures supérieures afférentes en théorie des types. | |
Confluence d'ordre supérieur et encodage d'univers dans le Logical Framework. | |
A Coq certified translation from an extension of relational algebra for SQL to a nested algebra. | |
Effective aspects : Un modèle monadique et typé pour contrôler l’interférence entre aspects. | |
Etendre la théorie des types à l'aide de modèles syntaxiques. | |
Une étude logique de l’équivalence de programmes. | |
Extending type theory with syntactic models | |
Formalisation et Méta-Théorie de la Théorie des Types. | |
Higher-Order Confluence and Universe Embedding in the Logical Framework | |
Lawvere-Tierney sheafification in Homotopy Type Theory | |
Principles of program verification for arbitrary monadic effects. | |
Réalisabilité classique : nouveaux outils et applications | |
Réductions et approximations linéaires | |
Refactoring functional programs with ornaments | |
Refactorisation de programmes fonctionnels par les ornements. | |
Resource modalities and control in tensorial logic. | |
Signatures et modèles pour la syntaxe et la sémantique opérationnelle en présence de liaison de variables. | |
Une théorie des types avec insignifiance des preuves définitionnelle. | |
Traduction mécanisée et certifiée en Coq d'une algèbre relationnelle étendue pour SQL vers une algèbre imbriquée | |
Typage Bidirectionnel pour le Calcul des Constructions Inductives. | |
A type theoretic approach to weak w-categories and related higher structures | |
A type theory with definitional proof-irrelevance |