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

文章基本信息

  • 标题:Big Step Normalisation for Type Theory
  • 本地全文:下载
  • 作者:Thorsten Altenkirch ; Colin Geniet
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:175
  • 页码:1-20
  • DOI:10.4230/LIPIcs.TYPES.2019.4
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to prove strong normalisation of β-reduction for typed lambda-calculi. We generalise big step normalisation to a minimalist dependent type theory. Compared to previous presentations of big step normalisation for e.g. the simply-typed lambda-calculus, we use a quotiented syntax of type theory, which crucially reduces the syntactic complexity introduced by dependent types. Most of the proof has been formalised using Agda.
  • 关键词:Normalisation; big step normalisation; type theory; dependent types; Agda
国家哲学社会科学文献中心版权所有