Abstract: In this paper we study the verification of semantic properties based on type-theoretic logical framework （LF）. For functional programming language LAZY-PCF＋SHAR we present formal descriptions of its concepts and proofs of the relevant properties by using

Key words: Type theory, Logic framework, Verification of semantic properties, Operational semantics, Functional programming