2013/10/31 by Mary Southern, Southern, Mary, Gopalan Nadathur +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Natural Language Processing Techniques #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.1310.8568
openalex publication_date 2013/10/31 · openalex created_date 2025/10/24 · openalex updated_date 2026/07/28
Dependently typed lambda calculi such as the Edinburgh Logical Framework (LF)\nare a popular means for encoding rule-based specifications concerning formal\nsyntactic objects. In these frameworks, relations over terms representing\nformal objects are naturally captured by making use of the dependent structure\nof types. We consider here the meaning-preserving translation of specifications\nwritten in this style into a predicate logic over simply typed \λ-terms.\nSuch a translation can provide the basis for efficient implementation and\nsophisticated capabilities for reasoning about specifications. We start with a\npreviously described translation of LF specifications to formulas in the logic\nof higher-order hereditary Harrop (hohh) formulas. We show how this translation\ncan be improved by recognizing and eliminating redundant type checking\ninformation contained in it. This benefits both the clarity of translated\nformulas, and reduces the effort which must be spent on type checking during\nexecution. To allow this translation to be used to execute LF specifications,\nwe describe an inverse transformation from hohh terms to LF expressions; thus\ncomputations can be carried out using the translated form and the results can\nthen be exported back into LF. Execution based on LF specifications may also\ninvolve some forms of type reconstruction. We discuss the possibility of\nsupporting such a capability using the translation under some reasonable\nrestrictions on the structure of specifications.\n