: Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation.
: Representing and Reasoning with Operational Semantics.
Chad E. Brown
: Combining Type Theory and Untyped Set Theory.
: Eliminating Redundancy in Higher-Order Unification: A Lightweight Approach.
: First-Order Logic with Dependent Types.
: Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials.
: On the Strength of Proof-Irrelevant Type Theories.