We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Object languages in a type-theoretic meta-framework.

Callaghan, P. and Luo, Z. and Pang, J. (2001) 'Object languages in a type-theoretic meta-framework.', Proof Transformation and Presentation and Proof Complexities Workshop : PTP'01. Siena, Italy, 19 June 2001.


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.

Item Type:Conference item (Paper)
Additional Information:Workshop of the International Joint Conference on Automated Reasoning : IJCAR 2001.
Keywords:Logical framework, LF, Plastic, Coercive subtyping.
Full text:Full text not available from this repository.
Publisher Web site:UNSPECIFIED
Record Created:12 Mar 2007
Last Modified:01 Apr 2010 15:41

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library