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

文章基本信息

  • 标题:Well-Founded Recursion over Contextual Objects
  • 本地全文:下载
  • 作者:Brigitte Pientka ; Andreas Abel
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:38
  • 页码:273-287
  • DOI:10.4230/LIPIcs.TLCA.2015.273
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.
  • 关键词:Type systems; Dependent Types; Logical Frameworks
国家哲学社会科学文献中心版权所有