Healfdene Goguen
Research Fellow
LFCS, Department of Computer Science
University of Edinburgh
JCMB, The King's Buildings
Edinburgh, EH9 3JZ
United Kingdom
hhg@dcs.ed.ac.uk
I now work for .
I used to be a member of the LEGO
Project in the European
TYPES Project.
I worked for one year in Projet CROAP at
INRIA.
You can find more information in my CV.
Papers

H. Goguen, R. Brooksby and R. Burstall.
An Abstract Formulation of Memory Management. Submitted to TYPES
Proceedings 1999.

H. Goguen and
A. Compagnoni. AntiSymmetry
of HigherOrder Subtyping. CSL, September 1999.

H. Goguen and
J. GoubaultLarrecq. Sequent
Combinators: A Hilbert System for the Lambda Calculus.
MSCS (2000), vol. 10, pp. 1  79. Submitted in
celebration of the 60th birthday of Roger
Hindley, November 1998. An earlier version appeared as
LFCS
Technical Report ECSLFCS97357, University of
Edinburgh, May 1997.

H. Goguen.
Soundness of Typed Operational Semantics for the Logical
Framework. TLCA,
April 1999.
 A. Compagnoni and
H. Goguen.
Decidability of higherorder subtyping via logical relations.
December 1997.
 A. Compagnoni and
H. Goguen.
Typed Operational Semantics for Higher Order Subtyping. LFCS
Technical Report ECSLFCS97361, University of Edinburgh, July 1997.
Submitted for publication.

H. Goguen and J. McKinna.
Candidates for Substitution. LFCS Technical Report
ECSLFCS97358, University of Edinburgh, May 1997.

H. Goguen.
Encoding Inductive Datatypes via the WType in Intensional Type
Theory. Draft, Apr. 1997. Comments welcome.

H. Goguen.
The Metatheory of UTT. In Types for Proofs and Programs,
volume 996 of Lecture Notes in Computer Science, pages 6082.
SpringerVerlag, 1995.

H. Goguen.
Typed Operational Semantics. In Proceedings of the
International Conference on Typed Lambda Calculi and Applications,
volume 902 of Lecture Notes in Computer Science, pages 186200.
SpringerVerlag, 1995.

H. Goguen.
A Typed Operational Semantics for Type Theory. PhD thesis,
University of Edinburgh, Aug. 1994. LFCS Report ECSLFCS94304. I
also have a
version compiled to use less space.

H. Goguen and Z. Luo.
Inductive Data Types: Wellordering Types Revisited.
In G. Huet and G. Plotkin, editors, Logical Environments.
Cambridge University Press, 1993.