Scholarlink

<p>In this paper, we show that the hyperintensional typed lambda calculus (HTLC) of Fait and Primiero (<i>Journal of Applied Logics - IfCoLog Journal of Logics and their Applications</i>, 8(2), 469–495, <CitationRef CitationID="CR10">2021</CitationRef>) inspired by transparent intensional logic is equivalent to the computational lambda calculus (CLC) of Moggi (<i>Information and Computation</i>, 93(1), 55–92, <CitationRef CitationID="CR17">1991</CitationRef>) extended by a simple axiom. We demonstrate this by first establishing a link between HTLC and propositional lax logic (PLL) which corresponds to CLC via the Curry-Howard isomorphism. Our result puts on solid formal ground a long-held assumption that there is a close connection between the notions of structured hyperintension and computation.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Hyperintensions as Computations

  • 期刊论文

  • 发表日期：

    2025年9月15日

查看全文
  • Ivo Pezlar

摘要

In this paper, we show that the hyperintensional typed lambda calculus (HTLC) of Fait and Primiero (Journal of Applied Logics - IfCoLog Journal of Logics and their Applications, 8(2), 469–495, 2021) inspired by transparent intensional logic is equivalent to the computational lambda calculus (CLC) of Moggi (Information and Computation, 93(1), 55–92, 1991) extended by a simple axiom. We demonstrate this by first establishing a link between HTLC and propositional lax logic (PLL) which corresponds to CLC via the Curry-Howard isomorphism. Our result puts on solid formal ground a long-held assumption that there is a close connection between the notions of structured hyperintension and computation.