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

文章基本信息

  • 标题:Search for Program Structure
  • 本地全文:下载
  • 作者:Gabriel Scherer
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2017
  • 卷号:71
  • 页码:15:1-15:14
  • DOI:10.4230/LIPIcs.SNAPL.2017.15
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:The community of programming language research loves the Curry-Howard correspondence between proofs and programs. Cut-elimination as computation, theorems for free, 'call/cc' as excluded middle, dependently typed languages as proof assistants, etc. Yet we have, for all these years, missed an obvious observation: "the structure of programs corresponds to the structure of proof search". For pure programs and intuitionistic logic, more is known about the latter than the former. We think we know what programs are, but logicians know better! To motivate the study of proof search for program structure, we retrace recent research on applying focusing to study the canonical structure of simply-typed lambda-terms. We then motivate the open problem of extending canonical forms to support richer type systems, such as polymorphism, by discussing a few enticing applications of more canonical program representations.
  • 关键词:programs; proofs; focusing; canonicity
国家哲学社会科学文献中心版权所有