首页    期刊浏览 2024年11月30日 星期六
登录注册

文章基本信息

  • 标题:A Certified Study of a Reversible Programming Language
  • 作者:Luca Paolini ; Mauro Piccolo ; Luca Roversi
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:69
  • 页码:7:1-7:21
  • DOI:10.4230/LIPIcs.TYPES.2015.7
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We advance in the study of the semantics of Janus, a C-like reversible programming language. Our study makes utterly explicit some backward and forward evaluation symmetries. We want to deepen mathematical knowledge about the foundations and design principles of reversible computing and programming languages. We formalize a big-step operational semantics and a denotational semantics of Janus. We show a full abstraction result between the operational and denotational semantics. Last, we certify our results by means of the proof assistant Matita.
  • 关键词:reversible computing; Janus; operational semantics; bi-deterministic evaluation; categorical semantics
Loading...
联系我们|关于我们|网站声明
国家哲学社会科学文献中心版权所有