Ruyer Frédéric

Frédéric Ruyer

Docteur
chercheur associé



Informations diverses

Thèmes de Recherche

Lambda calcul, réalisabilité , logique
classique , sous typage.

circuit electrique

Thèse

Résumé

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Mots-clés: Lambda-Calcul, théorie de la démonstration, typage, sous-typage, réalisabilité, preuve de programmes, langages fonctionnels, types de données, systèmes de modules.

Le manuscrit de ma thèse.

Les fichiers Phox de ma thèse sont disponibles sous la forme d'une archive tarzippée

Publications


Computer assisted teaching in Class situation: a high-school math lab on vectors (avec Maud Marshal, Peggy Provent Pirouz Djoharian et Fabrice Neyret): compte-rendu d'une expérience d'enseignement qui a été l'objet de notre mémoire de monitorat. Soumis et accepté pour les proceedings de la conférence Edutainment'06. computer assisted teaching...

Realizability of the Axiom of Choice in HOL: an analysis of Krivine's work (avec C. Raffalli). Accepté dans la revue Fundamenta Informaticae. Realizability...

Manuscrits


Russel's paradoxes in HOL : sur une idée de C.Raffalli, je donne une nouvelle preuve étonnament simple de l'inconsistance de U- basée sur le paradoxe de Russell, ainsi que deux autres preuves d'inconsistance basées sur le meme principe. les paradoxes

Abstract Datatypes and definite description: un travail exprimant la possibilité de coder les types abstraits et de donner un sens à l'opérateur de projection des types abstraits dans un système de type muni d'un opérateur de description définie. types abstraits

Mon mémoire de DEA (pour le moment, sans les annexes...) memoire de dea

titre:Une application d'un logiciel de démonstration assistée à un résultat d'algèbre.

résumé:

Les transparents de mon intervention à TYPES 2003 version dvi version ps

Les transparents de mon intervention au séminaire PPS (Mars 2008) fichier pdf

Liens

page des liens

Divers



Curriculum vitae: CV

Pour les débutants...: petit manuel de commandes linux

Ma bibliothèque d'articles glanés sur le web: Bibliothèque

Remerciements


Les images qui décorent ce site sont des oeuvres du plasticien-infographe Hugues-Thierry Jouan: site de l'artiste

amazone


Retour au site du LAMA