您当前所在位置: 首页 > 学者

傅育熙

  • 34浏览

  • 0点赞

  • 0收藏

  • 0分享

  • 96下载

  • 0评论

  • 引用

期刊论文

Categorical Properties of Logical Frameworks*

傅育熙Yuxi Fu†

Mathematical Structures in Computer Science, 7(1):1-47, 1997.,-0001,():

URL:

摘要/描述

In this paper we define a logical framework, called λTT, that is well-suited for semantic analysis. We introduce the notion of a fibration L1: T1→C1 being internally definable1 in a fibration L2: T2→C2. This notion amounts to distinguishing an internal category L in L2 and relating L1 to the externalization of L through a pullback. When both L1 and L2 are term models of typed calculi L1 and L2 respectively, we say that L1 is an internal typed calculus definable in the frame language L2. We will show by examples that if an object language is adequately represented in λTT, then it is an internal typed calculus definable in the frame language λTT. These examples also show a general phenomenon: if the term model of an object language has categorical structure S, then an adequate encoding of the language in λTT imposes an explicit internal categorical structure S in the term model of λTT and the two structures are related via internal definability. Our categorical investigation of logical frameworks indicates a sensible model theory of encodings.

关键词:

【免责声明】以下全部内容由[傅育熙]上传于[2005年01月17日 23时17分14秒],版权归原创者所有。本文仅代表作者本人观点,与本网站无关。本网站对文中陈述、观点判断保持中立,不对所包含内容的准确性、可靠性或完整性提供任何明示或暗示的保证。请读者仅作参考,并请自行承担全部责任。

我要评论

全部评论 0

本学者其他成果

    同领域成果