Based on the ELF(Edinburgh logical framework)and Martin—Lof logical framework,the authors propose a logical framework that unifies the two languages.Their logical framework is well suited for semantic analysis.Examples are given to show how to encode object languages in the calculus.