1 citations · 1 across the 4 of their papers we have counts for
4 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 Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi
Andrew Gacek
The intrinsic treatment of binding in the lambda calculus makes it an ideal data structure for representing syntactic objects with binding such as formulas, proofs, types, and prog…
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…