Universal properties of impure programming languages
Universal properties of impure programming languages
复制标题
非纯编程语言的通用属性
DOI：
10.1145/2480359.2429091
复制
发表时间：
2013
影响因子：
--
通讯作者：
Staton S
中科院分区：
文献类型：
--
作者：
Staton S
我们研究不纯的、按值调用的编程语言。我们的第一种语言只有变量和 let 绑定。它的方程理论是兰贝克多范畴理论的一个变体，省略了交换性公理。我们证明了不纯语言的类型构造——乘积、和和函数——可以用“预多范畴”（交换律可能失效的多范畴）设置中的通用属性来表征。这使我们对不纯编程语言的两种早期方程理论有了新的、通用的表征：Power 和 Robinson 的前幺半群范畴，以及 Moggi 的基于 monad 的模型。因此，我们的分析将这些早期的抽象概念置于规范的基础上，将它们带到一个新的句法水平。
We investigate impure, call-by-value programming languages. Our first language only has variables and let-binding. Its equational theory is a variant of Lambek's theory of multicategories that omits the commutativity axiom.We demonstrate that type constructions for impure languages --- products, sums and functions --- can be characterized by universal properties in the setting of 'premulticategories', multicategories where the commutativity law may fail. This leads us to new, universal characterizations of two earlier equational theories of impure programming languages: the premonoidal categories of Power and Robinson, and the monad-based models of Moggi. Our analysis thus puts these earlier abstract ideas on a canonical foundation, bringing them to a new, syntactic level.
登录
查看更多内容
按值调用模型中的线性使用状态
DOI：
10.1007/978-3-642-22944-2_21
发表时间：
2011
期刊：
Proceedings 11th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
R. E. Møgelberg;S. Staton
通讯作者：
S. Staton
弗雷德 (Freyd) 饰 克莱斯利 (Kleisli)，代表《绿箭侠》
DOI：
--
发表时间：
2006
期刊：
MSFP@MPC
影响因子：
--
作者：
B. Jacobs;I. Hasuo
通讯作者：
I. Hasuo
封闭的 Freyd 和 kappa 类别
DOI：
--
发表时间：
1999
期刊：
International Colloquium on Automata, Languages and Programming
影响因子：
--
作者：
J. Power;Hayo Thielecke
通讯作者：
Hayo Thielecke
影响因子：
0.8
作者：
B. Jacobs
通讯作者：
B. Jacobs
DOI：
--
发表时间：
1969
期刊：
影响因子：
--
作者：
J. Lambek
通讯作者：
J. Lambek