Object languages in a type-theoretic meta-framework

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

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, June). Object languages in a type-theoretic meta-framework. Presented at Proof Transformation and Presentation and Proof Complexities Workshop : PTP'01., Siena, Italy

• Presentation Conference Type: Conference Paper (published)
• Conference Name: Proof Transformation and Presentation and Proof Complexities Workshop : PTP'01.
• Start Date: Jun 19, 2001
• Publication Date: 2001
• Deposit Date: Mar 12, 2007
• Keywords: Logical framework, LF, Plastic, Coercive subtyping.
• Public URL: https://durham-repository.worktribe.com/output/1167296
• Additional Information: A Workshop of the International Joint Conference on Automated Reasoning : IJCAR 2001.