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 :
Reports
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101842
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:07:52 AM
Last modification on : Sunday, May 19, 2019 - 1:20:46 AM

File

RR1996-31.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101842, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

2

Files downloads

8