1 citations · 1 across the 4 of their papers we have counts for
5 papers
Combining generic judgments with recursive definitions
Andrew Gacek, Dale Miller, Gopalan Nadathur
Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Rece…
A Simplified Suspension Calculus and its Relationship to Other Explicit Substitution Calculi
Andrew Gacek, Gopalan Nadathur
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 th…
The Bedwyr system for model checking over syntactic expressions
David Baelde, Andrew Gacek, Dale Miller +2
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 direc…
A treatment of higher-order features in logic programming
Gopalan Nadathur
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 calcu…
Scoping Constructs in Logic Programming: Implementation Problems and their Solution
Gopalan Nadathur, Bharat Jayaraman, Keehang Kwon
The inclusion of universal quantification and a form of implication in goals in logic programming is considered. These additions provide a logical basis for scoping but they also r…