The Metatheory of UTT. - Healfdene Goguen (TYPES, 1994)

A typed operational semantics for type theory. - Healfdene Goguen (1994)

Typed Operational Semantics. - Healfdene Goguen (TLCA, 1995)

Anti-Symmetry of Higher-Order Subtyping. - Adriana B. Compagnoni; Healfdene Goguen (CSL, 1999)

Soundness of the Logical Framework for Its Typed Operational Semantics. - Healfdene Goguen (TLCA, 1999)

Memory Management: An Abstract Formulation of Incremental Tracing. - Healfdene Goguen; Richard Brooksby; Rod M. Burstall (TYPES, 1999)

A Kripke-Style Model for the Admissibility of Structural Rules. - Healfdene Goguen (TYPES, 2000)

Sequent combinators: a Hilbert system for the lambda calculus. - Healfdene Goguen; Jean Goubault-Larrecq (Math. Struct. Comput. Sci., 2000)

Typed operational semantics for higher-order subtyping. - Adriana B. Compagnoni; Healfdene Goguen (Inf. Comput., 2003)

A Few Constructions on Constructors. - Conor McBride; Healfdene Goguen; James McKinna (TYPES, 2004)

Component coordination: a telecommunication case study. - Pamela Zave; Healfdene Goguen; Thomas M. Smith (Comput. Networks, 2004)

Experience with Component-Based Development of a Telecommunication Service. - Gregory W. Bond; Eric Cheung; Healfdene Goguen; Karrie J. Hanson; Don Henderson; Gerald M. Karam; K. Hal Purdy; Thomas M. Smith; Pamela Zave (CBSE, 2005)

Justifying Algorithms for beta-eta-Conversion. - Healfdene Goguen (FoSSaCS, 2005)

A syntactic approach to eta equality in type theory. - Healfdene Goguen (POPL, 2005)

Eliminating Dependent Pattern Matching. - Healfdene Goguen; Conor McBride; James McKinna (Essays Dedicated to Joseph A. Goguen, 2006)

Anti-symmetry of higher-order subtyping and equality by subtyping. - Adriana B. Compagnoni; Healfdene Goguen (Math. Struct. Comput. Sci., 2006)

Theory and applications of subtyping: Introduction. - Adriana B. Compagnoni; Healfdene Goguen (Math. Struct. Comput. Sci., 2008)

Relating Church-Style and Curry-Style Subtyping - Adriana B. Compagnoni; Healfdene Goguen (ITRS, 2010)