A module calculus for Pure Type Systems. (Preliminary Version)
Résumé
Several proof-assistants rely on the very formal basis of Pure Type Systems. However, some practical issues raised by the development of large proofs lead to add other features to actual implementations for handling namespace management, for developing reusable proof libraries and for separate verification of distincts parts of large proofs. Unfortunately, few theoretical basis are given for these features. In this paper we propose an extension of Pure Type Systems with a module calculus adapted from SML-like module systems for programming languages. Our module calculus gives a theoretical framework addressing the need for these features. We show that our module extension is conservative, and that type inference in the module extension of a given PTS is decidable under some hypotheses over the considered PTS.
Plusieurs assistants de preuves sont fondés sur les Systèmes de Types Purs (PTS). Cependant, des considérations pratiques provenant du développement de grandes preuves conduisent à ajouter aux implémentations des mécanismes permettant une gestion rationnelle des noms, le développement de bibliothèques de preuves réutilisables, et la vérification séparée des différentes parties d'un gros développement. Alors que la correction des PTS utilisés est théoriquement bien fondé, ces mécanismes sont en revanche peu étudiés, alors qu'ils peuvent mettre en péril la correction de l'ensemble de l'outil de démonstration. Pour répondre à ce problème, nous proposons dans ce rapport une extension des PTS par un système de modules similaire à celui de SML pour le langage de programmation ML. Notre système de modules donne un cadre théorique rigoureux pour l'étude des mécanismes que nous avons cités. Nous montrons que l'extension proposée est conservative, et que l'inférence de type est décidable moyennant quelques hypothèses raisonnables sur le PTS considéré.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...