A Module Calculus for Pure Type Systems Export

@inproceedings{citeulike:805207, 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...}, address = {Nancy, France}, author = {Courant, Judicael}, booktitle = {Proceedings fo the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97)}, citeulike-article-id = {805207}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1548}, editor = {Hindley, R.}, keywords = {modules, pure, systems, type}, posted-at = {2006-08-18 10:51:06}, priority = {2}, publisher = {Springer-Verlag LNCS}, title = {A Module Calculus for Pure Type Systems}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1548}, year = {1997} }

TY - CONF ID - citeulike:805207 L3 - citeulike-article-id:805207 N2 - 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... AD - Nancy, France TI - A Module Calculus for Pure Type Systems PB - Springer-Verlag LNCS T2 - Proceedings fo the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97) KW - modules KW - pure KW - systems KW - type AU - Courant, Judicael A2 - Hindley, R PY - 1997/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.1548 ER -