Showing 1–27 of 27 results for author: Nadathur, G

A Modular Approach to Metatheoretic Reasoning for Extensible Languages

Authors: Dawn Michaelson, Gopalan Nadathur, Eric Van Wyk

Abstract: 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 ty**) and dynamic semantics… ▽ More 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 ty**) 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. △ Less

Submitted 21 December, 2023; originally announced December 2023.

Modularity and Separate Compilation in Logic Programming

Authors: Steven Holte, Gopalan Nadathur

Abstract: 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 hidi… ▽ More 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 sco** 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. △ Less

Submitted 18 March, 2023; originally announced March 2023.

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

Authors: Gopalan Nadathur

Abstract: 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 subty** for a specific algorithmic formulation of subty** for an extension of System F. The challenge represente… ▽ More 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 subty** for a specific algorithmic formulation of subty** for an extension of System F. The challenge represented by this problem derives from the fact that, for the given formulation, subty** 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 subty** relation in a way that modifies the challenge rather than the outcome of the manner in which the argument is mechanized. △ Less

Submitted 16 December, 2021; originally announced December 2021.

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

Authors: Gopalan Nadathur, Mary Southern

Abstract: 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 ty** and then re… ▽ More 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 ty** 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 map** 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. △ Less

Submitted 24 August, 2021; originally announced August 2021.

Adelfa: A System for Reasoning about LF Specifications

Authors: Mary Southern, Gopalan Nadathur

Abstract: 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. Ty** 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 u… ▽ More 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. Ty** 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. △ Less

Submitted 15 July, 2021; originally announced July 2021.

Comments: In Proceedings LFMTP 2021, arXiv:2107.07376

Journal ref: EPTCS 337, 2021, pp. 104-120

A Logic for Reasoning About LF Specifications

Authors: Gopalan Nadathur, Mary Southern

Abstract: 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 ty** derivations relative to this signature. The logic includes a collection of propositional connectives and quantifiers. Quantificat… ▽ More 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 ty** 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. △ Less

Submitted 8 April, 2022; v1 submitted 30 June, 2021; originally announced July 2021.

Comments: arXiv admin note: substantial text overlap with arXiv:2105.04110

Towards a Logic for Reasoning About LF Specifications

Authors: Mary Southern, Gopalan Nadathur

Abstract: We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, ty** 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 co… ▽ More We describe the development of a logic for reasoning about specifications in the Edinburgh Logical Framework (LF). In this logic, ty** 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 ty** 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. △ Less

Submitted 26 June, 2018; originally announced June 2018.

Comments: 9 pages

Schematic Polymorphism in the Abella Proof Assistant

Authors: Gopalan Nadathur, Yuting Wang

Abstract: 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 limi… ▽ More 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. △ Less

Submitted 19 June, 2018; originally announced June 2018.

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

Authors: Yuting Wang, Gopalan Nadathur

Abstract: 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 u… ▽ More 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. △ Less

Submitted 23 January, 2016; v1 submitted 12 September, 2015; originally announced September 2015.

A Lambda Prolog Based Animation of Twelf Specifications

Authors: Mary Southern, Gopalan Nadathur

Abstract: 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… ▽ More 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. △ Less

Submitted 6 July, 2014; originally announced July 2014.

Comments: 15 pages, accepted for presentation at the International Colloquium on Implementation of Constraint and Logic Programming Systems (CICLOPS) in Vienna

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

Authors: Mary Southern, Gopalan Nadathur

Abstract: 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 t… ▽ More 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. △ Less

Submitted 31 October, 2013; originally announced October 2013.

Comments: 14 pages, 11 figures

Towards Extracting Explicit Proofs from Totality Checking in Twelf

Authors: Yuting Wang, Gopalan Nadathur

Abstract: 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 o… ▽ More 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. △ Less

Submitted 5 July, 2013; originally announced July 2013.

Reasoning About Higher-Order Relational Specifications

Authors: Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur

Abstract: 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 reason… ▽ More 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. △ Less

Submitted 5 August, 2013; v1 submitted 11 February, 2013; originally announced February 2013.

Comments: Principles and Practice of Declarative Programming (2013)

Combining Deduction Modulo and Logics of Fixed-Point Definitions

Authors: David Baelde, Gopalan Nadathur

Abstract: 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… ▽ More 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. △ Less

Submitted 27 April, 2012; originally announced April 2012.

Comments: Long version of a paper accepted at LICS'12

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

Authors: Herman Geuvers, Gopalan Nadathur

Abstract: 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 im**e on their use in representing, implementing, and reasoning about a w… ▽ More 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 im**e 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. △ Less

Submitted 30 October, 2011; originally announced October 2011.

Journal ref: EPTCS 71, 2011

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

Authors: Zachary Snow, David Baelde, Gopalan Nadathur

Abstract: 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" notion, such calculi can also encode the correspondence between formulas and their proofs in ty** judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifica… ▽ More 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" notion, such calculi can also encode the correspondence between formulas and their proofs in ty** judgments. As such, these calculi provide a natural yet powerful means for specifying varied formal systems. Such specifications can be transformed into a more direct form that uses predicate formulas over simply typed lambda-terms and that thereby provides the basis for their animation using conventional logic programming techniques. However, a naive use of this idea is fraught with inefficiencies arising from the fact that dependently typed expressions typically contain much redundant ty** information. We investigate syntactic criteria for recognizing and, hence, eliminating such redundancies. In particular, we identify a property of bound variables in LF types called "rigidity" and formally show that checking that instantiations of such variables adhere to ty** restrictions is unnecessary for the purpose of ensuring that the overall expression is well-formed. We show how to exploit this property in a translation based approach to executing specifications in the Twelf language. Recognizing redundancy is also relevant to devising compact representations of dependently typed expressions. We highlight this aspect of our work and discuss its connection with other approaches proposed in this context. △ Less

Submitted 5 July, 2010; originally announced July 2010.

A Meta-Programming Approach to Realizing Dependently Typed Logic Programming

Authors: Zachary Snow, David Baelde, Gopalan Nadathur

Abstract: Dependently typed lambda calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the Twelf system is based on such an interpretation of LF. We consider here whether a conventional logic programming language can provide th… ▽ More Dependently typed lambda calculi such as the Logical Framework (LF) can encode relationships between terms in types and can naturally capture correspondences between formulas and their proofs. Such calculi can also be given a logic programming interpretation: the Twelf system is based on such an interpretation of LF. We consider here whether a conventional logic programming language can provide the benefits of a Twelf-like system for encoding type and proof-and-formula dependencies. In particular, we present a simple map** from LF specifications to a set of formulas in the higher-order hereditary Harrop (hohh) language, that relates derivations and proof-search between the two frameworks. We then show that this encoding can be improved by exploiting knowledge of the well-formedness of the original LF specifications to elide much redundant type-checking information. The resulting logic program has a structure that closely resembles the original specification, thereby allowing LF specifications to be viewed as hohh meta-programs. Using the Teyjus implementation of lambdaProlog, we show that our translation provides an efficient means for executing LF specifications, complementing the ability that the Twelf system provides for reasoning about them. △ Less

Submitted 24 May, 2010; originally announced May 2010.

ACM Class: D.3.2; F.4.1

A two-level logic approach to reasoning about computations

Authors: Andrew Gacek, Dale Miller, Gopalan Nadathur

Abstract: Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, ty**, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object lang… ▽ More Relational descriptions have been used in formalizing diverse computational notions, including, for example, operational semantics, ty**, and acceptance by non-deterministic machines. We therefore propose a (restricted) logical theory over relations as a language for specifying such notions. Our specification logic is further characterized by an ability to explicitly treat binding in object languages. Once such a logic is fixed, a natural next question is how we might prove theorems about specifications written in it. We propose to use a second logic, called a reasoning logic, for this purpose. A satisfactory reasoning logic should be able to completely encode the specification logic. Associated with the specification logic are various notions of binding: for quantifiers within formulas, for eigenvariables within sequents, and for abstractions within terms. To provide a natural treatment of these aspects, the reasoning logic must encode binding structures as well as their associated notions of scope, free and bound variables, and capture-avoiding substitution. Further, to support arguments about provability, the reasoning logic should possess strong mechanisms for constructing proofs by induction and co-induction. We provide these capabilities here by using a logic called G which represents relations over lambda-terms via definitions of atomic judgments, contains inference rules for induction and co-induction, and includes a special generic quantifier. We show how provability in the specification logic can be transparently encoded in G. We also describe an interactive theorem prover called Abella that implements G and this two-level logic approach and we present several examples that demonstrate the efficacy of Abella in reasoning about computations. △ Less

Submitted 1 September, 2010; v1 submitted 16 November, 2009; originally announced November 2009.

Comments: To appear in the Journal of Automated Reasoning

Nominal Abstraction

Authors: Andrew Gacek, Dale Miller, Gopalan Nadathur

Abstract: Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassi… ▽ More Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such descriptions: the interpretation of atomic judgments through recursive definitions and an encoding of binding constructs via generic judgments. However, logics encompassing these two features do not currently allow for the definition of relations that embody dynamic aspects related to binding, a capability needed in many reasoning tasks. We propose a new relation between terms called nominal abstraction as a means for overcoming this deficiency. We incorporate nominal abstraction into a rich logic also including definitions, generic quantification, induction, and co-induction that we then prove to be consistent. We present examples to show that this logic can provide elegant treatments of binding contexts that appear in many proofs, such as those establishing properties of ty** calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments. △ Less

Submitted 23 September, 2010; v1 submitted 10 August, 2009; originally announced August 2009.

Comments: To appear in the Journal of Information and Computation

Reasoning in Abella about Structural Operational Semantics Specifications

Authors: Andrew Gacek, Dale Miller, Gopalan Nadathur

Abstract: The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The treatment… ▽ More The approach to reasoning about structural operational semantics style specifications supported by the Abella system is discussed. This approach uses lambda tree syntax to treat object language binding and encodes binding related properties in generic judgments. Further, object language specifications are embedded directly into the reasoning framework through recursive definitions. The treatment of binding via generic judgments implicitly enforces distinctness and atomicity in the names used for bound variables. These properties must, however, be made explicit in reasoning tasks. This objective can be achieved by allowing recursive definitions to also specify generic properties of atomic predicates. The utility of these various logical features in the Abella system is demonstrated through actual reasoning tasks. Brief comparisons with a few other logic based approaches are also made. △ Less

Submitted 2 June, 2008; v1 submitted 24 April, 2008; originally announced April 2008.

Comments: 15 pages. To appear in LFMTP'08

Combining generic judgments with recursive definitions

Authors: Andrew Gacek, Dale Miller, Gopalan Nadathur

Abstract: Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that allow direct, logic-based reasoning about such descriptions: the treatment of atomic judgments as fixed points (recursive definitions) and an encoding of bin… ▽ More Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that allow direct, logic-based reasoning about such descriptions: the treatment of atomic judgments as fixed points (recursive definitions) and an encoding of binding constructs via generic judgments. However, the logics encompassing these two features have thus far treated them orthogonally: that is, they do not provide the ability to define object-logic properties that themselves depend on an intrinsic treatment of binding. We propose a new and simple integration of these features within an intuitionistic logic enhanced with induction over natural numbers and we show that the resulting logic is consistent. The pivotal benefit of the integration is that it allows recursive definitions to not just encode simple, traditional forms of atomic judgments but also to capture generic properties pertaining to such judgments. The usefulness of this logic is illustrated by showing how it can provide elegant treatments of object-logic contexts that appear in proofs involving ty** calculi and of arbitrarily cascading substitutions that play a role in reducibility arguments. △ Less

Submitted 14 April, 2008; v1 submitted 6 February, 2008; originally announced February 2008.

Comments: To appear in LICS 2008

A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi

Authors: Andrew Gacek, Gopalan Nadathur

Abstract: This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this calculus provides a cumbersome encoding of substitution composition, an operation that is important to the efficient realization of reduction. This encoding is… ▽ More This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this calculus provides a cumbersome encoding of substitution composition, an operation that is important to the efficient realization of reduction. This encoding is simplified here, resulting in a treatment that is easy to use directly in applications. The rationalization consists of the elimination of a practically inconsequential flexibility in the unravelling of substitutions that has the inadvertent side effect of losing contextual information in terms; the modified calculus now has a structure that naturally supports logical analyses, such as ones related to the assignment of types, over lambda terms. The overall calculus is shown to have pleasing theoretical properties such as a strongly terminating sub-calculus for substitution and confluence even in the presence of term meta variables that are accorded a grafting interpretation. Another contribution of the paper is the identification of a broad set of properties that are desirable for explicit substitution calculi to support and a classification of a variety of proposed systems based on these. The suspension calculus is used as a tool in this study. In particular, map**s are described between it and the other calculi towards understanding the characteristics of the latter. △ Less

Submitted 25 February, 2007; originally announced February 2007.

Comments: 38 pages

The Bedwyr system for model checking over syntactic expressions

Authors: David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu

Abstract: Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference ru… ▽ More Bedwyr is a generalization of logic programming that allows model checking directly on syntactic expressions possibly containing bindings. This system, written in OCaml, is a direct implementation of two recent advances in the theory of proof search. The first is centered on the fact that both finite success and finite failure can be captured in the sequent calculus by incorporating inference rules for definitions that allow fixed points to be explored. As a result, proof search in such a sequent calculus can capture simple model checking problems as well as may and must behavior in operational semantics. The second is that higher-order abstract syntax is directly supported using term-level $λ$-binders and the $\nabla$ quantifier. These features allow reasoning directly on expressions containing bound variables. △ Less

Submitted 25 April, 2008; v1 submitted 20 February, 2007; originally announced February 2007.

Comments: 6 page system description. Appeared in CADE 2007

Journal ref: CADE 2007: 21th Conference on Automated Deduction, Frank Pfenning, editor, LNAI 4603, pages 391-397. Springer, 2007

A treatment of higher-order features in logic programming

Authors: Gopalan Nadathur

Abstract: The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problem… ▽ More The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problems. One issue concerns the machine representation of lambda terms suitable to their intended use: an adequate encoding must facilitate comparison operations over terms in addition to supporting the usual reduction computation. Another aspect relates to the treatment of a unification operation that has a branching character and that sometimes calls for the delaying of the solution of unification problems. A final issue concerns the execution of goals whose structures become apparent only in the course of computation. These various problems are exposed in this paper and solutions to them are described. A satisfactory representation for lambda terms is developed by exploiting the nameless notation of de Bruijn as well as explicit encodings of substitutions. Special mechanisms are molded into the structure of traditional Prolog implementations to support branching in unification and carrying of unification problems over other computation steps; a premium is placed in this context on exploiting determinism and on emulating usual first-order behaviour. An extended compilation model is presented that treats higher-order unification and also handles dynamically emergent goals. The ideas described here have been employed in the Teyjus implementation of the Lambda Prolog language, a fact that is used to obtain a preliminary assessment of their efficacy. △ Less

Submitted 7 April, 2004; originally announced April 2004.

Comments: 50 pages, 4 figures, 2 tables. To appear in Theory and Practice of Logic Programming (TPLP)

ACM Class: D.3.2; D.3.3; D.3.4

Sco** Constructs in Logic Programming: Implementation Problems and their Solution

Authors: Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon

Abstract: The inclusion of universal quantification and a form of implication in goals in logic programming is considered. These additions provide a logical basis for sco** but they also raise new implementation problems. When universal and existential quantifiers are permitted to appear in mixed order in goals, the devices of logic variables and unification that are employed in solving existential goal… ▽ More The inclusion of universal quantification and a form of implication in goals in logic programming is considered. These additions provide a logical basis for sco** but they also raise new implementation problems. When universal and existential quantifiers are permitted to appear in mixed order in goals, the devices of logic variables and unification that are employed in solving existential goals must be modified to ensure that constraints arising out of the order of quantification are respected. Suitable modifications that are based on attaching numerical tags to constants and variables and on using these tags in unification are described. The resulting devices are amenable to an efficient implementation and can, in fact, be assimilated easily into the usual machinery of the Warren Abstract Machine (WAM). The provision of implications in goals results in the possibility of program clauses being added to the program for the purpose of solving specific subgoals. A naive scheme based on asserting and retracting program clauses does not suffice for implementing such additions for two reasons. First, it is necessary to also support the resurrection of an earlier existing program in the face of backtracking. Second, the possibility for implication goals to be surrounded by quantifiers requires a consideration of the parameterization of program clauses by bindings for their free variables. Devices for supporting these additional requirements are described as also is the integration of these devices into the WAM. Further extensions to the machine are outlined for handling higher-order additions to the language. The ideas presented here are relevant to the implementation of the higher-order logic programming language lambda Prolog. △ Less

Submitted 10 September, 1998; originally announced September 1998.

Comments: 46 pages

ACM Class: D.3.2

Journal ref: Journal of Logic Programming, 25(2)-119:161, 1995

Correspondences between Classical, Intuitionistic and Uniform Provability

Authors: Gopalan Nadathur

Abstract: Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform provability, a restriction of intuitionistic provability that embodies a special form of goal-directedness. We determine, first, the circumstances in which the… ▽ More Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform provability, a restriction of intuitionistic provability that embodies a special form of goal-directedness. We determine, first, the circumstances in which the former relations imply the latter. Using this result, we identify the richest versions of the so-called abstract logic programming languages in classical and intuitionistic logic. We then study the reduction of classical and, derivatively, intuitionistic provability to uniform provability via the addition to the assumption set of the negation of the formula to be proved. Our focus here is on understanding the situations in which this reduction is achieved. However, our discussions indicate the structure of a proof procedure based on the reduction, a matter also considered explicitly elsewhere. △ Less

Submitted 10 September, 1998; originally announced September 1998.

Comments: 31 pages

Report number: University of Chicago, CS Dept, TR-97-12 ACM Class: F.4.1

Uniform Provability in Classical Logic

Authors: Gopalan Nadathur

Abstract: Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We investigate the relevance of this uniform proof notion to structuring proof search in classical logic. A logical language in whose context provability is equivale… ▽ More Uniform proofs are sequent calculus proofs with the following characteristic: the last step in the derivation of a complex formula at any stage in the proof is always the introduction of the top-level logical symbol of that formula. We investigate the relevance of this uniform proof notion to structuring proof search in classical logic. A logical language in whose context provability is equivalent to uniform provability admits of a goal-directed proof procedure that interprets logical symbols as search directives whose meanings are given by the corresponding inference rules. While this uniform provability property does not hold directly of classical logic, we show that it holds of a fragment of it that only excludes essentially positive occurrences of universal quantifiers under a modest, sound, modification to the set of assumptions: the addition to them of the negation of the formula being proved. We further note that all uses of the added formula can be factored into certain derived rules. The resulting proof system and the uniform provability property that holds of it are used to outline a proof procedure for classical logic. An interesting aspect of this proof procedure is that it incorporates within it previously proposed mechanisms for dealing with disjunctive information in assumptions and for handling hypotheticals. Our analysis sheds light on the relationship between these mechanisms and the notion of uniform proofs. △ Less

Submitted 10 September, 1998; originally announced September 1998.

Comments: 23 pages

ACM Class: F.4.1

Journal ref: Journal of Logic and Computation, Vol 8, No 96-15, pp 209-229, 1998