A Representation of Fω in LF |
| |
Authors: | Carsten Schürmann Dachuan Yu Zhaozhong Ni |
| |
Affiliation: | aDepartment of Computer Science, Yale University, New Haven, USA |
| |
Abstract: | We 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. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|