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. Anti-Symmetry of Higher-Order Subtyping. CSL, September 1999.
• H. Goguen and J. Goubault-Larrecq. 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 ECS-LFCS-97-357, 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 higher-order subtyping via logical relations. December 1997.
• A. Compagnoni and H. Goguen. Typed Operational Semantics for Higher Order Subtyping. LFCS Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. Submitted for publication.
• H. Goguen and J. McKinna. Candidates for Substitution. LFCS Technical Report ECS-LFCS-97-358, University of Edinburgh, May 1997.
• H. Goguen. Encoding Inductive Datatypes via the W-Type 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 60-82. Springer-Verlag, 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 186-200. Springer-Verlag, 1995.
• H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994. LFCS Report ECS-LFCS-94-304. I also have a version compiled to use less space.
• H. Goguen and Z. Luo. Inductive Data Types: Well-ordering Types Revisited. In G. Huet and G. Plotkin, editors, Logical Environments. Cambridge University Press, 1993.