3 papers
cs.LO2025
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…
cs.LO2025
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…
cs.LO2024
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…