Type theoretic semantics for programming languages
Institution:
NiceDisciplines:
Directors:
Abstract EN:
Semantics of programming languages gives the meaning of program constructs. Operational and denotational semantics are two main approaches for programming languages semantics. Operational semantics is usually given by inductive relations. Denotational semantics is given by partial functions. Implementing the denotational semantics inside type theory is difficult as the type theory expects total functions. In this dissertation we develop a functional semantics for a small imperative language inside type theory and show its equivalence with operational semantics. We then exploit this functional semantics to obtain a more direct proof search tool, while developing a way to describer and manipulate unknown expressions, in the symbolic computation of programs for formal proof development. In a third part, we address the problem of encoding complex programs inside type theory and we show how to circumvent the limitations of guardedness conditions as the are used in the Calculus of Inductive Constructions.
Abstract FR:
La sémantique des langages de programmation donne la signification des constructions de programme. Les sémantiques opérationnelle et dénotationelle sont les deux principales approches pour la sémantique de langage de programmation. La sémantique opérationnelle est habituellement donnée par des relations inductives. La sémantique dénotationelle est donnée par des fonctions partielles. Mettre en application la sémantique dénotationelle à l’intérieur de la théorie des types est difficile car cette théorie ne supporte que les fonctions totales. Dans cette thèse nous développons une sémantique fonctionnelle pour un petit langage impératif à l’intérieur de la théorie des types et montrons son équivalence avec la sémantique opérationnelle. Nous exploitons ensuite cette sémantique fonctionnelle pour obtenir un outil plus direct de recherche de preuve, tout en développant une manière de décrire et manipuler des expressions inconnues dans le calcul symbolique des programmes pour le développement formel de preuve. Dans une troisième partie, nous adressons le problème de coder des programmes complexes à l’intérieur de la théorie des types et nous montrons comment éviter les limitations des conditions de garde telle qu’elles sont employées dans le calcul des constructions inductives.