arXiv subjects

Gopalan Nadathur

Publications and source records attributed to Gopalan Nadathur.

At least 19 recordsLinked to original sources

arXiv2025

Ground Stratification for a Logic of Definitions with Induction

The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the logic includes a strict stratification condition on definitions that is too restrictive for some applications such as those that use a logical relations based approach to semantic equivalence. Tiu has shown how this restriction can be eased by utilizing a weaker notion referred to as ground stratification. Tiu's results were limited to a version of the logic that does not treat inductive definitions. We show here that they can be extended to cover such definitions. While our results are obtained by using techniques that have been previously deployed in related ways in this context, their use is sensitive to the particular way in which we generalize the logic. In particular, although ground stratification may be used with arbitrary fixed-point definitions, we show that weakening stratification to this form for inductive definitions leads to inconsistency. The particular generalization we describe accords well with the way logical relations are used in practice. Our results are also a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.

cs.LO↗

arXiv2025

Transporting Theorems about Typeability in LF Across Schematically Defined Contexts

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 fashion requires reasoning about formulas over LF typing judgements. An important characteristic of LF is that it supports a higher-order abstract syntax representation of binding structure. When such an encoding is used, the typing judgements include contexts that assign types to bound variables and formulas must therefore allow for quantification over contexts. The possible instantiations of such quantifiers are usually governed by schematic descriptions that must also be made explicit for effectiveness in reasoning. In practical reasoning tasks, it is often necessary to transport theorems involving universal quantification over contexts satisfying one schematic description to those satisfying another description. We provide here a logical justification for this ability. Towards this end, we utilize the logic $\mathcal{L}_{LF}$, which has previously been designed for formalizing properties of LF specifications. We develop a transportation proof rule and show it to be sound relative to the semantics of $\mathcal{L}_{LF}$. Key to this proof rule is a notion of context schema subsumption that uses the subordination relation between types as a means for determining the equivalence of contexts relative to individual LF typing judgements. We discuss the incorporation of this rule into the Adelfa proof assistant and its use in actual reasoning examples.

cs.LO↗

arXiv2024

Binding Contexts as Partitionable Multisets in Abella

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 related attributes with variables that appear free in the expressions. We refer to such associations as binding contexts. Reasoning tasks also require properties such as the shape and uniqueness of associations concerning binding contexts to be made explicit. The Abella proof assistant, which supports a higher-order treatment of syntactic constructs, provides a simple and elegant way to describe such contexts from which their properties can be extracted. This mechanism is based at the outset on viewing binding contexts as ordered sequences of associations. However, when dealing with object systems that embody notions of linearity, it becomes necessary to treat binding contexts more generally as partitionable multisets. We show how to adapt the original Abella encoding to encompass such a generalization. The key idea in this adaptation is to base the definition of a binding context on a mapping to an underlying ordered sequence of associations. We further show that properties that hold with the ordered sequence view can be lifted to the generalized definition of binding contexts and that this lifting can, in fact, be automated. These ideas find use in the extension currently under development of the two-level logic approach of Abella to a setting where linear logic is used as the specification logic.

cs.LO↗

arXiv2023

A Modular Approach to Metatheoretic Reasoning for Extensible Languages

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 are to be constructed by composing components from an open library of independently-developed extensions to a host language. In the elaboration of this perspective, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented in this context by formulas over such relations. These properties may be fundamental to the language, introduced by the host language, or they may pertain to analyses introduced by individual extensions. We expose the problem of modular metatheory, i.e., the notion that proofs of relevant properties can be constructed by reasoning independently within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad, a priori constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Mathematical precision is given to our discussions by framing them within a logic that encodes inductive rule-based specifications via least fixed-point definitions. We also sketch the structure of a practical system for metatheoretic reasoning for extensible languages based on the ideas developed.

cs.PL↗

arXiv2023

Modularity and Separate Compilation in Logic Programming

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 realized through logic-based devices. We describe an approach for doing this here. In our scheme a module corresponds to a block of code whose external view is mediated by a signature. Thus, signatures impose a form of hiding that is explained logically via existential quantifications over predicate, function and constant names. Modules interact through the mechanism of accumulation that translates into conjoining the clauses in them while respecting the scopes of existential quantifiers introduced by signatures. We show that this simple device for statically structuring name spaces suffices for realizing features related to code scoping for which the dynamic control of predicate definitions was earlier considered necessary. The module capabilities we present have previously been implemented via the compile-time inlining of accumulated modules. This approach does not support separate compilation. We redress this situation by showing how each distinct module can be compiled separately and inlining can be realized by a later, complementary and equally efficient linking phase.

cs.PL↗

arXiv2022

A Logic for Reasoning About LF Specifications

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 the LF signature that constitutes the specification. Atomic formulas correspond to typing derivations relative to this signature. The logic includes a collection of propositional connectives and quantifiers. Quantification ranges over expressions that denote LF terms and LF contexts. Quantifiers of the first variety are qualified by simple types that describe the functional structure associated with the variables they bind; deeper, dependency related properties are expressed by the body of the formula. Context-level quantifiers are qualified by context schemas that identify patterns of declarations out of which actual contexts may be constructed. The semantics of variable-free atomic formulas is articulated via the derivability in LF of the judgements they encode. Propositional constants and connectives are understood in the usual manner and the meaning of quantifiers is explicated through substitutions of expressions that adhere to the type qualifications. The logic is complemented by a proof system that enables reasoning that is sound with respect to the described semantics. The main novelties of the proof system are the provision for case-analysis style reasoning about LF judgements, support for inductive reasoning over the heights of LF derivations and the encoding of LF meta-theorems. The logic is motivated by the paradigmatic example of type assignment in the simply-typed lambda calculus and the proof system is illustrated through the formalization of a proof of type uniqueness for this calculus.

cs.LO↗

arXiv2021

About a Proof Pearl: A Purported Solution to a POPLMARK Challenge Problem that is Not One

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 the challenge was enunciated. Included in the collection is the exercise of demonstrating transitivity of subtyping for a specific algorithmic formulation of subtyping for an extension of System F. The challenge represented by this problem derives from the fact that, for the given formulation, subtyping must be proved simultaneously with another property called narrowing. In a paper published as a proof pearl, Brigitte Pientka claimed to have presented a solution to the problem in which "the full power of parametric and higher-order judgments" is exploited to "get the narrowing lemma for free." We show this claim to be inaccurate. In particular, we show that the simplification is in substantial part the result of changing the formulation of the subtyping relation in a way that modifies the challenge rather than the outcome of the manner in which the argument is mechanized.

cs.LO↗

arXiv2021

On Encoding LF in a Predicate Logic over Simply-Typed Lambda Terms

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 intuitionistic variant of Church's Simple Theory of Types. Their encoding is based roughly on translating object expressions in LF into terms in a simply typed lambda calculus by erasing dependencies in typing and then recapturing the erased dependencies through the use of predicates. Unfortunately, this idea does not quite work. In particular, we provide a counterexample to the claim that the described encoding is faithful. The underlying reason for the falsity of the claim is that the mapping from dependently typed lambda terms to simply typed ones is not one-to-one and hence the inverse transformation is ambiguous. This observation has a broad implication for other related encodings.

cs.LO↗

arXiv2021

Adelfa: A System for Reasoning about LF Specifications

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 logic named L_LF. Typing judgements in LF are represented by atomic formulas in L_LF and quantification is permitted over contexts and terms that appear in such formulas. Contexts, which constitute type assignments to uniquely named variables that are modelled using the technical device of nominal constants, are characterized in L_LF by context schemas that describe their inductive structure. We present these formulas and an associated semantics before sketching a proof system for constructing arguments that are sound with respect to the semantics. We then outline the realization of this proof system in Adelfa and illustrate its use through a few example proof developments. We conclude the paper by relating Adelfa to existing systems for reasoning about LF specifications.

cs.LO↗

arXiv2018

Towards a Logic for Reasoning About LF Specifications

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, and quantification is permitted over contexts and terms that might appear in them. Further, contexts, which constitute type assignments to uniquely named variables that are modeled using the technical device of nominal constants, can be characterized via an inductive description of their structure. We present a semantics for such formulas and then consider the task of proving them. Towards this end, we restrict the collection of formulas we consider so as to ensure that they have normal forms upon which proof rules may be based. We then specifically discuss a proof rule that provides the basis for case analysis over LF typing judgments; this rule is the most complex and innovative one in the collection. We illustrate the proof system through an example. Finally, we discuss ongoing work and we relate our project to existing systems that have a similar goal.

cs.LO↗

arXiv2018

Schematic Polymorphism in the Abella Proof Assistant

The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic: formalizations that are identical except in the respect that they apply to different types have to be repeated at each type. We develop an approach that overcomes this limitation while preserving the logical underpinnings of the system. In this approach object constructors, formulas and other relevant logical notions are allowed to be parameterized by types, with the interpretation that they stand for the (infinite) collection of corresponding constructs that are obtained by instantiating the type parameters. The proof structures that we consider for formulas that are schematized in this fashion are limited to ones whose type instances are valid proofs in the simply typed logic. We develop schematic proof rules that ensure this property, a task that is complicated by the fact that type information influences the notion of unification that plays a key role in the logic. Our ideas, which have been implemented in an updated version of the system, accommodate schematic polymorphism both in the core logic of Abella and in the executable specification logic that it embeds.

cs.LO↗

arXiv2016

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs

We describe an approach to the verified implementation of transformations on functional programs that exploits the higher-order representation of syntax. In this approach, transformations are specified using the logic of hereditary Harrop formulas. On the one hand, these specifications serve directly as implementations, being programs in the language Lambda Prolog. On the other hand, they can be used as input to the Abella system which allows us to prove properties about them and thereby about the implementations. We argue that this approach is especially effective in realizing transformations that analyze binding structure. We do this by describing concise encodings in Lambda Prolog for transformations like typed closure conversion and code hoisting that are sensitive to such structure and by showing how to prove their correctness using Abella.

cs.PL↗

arXiv2014

A Lambda Prolog Based Animation of Twelf Specifications

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 specifications using a Lambda Prolog implementation. This approach is based on a lossy translation of the dependently typed LF expressions into the simply typed lambda calculus (STLC) terms of Lambda Prolog and a subsequent encoding of lost dependency information in predicates that are defined by suitable clauses. To use this idea in an implementation of logic programming a la Twelf, it is also necessary to translate the results found for Lambda Prolog queries back into LF expressions. We describe such an inverse translation and show that it has the necessary properties to facilitate an emulation of Twelf behavior through our translation of LF specifications into Lambda Prolog programs. A characteristic of Twelf is that it permits queries to consist of types which have unspecified parts represented by meta-variables for which values are to be found through computation. We show that this capability can be supported within our translation based approach to animating Twelf specifications.

cs.PL↗

arXiv2013

Translating Specifications in a Dependently Typed Lambda Calculus into a Predicate Logic Form

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 these frameworks, relations over terms representing formal objects are naturally captured by making use of the dependent structure of types. We consider here the meaning-preserving translation of specifications written in this style into a predicate logic over simply typed λ-terms. Such a translation can provide the basis for efficient implementation and sophisticated capabilities for reasoning about specifications. We start with a previously described translation of LF specifications to formulas in the logic of higher-order hereditary Harrop (hohh) formulas. We show how this translation can be improved by recognizing and eliminating redundant type checking information contained in it. This benefits both the clarity of translated formulas, and reduces the effort which must be spent on type checking during execution. To allow this translation to be used to execute LF specifications, we describe an inverse transformation from hohh terms to LF expressions; thus computations can be carried out using the translated form and the results can then be exported back into LF. Execution based on LF specifications may also involve some forms of type reconstruction. We discuss the possibility of supporting such a capability using the translation under some reasonable restrictions on the structure of specifications.

cs.LO↗

arXiv2013

Reasoning About Higher-Order Relational Specifications

The logic of hereditary Harrop formulas (HH) has proven useful for specifying a wide range of formal systems. This logic includes a form of hypothetical judgment that leads to dynamically changing sets of assumptions and that is key to encoding side conditions and contexts that occur frequently in structural operational semantics (SOS) style presentations. Specifications are often useful in reasoning about the systems they describe. The Abella theorem prover supports such reasoning by explicitly embedding the specification logic within a rich reasoning logic; specifications are then reasoned about through this embedding. However, realizing an induction principle in the face of dynamically changing assumption sets is nontrivial and the original Abella system uses only a subset of the HH specification logic for this reason. We develop a method here for supporting inductive reasoning over all of HH. Our approach takes advantage of a focusing property of HH to isolate the use of an assumption and the ability to finitely characterize the structure of any such assumption in the reasoning logic. We demonstrate the effectiveness of these ideas via several specification and meta-theoretic reasoning examples that have been implemented in an extended version of Abella.

cs.LO↗

arXiv2013

Towards Extracting Explicit Proofs from Totality Checking in Twelf

The Edinburgh Logical Framework (LF) is a dependently type lambda calculus that can be used to encode formal systems. The versatility of LF allows specifications to be constructed also about the encoded systems. The Twelf system exploits the correspondence between formulas and types to give specifications in LF a logic programming interpretation. By interpreting particular arguments as input and others as output, specifications can be seen as describing non-deterministic functions. If particular such functions can be shown to be total, they represent constructive proofs of meta-theorems of the encoded systems. Twelf provides a suite of tools for establishing totality. However, all the resulting proofs of meta-theorems are implicit: Twelf's totality checking does not yield a certificate that can be given to a proof checker. We begin the process here of making these proofs explicit. We treat the restricted situation in Twelf where context definitions (regular worlds) and lemmas are not used. In this setting we describe and prove correct a translation of the steps in totality checking into an actual proof in the companion logic M2. We intend in the long term to extend our translation to all of Twelf and to use this work as the basis for producing proofs in the related Abella system.

cs.LO↗

arXiv2012

Combining Deduction Modulo and Logics of Fixed-Point Definitions

Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of recursive specifications. These specifications are not directly complemented by fixed-point reasoning techniques and, correspondingly, do not have to satisfy strong monotonicity restrictions. We show how to incorporate a rewriting capability into logics of fixed-point definitions towards additionally supporting recursive specifications. In particular, we describe a natural deduction calculus that adds a form of "closed-world" equality - a key ingredient to supporting fixed-point definitions - to deduction modulo, a framework for extending a logic with a rewriting layer operating on formulas. We show that our calculus enjoys strong normalizability when the rewrite system satisfies general properties and we demonstrate its usefulness in specifying and reasoning about syntax-based descriptions. The integration of closed-world equality into deduction modulo leads us to reconfigure the elimination principle for this form of equality in a way that, for the first time, resolves issues regarding the stability of finite proofs under reduction.

cs.LO↗

arXiv2011

Proceedings Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice

This volume constitutes the proceedings of LFMTP 2011, the Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice. The LFMTP workshop series brings together designers, implementors, and practitioners to discuss varied aspects of the structure of logical frameworks and meta-languages that impinge on their use in representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. LFMTP 2011 was held on August 26, 2011 in Nijmegen, Netherlands, as a workshop associated with ITP 2011, the Second International Conference on Interactive Theorem Proving. Its program consisted of contributed and invited presentations and was integrated with that of MLPA 11, the Third Workshop on Modules and Libraries for Proof Assistants. This proceedings contains only the contributed papers that were accepted for presentation at the workshop. Each of these papers was accepted based on the reviews of three members of the program committee. Authors were subsequently given the opportunity to revise their submissions based on the comments provided by the reviewers and the feedback obtained during their presentations at the workshop.

cs.LO↗