A First-Order Calculus for Allegories

被引：0
|
作者：
Aameri, Bahar [1 ]
Winter, Michael [2 ]
机构：
[1] Univ Toronto, Dept Comp Sci, Toronto, ON M5S 3G8, Canada
[2] Brock Univ, Dept Comp Sci, St Catharines, ON L2S 3A1, Canada
来源：
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE | 2011年 / 6663卷
基金：
加拿大自然科学与工程研究理事会;
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In this paper we present a language and first-order calculus for formal reasoning about relations based on the theory of allegories. Since allegories are categories, the language is typed in Church-style. We show soundness and completeness of the calculus and demonstrate its usability by presenting the RelAPS system; a proof assistant for relational categories based on the calculus presented here.
引用
收藏
页码：74 / 91
页数：18
相关论文
共 50 条
12345