3 citations · 3 across the 2 of their papers we have counts for
4 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 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…