Université Lille1 - Sciences et Technologies
Autour du lambda-calcul partiel
005.1
Langages de programmation
LISP (langage de programmation)
Lambda-calcul
Caml (langage de programmation)
AUTOMATH (langage formel)
ML (langage de programmation)
Fonctions calculables
Informatique
Text
Electronic Thesis or Dissertation
fr
Cette thèse a pour objet l'étude des aspects syntaxiques, algébriques et catégoriques du lambda-calcul partiel, qui est un outil théorique pour étudier l'équivalence de programmes exécutées selon un mécanisme d'appel par valeur. En appliquant des techniques éprouvées dans le lambda-calcul pur et en les adaptant à ce calcul on a ainsi obtenu: 1) une preuve de la confluence pour un lambda-calcul partiel simplifie; 2) la caractérisation d'une classe de termes fortement normalisables par un système de types simples; 3) la caractérisation des termes égalisables à une valeur dans le lambda-calcul partiel comme conséquence de celle obtenue par un système de types dans le lambda-calcul par valeur, calcul antérieur et de même vocation que le précédent, mais moins expressif; 4) l'élaboration d'une notion d'algèbre combinatoire répondant à celle de modèle du lambda-calcul partiel et de la relation de cette notion avec la donnée d'une catégorie cartesienne fermée partielle munie d'un objet réflexif
application/pdf
1 : 1 Mo
https://pepite-depot.univ-lille.fr/LIBRE/Th_Num/1993/50376-1993-71.pdf
Even
Christian
1900-01-01
074225855
1993LIL10045
1993-01-01
Informatique
Université Lille1 - Sciences et Technologies
026404184
Doctorat
non
oui
Jacob
Gérard
03068739X
ddc:000
ASCII
PDF
9999