Skip to main content

Research Repository

Advanced Search

Object languages in a type-theoretic meta-framework

Callaghan, P.; Luo, Z.; Pang, J.

Authors

P. Callaghan

Z. Luo

J. Pang



Abstract

This paper concerns techniques for providing a convenient syntax for object languages implemented via a type-theoretic Logical Framework, and reports on work in progress. We first motivate the need for a type-theoretic logical framework. Firstly, we take the logical framework seriously as a meta-language for implementing object languages (including object type theories). Another reason is the goal of building domain-specific reasoning tools which are implemented using type theory technology but do not require great expertise in type theory to use productively. We then present several examples of bi-directional translations between an encoding in the framework language and a more convenient syntax. The paper ends by discusing several techniques for implementing the translations and properties that we may require for the translation. Coercive subtyping is shown to help in the translation.

Citation

Callaghan, P., Luo, Z., & Pang, J. (2001). Object languages in a type-theoretic meta-framework.

Conference Name Proof Transformation and Presentation and Proof Complexities Workshop : PTP'01.
Conference Location Siena, Italy
Start Date Jun 19, 2001
Publication Date 2001
Deposit Date Mar 12, 2007
Keywords Logical framework, LF, Plastic, Coercive subtyping.
Additional Information A Workshop of the International Joint Conference on Automated Reasoning : IJCAR 2001.