Skip to main content

Research Repository

Advanced Search

LFTOP : an LF-based approach to domain-specific reasoning

Pang, Jianmin; Callaghan, Paul; Luo, Zhaohui

Authors

Jianmin Pang

Paul Callaghan

Zhaohui Luo



Abstract

A new approach to domain-specific reasoning is presented that is based on a type-theoretic logical framework (LF) but does not require the user to be an expert in type theory. The concepts of the domain and its related reasoning systems are formalized in LF, but the user works with the system through a syntax and interface appropriate to his/her work. A middle layer provides translation between the user syntax and LF, and allows additional support for reasoning (e.g., model checking). Thus, the complexity of the logical framework is hidden but the benefits of using type theory and its related tools are retained, such as precision and machine-checkable proofs. This approach is investigated through a number of case studies: here, the authors consider the verification of properties of concurrency. The authors have formalized a specification language (CCS) and logic (μ--calculus) in LF, together with useful lemmas, and a user-oriented syntax has been designed. The authors demonstrate the approach with simple examples. However, applying lemmas to objects introduced by the user may result in framework-level objects which cannot be translated back to the user level.The authors discuss this problem, define a notion of adequacy, and prove that in this case study, translation can always be reversed.

Citation

Pang, J., Callaghan, P., & Luo, Z. (2005). LFTOP : an LF-based approach to domain-specific reasoning. Journal of Computer Science and Technology, 20(4), 526-535. https://doi.org/10.1007/s11390-005-0526-y

Journal Article Type Article
Publication Date 2005-07
Deposit Date Oct 7, 2008
Journal Journal of Computer Science and Technology
Print ISSN 1000-9000
Electronic ISSN 1860-4749
Publisher Springer
Peer Reviewed Peer Reviewed
Volume 20
Issue 4
Pages 526-535
DOI https://doi.org/10.1007/s11390-005-0526-y
Keywords Domain-specific, Formal reasoning, Logical framework, Proof assistant, Type theory.