2024-03-29T11:31:54Z
https://repository.nii.ac.jp/oai
oai:repository.nii.ac.jp:00001267
2023-01-11T02:10:17Z
136
NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths
龍田, 真
Tatsuta, Makoto
テクニカルレポート
Technical Report
This paper formalizes the proof of Lemma A13 given in the paper ``Compositional characterizations of lambda-terms using intersection types'' by M.~Dezani-Ciancaglini et al, so that one can verify it by a theorem prover such as HOL by typing the content of this paper. The proof in the original paper is simplified by reorganizing case analysis. Several properties implicitly used in the original paper are explicitly stated and proved.
国立情報学研究所
2012-02-17
eng
departmental bulletin paper
https://doi.org/10.20736/0000001267
https://repository.nii.ac.jp/records/1267
10.20736/0000001267
1346-5597
NIIテクニカル・レポート
NII Technical Report
1
25
https://repository.nii.ac.jp/record/1267/files/12-002E.pdf
application/pdf
271.1 kB
2019-03-13