About

Gopalan Nadathur's research and teaching focus on the foundational aspects of computer science. He has taught courses on programming languages and programming principles, compilation, logic, and computability theory. His research has spanned topics in computational logic, structural proof theory, and logic-based programming languages and their implementation. At a practical level, he has collaboratively developed implementations of languages and proof assistants that are useful in formally specifying and reasoning about computational systems described in a rule-based fashion. Gopalan Nadathur joined the Department of Computer Science & Engineering at the University of Minnesota in 2000, after receiving his Ph.D. in computer science from the University of Pennsylvania. Prior to his current position, he was a faculty member at Duke University, the University of Chicago, and Loyola University Chicago, and has held visiting professorships at several international institutions, including the University of Munich, Ecole Polytechnique in France, the Australian National University, the IT University of Copenhagen, and IIT Delhi. He has also served as a visiting Director of Research at Inria in Nancy.

Research topics

• Computer Science
• Theoretical computer science
• Programming language
• Mathematics

Selected publications

• A Modular Approach to Metatheoretic Reasoning for Extensible Languages

  ACM Transactions on Programming Languages and Systems · 2025-05-07

  article

  This article concerns the development of metatheory for extensible languages. It starts with the 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 this context, 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 by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of modular metatheory , by which we mean that proofs of relevant properties should be constructible 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. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called Sterling and a proof assistant called Extensibella and have used them to validate the examples that motivate the theoretical discussions.

  PublisherDOI

• Ground Stratification for a Logic of Definitions with Induction

  Electronic Proceedings in Theoretical Computer Science · 2025-10-13

  articleOpen accessSenior author

  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.

  PublisherOA PDFDOI

• Binding Contexts as Partitionable Multisets in Abella

  Electronic Proceedings in Theoretical Computer Science · 2024-07-08 · 1 citations

  articleOpen accessSenior author

  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.

  PublisherOA PDFDOI

• A Modular Approach to Metatheoretic Reasoning for Extensible Languages

  arXiv (Cornell University) · 2023-12-22 · 1 citations

  preprintOpen access

  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.

  PublisherOA PDFDOI

• Modularity and Separate Compilation in Logic Programming

  arXiv (Cornell University) · 2023

  Senior authorCorresponding
  • Computer Science
  • Computer Science
  • Programming language

  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.

  PublisherOA PDFDOI

• A Logic for Formalizing Properties of LF Specifications

  2022-09-20

  article1st authorCorresponding

  A logic is presented for formalizing properties of specifications in the Edinburgh Logical Framework or LF. In this logic, typing judgments in LF serve as atomic formulas and quantification is permitted over LF terms and contexts. Quantifiers of the first variety are qualified by simple types that describe the functional structure associated with the variables they bind. Quantifiers over contexts are typed by context schemas that constrain their instantiations to adhere to a regular structure. The semantics of the logic is based ultimately on an understanding of derivability in LF. As such, valid formulas in the logic represent meta-theoretic properties of object systems that are encoded via LF signatures. The logic is complemented by a proof system that is briefly discussed. There are two categories to the rules in this proof system. One collection of rules captures the meanings of logical connectives and quantifiers. Another collection provides a means for analyzing atomic formulas based on an understanding of derivability in LF; these rules build in the capability for a case-analysis style reasoning about LF judgements and for induction over the heights of LF derivations.

  PublisherDOI

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

  arXiv (Cornell University) · 2021-08-24

  preprintOpen access1st authorCorresponding

  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.

  PublisherOA PDFDOI

• A Logic for Reasoning About LF Specifications

  arXiv (Cornell University) · 2021-06-30

  preprintOpen access1st authorCorresponding

  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.

  PublisherOA PDFDOI

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

  arXiv (Cornell University) · 2021-12-17

  preprintOpen access1st authorCorresponding

  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.

  PublisherOA PDFDOI

• A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday

  Mathematical Structures in Computer Science · 2019-09-01

  articleOpen access

  The genesis of this special issue was in a meeting that took place at Université Paris Diderot on December 15 and 16, 2016. Dale Miller, Professor at École polytechnique, had turned 60 a few days earlier. In a career spanning over three decades and in work conducted in collaboration with several students and colleagues, Dale had had a significant influence in an area that can be described as structural proof theory and its application to computation and reasoning. In recognition of this fact, several of his collaborators thought it appropriate to celebrate the occasion by organizing a symposium on topics broadly connected to his areas of interest and achievements. The meeting was a success in several senses: it was attended by over 35 people, there were 15 technical presentations describing new results, and, quite gratifyingly, we managed to spring the event as a complete surprise to Dale.

  PublisherOA PDFDOI

Recent grants

• SHF:Small:Reasoning about Specifications of Computations

  NSF · $568k · 2009–2014

• Supporting Higher-Order Approaches to Symbolic Computation

  NSF · $238k · 2004–2009

• SHF: Small: A Higher-Order Framework for Meta-Theoretic Reasoning

  NSF · $558k · 2016–2022

Frequent coauthors

• Dale Miller

  École Polytechnique

  77 shared

• Jörn Richts

  74 shared

• Bernhard Gramlich

  74 shared

• Christophe Ringeissen

  74 shared

• Uwe Waldmann

  74 shared

• Anne-Cécile Caron

  74 shared

• Philippe de Groote

  Centre National de la Recherche Scientifique

  74 shared

• Denis Lugiez

  Laboratoire d’Informatique et Systèmes

  74 shared

Labs

• Gopalan NadathurPI

Awards & honors

• Selected Grants SHF: Small: A Higher-Order Framework for Met…
• Towards the verified compilation of functional languages
• SHF: Small: Reasoning about Specifications of Computation