2 citations · 3 across the 7 of their papers we have counts for
7 papers
Binding Contexts as Partitionable Multisets in Abella
Terrance Gray, Gopalan Nadathur
When reasoning about formal objects whose structures involve binding, it is often necessary to analyze expressions relative to a context that associates types, values, and other re…
Modularity and Separate Compilation in Logic Programming
Steven Holte, Gopalan Nadathur
The ability to compose code in a modular fashion is important to the construction of large programs. In the logic programming setting, it is desirable that such capabilities be rea…
About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One
Gopalan Nadathur
The POPLMARK Challenge comprises a set of problems intended to measure the strength of reasoning systems in the realm of mechanizing programming language meta-theory at the time th…
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…
Combining Deduction Modulo and Logics of Fixed-Point Definitions
David Baelde, Gopalan Nadathur
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point defin…
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search
Zachary Snow, David Baelde, Gopalan Nadathur
Dependently typed lambda calculi such as the Logical Framework (LF) are capable of representing relationships between terms through types. By exploiting the "formulas-as-types" not…