Incrementality and effect simulation in the simply typed lambda calculus

Lourdes del Carmen Gonzalez Huesca 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Résumé : La programmation certifiée offre un cadre dans lequel tout programme est correct par construction. Les assistants de preuve et les langages de programmation avec types dépendents sont les représentants de ce paradigme, où la prévue et l’implementation d’un programme sont faites au même temps. Toutefois, il existe certaines limitations : un programme écrit en théorie des types est construit seulement avec des fonctions pures et totales. Notre objectif est d’écrire des programmes efficaces et certifiés. Les contributions de cette thèse sont la formalisation, dans le lambda calcul simplement typé, de deux mécanismes pour améliorer l’efficacité : la validation des calculs impurs et l’optimisation des calculs incrémentaux. Un calcul impur, c’est-à-dire un programme avec effets, et sa validation dans un langage fonctionnel et total est fait á l’aide d’une simulation a posteriori. La simulation est effectuée après, par une procédure monadique et elle est guidée par une prophétie. Un oracle efficace est responsable de la production des prophéties et lui est en fait, la procédure monadique traduite dans un language de programmation généraliste. La deuxième contribution est une optimisation pour les calculs incrémentaux. L’incrémentalité consiste à propager des changements des entrées en changements des sorties, elle est guidée par les descriptions formelles du changement des termes et une différenciation dynamique des fonctions. La représentation des changements de données est pris en charge par les types déplaçables et une extension du lambda calcul simplement typé avec dérivées et dérivées partielles offre un language pour raisonner sur l’incrementalité.
Type de document :
Thèse
Computer Science [cs]. Universite Paris Diderot-Paris VII, 2015. English
Liste complète des métadonnées

Littérature citée [115 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/tel-01248531
Contributeur : Lourdes del Carmen González Huesca <>
Soumis le : lundi 4 janvier 2016 - 23:58:21
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : jeudi 7 avril 2016 - 16:47:23

Fichier

Identifiants

  • HAL Id : tel-01248531, version 1

Collections

INRIA | PPS | USPC

Citation

Lourdes del Carmen Gonzalez Huesca. Incrementality and effect simulation in the simply typed lambda calculus. Computer Science [cs]. Universite Paris Diderot-Paris VII, 2015. English. 〈tel-01248531〉

Partager

Métriques

Consultations de la notice

227

Téléchargements de fichiers

155