Pour obtenir le grade de
212
pages
Français
Documents
2006
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
212
pages
Français
Documents
2006
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
THÈSE Pour obtenir le grade de DOCTEUR DE L'UNIVERSITÉ DE GRENOBLE Spécialité : Informatique Arrêté ministériel : 7 août 2006 Présentée par Alejandro DÍAZ-CARO Thèse dirigée par Pablo ARRIGHI et codirigée par Frédéric PROST préparée au sein du Laboratoire d'Informatique de Grenoble et de l'École Doctorale Mathématiques, Sciences et Technologies de l'Information, Informatique Du typage vectoriel Thèse soutenue publiquement le 23 Septembre 2011, devant le jury composé de : M. Philippe JORRAND Directeur de Recherche Émérite CNRS, HDR, Président M. Eduardo BONELLI Profesor Asociado à l'UNQ et Investigador Adjunto au CONICET, Rapporteur M. Gilles DOWEK Directeur de Recherche INRIA, HDR, Rapporteur M. Thomas EHRHARD Directeur de Recherche CNRS, HDR, Rapporteur M. Michele PAGANI Maître de Conférences à l'Université de Paris Nord, Examinateur M. Laurent REGNIER Professeur à l'Université de la Méditerranée, HDR, Examinateur M. Lionel VAUX Maître de Conférences à l'Université de la Méditerranée, Examinateur M. Pablo ARRIGHI Maître de Conférences à l'Université de Grenoble, HDR, Directeur de thèse
- typage vectoriel
- investigador adjunto au conicet
- linear-algebraic ?-calculus
- extension du ?-calcul
- directeur de la recherche
THÈSE
Pour obtenir le grade de
DOCTEURDEL’UNIVERSITÉDEGRENOBLE
Spécialité : Informatique
Arrêté ministériel : 7 août 2006
Présentée par
AlejandroDÍAZ-CARO
Thèse dirigée parPabloARRIGHI
et codirigée parFrédéricPROST
préparée au sein duLaboratoired’InformatiquedeGrenoble
et de l’École Doctorale Mathématiques, Sciences et Technologies de
l’Information,Informatique
Dutypagevectoriel
Thèse soutenue publiquement le23Septembre2011,
devant le jury composé de :
M.PhilippeJORRAND
Directeur de Recherche Émérite CNRS, HDR, Président
M.EduardoBONELLI
Profesor Asociado à l’UNQ et Investigador Adjunto au CONICET, Rapporteur
M.GillesDOWEK
Directeur de Recherche INRIA, HDR, Rapporteur
M.ThomasEHRHARD
Directeur de Recherche CNRS, HDR, Rapporteur
M.MichelePAGANI
Maître de Conférences à l’Université de Paris Nord, Examinateur
M.LaurentREGNIER
Professeur à l’Université de la Méditerranée, HDR, Examinateur
M.LionelVAUX
Maître de Conférences à l’Université de la Méditerranée, Examinateur
M.PabloARRIGHI
Maître de Conférences à l’Université de Grenoble, HDR, Directeur de thèsea Nache
mi compañera de rutai
Résumé
’objectif de cette thèse est de développer une théorie de types pour le -calcul linéaire-algébrique,
une extension du-calcul motivé par l’informatique quantique. Cette extension algébrique comprendL touslestermesdu-calculplusleurscombinaisonslinéaires, doncsitetrsontdestermes,:t+:r
est aussi un terme, avec et des scalaires pris dans un anneau. L’idée principale et le défi de cette
thèse était d’introduire un système de types où les types, de la même façon que les termes, constituent un
espace vectoriel, permettant la mise en évidence de la structure de la forme normale d’un terme. Cette
thèse présente le système Lineal, ainsi que trois systèmes intermédiaires, également intéressants en
euxCAmême : Scalar, Additive et , chacun avec leurs preuves de préservation de type et de normalisation
forte.
Abstract
heobjectiveofthisthesisistodevelopatypetheoryforthelinear-algebraic-calculus, anextension
of-calculus motivated by quantum computing. This algebraic extension encompasses all the termsT of together with their linear combinations, so ift andr are two terms, so is:t+:r, with
and being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type
system where the types, in the same way as the terms, form a vectorial space, providing the information
about the structure of the normal form of the terms. This thesis presents the system Lineal, and also
CAthree intermediate systems, however interesting by themselves: Scalar, Additive and , all of them
with their subject reduction and strong normalisation proofs.ii
