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:||Export: EndNote, Zotero | BibTex|
|Usage statistics||Look up in GoogleScholar | Find in a UK Library|