Abstract
Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS). 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 distinct 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 pratiqueslanguages. 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 this PTS.
This research was partially supported by the ESPRIT Basic Research Action Types and by the GDR Programmation cofinanced by MRE-PRC and CNRS.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
MarĆa Virginia Aponte and Giuseppe Castagna. Programmation modulaire avec surcharge et liaison tardive. In JournĆ©es Francophonesdes Langages Applicatifs, January 1996.
H. Barendregt. Lambda calculi with types. Technical Report 91-19, Catholic University Nijmegen, 1991. in Handbook of Logic in Computer Science, Vol II.
Nicolas Bourbaki. ElƩments de MathƩmatique; ThƩorie des Ensembles, chapter IV. Hermann, Paris, 1970.
C. Cornes, J. Courant, J.-C. FilliĆ¢tre, G. Huet, P. Manoury, C. MuƱoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. SaĆÆbi, and B. Werner. The Coq Proof Assistant Reference Manual Version 5.10. Technical Report 0177, INRIA, July 1995.
T. Coquand and G. Huet. The Calculus of Constructions. Inf. Comp., 76:95ā120, 1988.
Evelyne Contejean and Claude MarchƩ. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science. Springer-Verlag, Rutgers University, NJ, USA, July 1996.
Judicaƫl Courant. A module calculus enjoying the subject-reduction property. Research Report RR 96-30, LIP, 1996. Preliminary version.
Roberto Di Cosmo. Isomorphisms of types: from Ī»-calculus to information retrieval and language design. Progress in Theoretical Computer Science. Birkhauser, 1995. ISBN-0-8176-3763-X.
William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. The IMPS User's Manual. The MITRE Corporation, first edition, version 2 edition, 1995.
Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143ā184, January 1993. Preliminary version appeared in Proc. 2nd IEEE Symposium on Logic in Computer Science, 1987,194ā204.
R. Harper and M. Lillibridge. A type-theoretic approach to higher-order modules with sharing. In 21st Symposium on Principles of Programming Languages, pages 123ā137. ACM Press, 1994.
Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Technical Report CMU-CS-92-191, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992.
Mark P. Jones. Using parameterized signatures to express modular structures. In 23rd Symposium on Principles of Programming Languages. ACM Press, 1996. To appear.
Xavier Leroy. Manifest types, modules, and separate compilation. In 21st symp. Principles of Progr. Lang., pages 109ā122. ACM Press, 1994.
Xavier Leroy. Applicative functors and fully transparent higher-order modules. In 22nd Symposium on Principles of Programming Languages, pages 142ā153. ACM Press, 1995.
Zhaohui Luo. ECC: an Extended Calculus of Constructions. In Proc. of IEEE 4th Ann. Symp. on Logic In Computer Science, Asilomar, California, 1989.
David B. MacQueen. Modules for Standard ML. Polymorphism, 2(2), 1985. 35 pages. An earlier version appeared in Proc. 1984 ACM Conf. on Lisp and Functional Programming.
Lena Magnusson and Bengt Nordstrƶm. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 213ā237. Springer-Verlag LNCS 806,1994.
C. Paulin-Mohring. Inductive definitions in the system Coq: Rules and Properties. In M. Bezem, J.F. Groote, editor, Proceedings of the TLCA, 1993.
Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.
FranƧois Rouaix. The Alcool 90 report. Technical report, INRIA, 1992. Included in the distribution available at ftp. inria. fr.
Amokrane Saibi, 1996. Private Communication.
Don Sannella. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS/FACS Workshop on Refinement, pages 99ā130. Springer Workshops in Computing, 1990.
P. Severi and E. Poll. Pure type systems with definitions. Lecture Notes in Computer Science, 813, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
Ā© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Courant, J. (1997). A module calculus for pure type systems. In: de Groote, P., Roger Hindley, J. (eds) Typed Lambda Calculi and Applications. TLCA 1997. Lecture Notes in Computer Science, vol 1210. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62688-3_32
Download citation
DOI: https://doi.org/10.1007/3-540-62688-3_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62688-6
Online ISBN: 978-3-540-68438-1
eBook Packages: Springer Book Archive