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

スポンサーリンク

概要

• 論文の詳細を見る

• 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.

• 一般社団法人 情報処理学会の論文

著者

• 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

スポンサーリンク