Verification of Substitution Theorem Using HOL

スポンサーリンク

概要

• 論文の詳細を見る

• Substitution Theorem is a new theorem in untyped lambda calculus, which was proved in 2006. This theorem states that for a given lambda term and given free variables in it, the term becomes weakly normalizing when we substitute arbitrary weakly normalizing terms for these free variables, if the term becomes weakly normalizing when we substitute a single arbitrary weakly normalizing term for these free variables. This paper formalizes and verifies this theorem by using the higher-order theorem prover HOL. A control path, which is the key notion in the proof, explicitly uses names of bound variables in lambda terms, and it is defined only for lambda terms without bound variable renaming. The lambda terms without bound variable renaming are formalized by using the HOL package based on contextual alpha-equivalence. The verification uses 10119 lines of HOL code and 326 lemmas.

• Information and Media Technologies 編集運営会議の論文

著者

• Tatsuta Makoto

  National Institute of Informatics

• Koai Takayuki

  National Institute of Informatics

関連論文

• Verification of Substitution Theorem Using HOL (プログラミング Vol.5 No.2)
• Verification of Substitution Theorem Using HOL

スポンサーリンク