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

文章基本信息

  • 标题:Observability for Pair Pattern Calculi
  • 本地全文:下载
  • 作者:Antonio Bucciarelli ; Delia Kesner ; Simona Ronchi Della Rocca
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2015
  • 卷号:38
  • 页码:123-137
  • DOI:10.4230/LIPIcs.TLCA.2015.123
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which - together with typability - allows to obtain a full characterization of observability.
  • 关键词:solvability; pattern calculi; intersection types; inhabitation
国家哲学社会科学文献中心版权所有