Healthiness is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic'/> Healthiness from Duality
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Healthiness from Duality
【24h】

Healthiness from Duality

机译：双重性带来的健康

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Healthiness is a good old question in program logics that dates back to Dijkstra. It asks for an intrinsic characterization of those predicate transformers which arise as the (backward) interpretation of a certain class of programs. There are several results known for healthiness conditions: for deterministic programs, nondeterministic ones, probabilistic ones, etc. Building upon our previous works on so-called state-and-effect triangles, we contribute a unified categorical framework for investigating healthiness conditions. This framework is based on a dual adjunction induced by a dualizing object and on our notion of relative Eilenberg-Moore algebra. The latter notion seems interesting in its own right in the context of monads, Lawvere theories and enriched categories.
机译：健康 这是程序逻辑中一个很好的老问题，可以追溯到Dijkstra。它要求对这些谓词转换器进行内在表征，这些谓词转换器是对某种程序类别的（向后）解释。有一些关于健康状况的结果：确定性程序，非确定性程序，概率性程序等。以我们先前在所谓的“工作”上的工作为基础 状态和效果三角形< / i> ，我们为调查健康状况提供了一个统一的分类框架。该框架基于由双重化对象引起的双重结合以及我们的 相对的Eilenberg-Moore代数 。在单子论，Lawvere理论和丰富的范畴的背景下，后一种概念本身似乎很有趣。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号