3 citations · 7 across the 7 of their papers we have counts for
7 papers
On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms
Gopalan Nadathur, Mary Southern
Felty and Miller have described what they claim to be a faithful encoding of the dependently typed lambda calculus LF in the logic of hereditary Harrop formulas, a sublogic of an i…
Adelfa: A System for Reasoning about LF Specifications
Mary Southern, Gopalan Nadathur
We present a system called Adelfa that provides mechanized support for reasoning about specifications developed in the Edinburgh Logical Framework or LF. Underlying Adelfa is a new…
A Logic for Reasoning About LF Specifications
Gopalan Nadathur, Mary Southern
We present a logic named L_{LF} whose intended use is to formalize properties of specifications developed in the dependently typed lambda calculus LF. The logic is parameterized by…
A Framework for Reasoning About LF Specifications
Mary Southern
This thesis develops a framework for formalizing reasoning about specifications of systems written in LF. This formalization centers around the development of a reasoning logic tha…
Towards a Logic for Reasoning About LF Specifications
Mary Southern, Gopalan Nadathur
We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, typing judgments in LF serve as atomic formulas, a…
A Lambda Prolog Based Animation of Twelf Specifications
Mary Southern, Gopalan Nadathur
Specifications in the Twelf system are based on a logic programming interpretation of the Edinburgh Logical Framework or LF. We consider an approach to animating such specification…
Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form
Mary Southern, Gopalan Nadathur
Dependently typed lambda calculi such as the Edinburgh Logical Framework (LF) are a popular means for encoding rule-based specifications concerning formal syntactic objects. In the…