Skip to Main content Skip to Navigation

A module calculus for Pure Type Systems. (Preliminary Version)

Abstract : 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.
Document type :
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:07:52 AM
Last modification on : Saturday, September 11, 2021 - 3:19:18 AM


Files produced by the author(s)


  • HAL Id : hal-02101842, version 1



Judicael Courant. A module calculus for Pure Type Systems. (Preliminary Version). [Research Report] LIP RR-1996-31, Laboratoire de l'informatique du parallélisme. 1996, 2+18p. ⟨hal-02101842⟩



Record views


Files downloads