<Emphasis Type="Italic">LFTOP</Emphasis>: An <Emphasis Type="Italic">LF</Emphasis>-Based Approach to Domain-Specific Reasoning

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. This research is partly supported by the UK EPSRC projects (Grant Nos.GR/R72259 and GR/R84092), and EU Working Group ‘TYPES’ (Grant No.29001). Jian-Min Pang is an associate professor at University of Information Engineering, P.R. China. He is a Ph.D. candidate of the University of Durham, U.K. His main research interests are type theory, logical framework, and computer assisted reasoning and their applications. Paul Callaghan is a lecturer in computer science at the University of Durham (UK). He received his Ph.D. degree (1998) in natural language processing, but he has then specialised in applications of type theory. His interests include formal reasoning, programming with dependent type systems, interfaces, functional programming, and ambiguous grammar parsing. Zhao-Hui Luo is a professor of Computer Science at Royal Holloway, University of London. He received his Ph.D. degree in 1990 from University of Edinburgh, U.K. He has worked on and made substantial contributions to logic, type theory, and their applications to computer science, such as computer-assisted reasoning and functional programming. His publications include two books on type theory and programming methodology.