The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

An Encoding of Fomega in LF

Last modified: Wed Sep 5 18:52:13 2001 GMT.

Authors

Carsten Schürmann
Dachuan Yu
Zhaozhong Ni

Abstract

We study how the type theory Fomega can be adequately represented in the meta-logical framework Twelf. 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.

Published

  • In Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001), Siena, Italy, June 2001.

Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon