报告人：赵涌鑫
报告题目：An Algebraic Approach of Linking Semantic Theories of Signal Calculus
时间：2017-08-31 (星期四) 09:30 ~ 2017-08-31 (星期四) 10:30
地点：成功楼603报告厅
主办：数学与信息学院
参加对象：计算机专业感兴趣的教师和学生
报告摘要：The signal calculus for event-based synchronous language is used for specification and programming of embedded systems, which adopts broadcasting communication and follows the so-called synchronous hypothesis. Our intention is to develop an algebra for linking semantic theories ofreactions. In this paper, we mainly investigate instantaneous signal calculus (I-calculus) which contains all conceptually instantaneous reactions, i.e., zero-time reactions. The delay-time reactions will be researched in the follow-up work. To explore the semantic definition of instantaneous signal calculus, a set of algebraic laws is provided to reduce all instantaneous reactions to a normal form algebraically, which exposes the internal implicit dependence explicitly. Consequently, that two differently written reactions happen to mean the same thing can be proved from the equations of an algebraic presentation. Based on the algebra, we give several important concepts and properties concerning the distinct features of instantaneous reactions and derive an observation-oriented denotation semantics with respect to the algebraic semantics. Thus the equality of two differently written reaction is algebraically provable if and only if the two reactions are equivalent with respect to the denotational semantics.
报告人简介：2012年毕业于华东师范大学，取得计算机科学博士学位，导师为何积丰院士。2012年至2014年在新加坡国立大学担任博士后。现为华东师范大学计算机科学与软件工程学院副教授，主要研究领域为形式化方法、高可信计算等，主要研究方向为程序语言与语义模型、高可信软件建模理论与验证方法、CPS系统建模与分析等。已在形式化方法相关国际期刊与会议上发表学术论文38篇，其中第一作者与通讯作者论文15篇，18篇为CCF C类及以上期刊与会议。承担国家自然科学基金委青年基金项目《基于UTP的混成建模语言的理论研究》。
