Explicit convertibility proofs in pure type systems

Autor: Doorn, F. van, Geuvers, H., Wiedijk, F., Momiglinao, A.

Publikováno v: Momiglinao, A. (ed.), LFMTP '13 : Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, September 25-27, Boston, MA, USA, pp. 25-36
LFMTP
Momiglinao, A. (ed.), LFMTP '13 : Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, September 25-27, Boston, MA, USA, 25-36. New York : ACM
STARTPAGE=25;ENDPAGE=36;TITLE=Momiglinao, A. (ed.), LFMTP '13 : Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice, September 25-27, Boston, MA, USA
Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice (LFMTP'13, Boston MA, USA, September 23, 2013; in conjunction with ICFP'13), 25-36
STARTPAGE=25;ENDPAGE=36;TITLE=Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice (LFMTP'13, Boston MA, USA, September 23, 2013; in conjunction with ICFP'13)

We define type theory with explicit conversions. When type checking a term in normal type theory, the system searches for convertibility paths between types. The results of these searches are not stored in the term, and need to be reconstructed every

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::817f7e3ac8e42f6c27f97768fd07db4f
http://doi.acm.org/10.1145/2503887.2503890