René M. C. Ahn
: Communication Contexts: a Pragmatic Approach to Information Exchange.
: A short and flexible proof of Strong Normalization for the Calculus of Constructions.
: Codifying Guarded Definitions with Recursive Schemes.
: A User's Friendly Syntax to Define Recursive Functions as Typed lambda-Terms.
: Syntactic Categories in the Language of Mathematics.
: Formalization of a lamda-Calculus with Explicit Substitutions in Coq.