A Representation of Fω in LF

AbstractWe study how the type theory Fω can be adequately represented in the meta-logical framework Twelf [16]. This development puts special emphasis on the way how terms, types, and kinds are represented in that it uses higher-order abstract syntax to model variable binding and dependent types to model typing constraints. Furthermore our design ensures that only well-typed terms and well-kinded types can be constructed. A possible application of this work lies in the development of safe intermediate languages for compilation