13 citations · 21 across the 30 of their papers we have counts for
30 papers
Ground Stratification for a Logic of Definitions with Induction
Nathan Guermond, Gopalan Nadathur
The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively…
Transporting Theorems about Typeability in LF Across Schematically Defined Contexts
Chase Johnson, Gopalan Nadathur
The dependently-typed lambda calculus LF is often used as a vehicle for formalizing rule-based descriptions of object systems. Proving properties of object systems encoded in this…
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…
A Modular Approach to Metatheoretic Reasoning for Extensible Languages
Dawn Michaelson, Gopalan Nadathur, Eric Van Wyk
This paper concerns the development of metatheory for extensible languages. It uses as its starting point a view that programming languages tailored to specific application domains…
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…