Healfdene Goguen

Address

Department of Computer Science The King’s Buildings University of Edinburgh Edinburgh, EH9 3JZ, United Kingdom

Telephone: (+44) (131) 650-5152 FAX: (+44) (131) 667-7209

EMail: hhg@dcs.ed.ac.uk
WWW: http://www.dcs.ed.ac.uk/home/hhg

Qualifications

Through my education and professional experience, I have acquired a rare combination of practical and theoretical skills. In my work at AT&T I gained ex-

tensive knowledge of C and Unix, and more recently I have worked on user interfaces and memory management systems. In my PhD and subsequent research experience I have studied type systems, allowing expressive but secure programs, and formalisms for concurrency, allowing the abstract study of properties such as deadlock for distributed systems. This combination of analytic and implementation skills makes me uniquely qualified to design and implement reliable software systems.

Professional Experiences

University of Edinburgh, United Kingdom: October 1995 – Present. Research Fellow. Ongoing collaboration with Harlequin Ltd on an abstract understanding of memory management together with Prof. Burstall and Dr Paul Jackson, which to date has saved the company project an estimated 6 months implementation time. Theoretical work on type-theoretic foundations of objectoriented programming languages, combinators and explicit substitution, and inductive types in type theory.

Acting Research Fellow representative on Advisory Board to the LFCS. Acting manager of technical maintenance of the Lego computer-aided proof assistant at Edinburgh. Second supervisor for graduated student Dr David Aspinall and PhD students Tim Heap, Conor McBride and Claudio Russo, whose projects include module systems for SML and dependent pattern matching. Gave a postgraduate course on topics in type theory alone in 1997 and together with Dr James McKinna in 1996. Deputy head of Lego project between July and September 1996 and in June 1997. Supervised French Master’s Candidate Sylvan Boulmé together with Dr James McKinna. Updated and maintained World Wide Web site for Esprit Basic Research Action “Types”.

University of Cambridge, United Kingdom: October 1996 – December 1996. Visiting Scholar. Research as above.

INRIA Sophia–Antipolis, France: September 1994 – September 1995. National Science Foundation NATO Postdoctoral Scholar. Work on Centaur environment and CtCoq interface to Coq theorem prover. Theoretical work on systems of explicit substitution.

AT&T Bell Laboratories: March 1983 – August 1992. Worked part-time during academic year and full-time during summers. Involved in a variety of implementation projects, including porting device drivers and X servers to Unix, developing a schematic capture and layout tool for VLSI Design Automation Assistant, and adding a datatype package to HOL, a theorem prover based on higher-order classical logic.

Also primary developer of a C interpreter and incremental loader implemented on a wide variety of platforms. These tools form the core of an integrated C programming environment that became an AT&T product.

Education

University of Edinburgh, United Kingdom: October 1989 – September 1994 PhD Student at the Laboratory for Foundations of Computer Science (LFCS) Supervisors: Dr Zhaohui Luo, Prof. Rod Burstall Thesis title: A Typed Operational Semantics for Type Theory Summary: Provides the theoretical basis for confidence in UTT, a uniform language of programs, specifications and proofs of correctness underlying the computer-aided proof assistant Lego. Introduces a new technique, typed operational semantics, for developing such a theoretical basis.

Carnegie-Mellon University, Pittsburgh, PA: August 1985 – May 1988 Bachelor of Science in Applied Mathematics (Computer Science)

Honors

1993 National Science Foundation NATO Postdoctoral Scholarship

1989 National Science Foundation PhD Studentship Honorable Mention

1985 Second place in Physics, New Jersey State Science Day

1984 National Merit Honorable Mention

Personal

Birth Date: 25 December 1967 Birth Place: Berkeley, CA
Citizenship: USA  Marital Status: Single

Languages:

My native language is English, and I am fluent in French and Spanish.

References

[1] Healfdene Goguen, Richard Brooksby and Rod Burstall. An Abstract Formulation of Memory Management. Draft, February 1998.

[2] Adriana Compagnoni and Healfdene Goguen. Decidability of higher-order subtyping via logical relations, December 1997.

[3] J. Bertot, Y. Bertot, Y. Coscoy, H. Goguen, and F. Montagnac. User Guide to the CtCoq Proof Environment. Technical Report 0210, INRIA, October 1997.

[4] Adriana Compagnoni and Healfdene Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. Submitted to Information and Computation.

[5] Healfdene Goguen and James McKinna. Candidates for substitution. Technical Report ECS-LFCS-97-358, University of Edinburgh, May 1997. Submitted to Theoretical Computer Science.

[6] Healfdene Goguen. Sequent combinators: A Hilbert system for the lambda calculus. Technical Report ECS-LFCS-97-357, University of Edinburgh, May 1997.

[7] Healfdene Goguen. Encoding inductive datatypes via the W -type in intensional type theory, April 1997.

[8] Healfdene Goguen. The metatheory of UTT. In Types for Proofs and Programs, volume 996 of Lecture Notes in Computer Science, pages 60–82, Baastad, Sweden, June 1995. Springer–Verlag.

[9] Healfdene 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.

[10] Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994.

[11] Healfdene Goguen and Zhaohui Luo. Inductive data types: Well-ordering types revisited. In Gérard Huet and Gordon Plotkin, editors, Logical Environments, pages 198–218. Cambridge University Press, 1993.

[12] T. J. Kowalski, C. R. Seaquist, B. Ellis, H. H. Goguen, J. J. Puttress, J. R. Rowland, C. A. Rath, J. M. Wilson, G. T. Vesonder, and J. L. Schmidt. A reflective C and C++ programming environment. In Proceedings of the International Workshop on UNIX-Based Software Development Environments, Dallas, TX, January 1991. USENIX.

[13] T. J. Kowalski, H. H. Goguen, and J. J. Puttress. The C interpreter: A tutorial for cin version 0.18. In A. Hume, editor, UNIX Programmer’s Manual, Tenth Edition, volume 2. Saunders College Publishing, December 1989.

[14] J. J. Puttress and H. H. Goguen. Incremental loading of subroutines at runtime. Technical report, AT&T Bell Laboratories, 1986.

Referees

Professor Rod Burstall Telephone: (+44) (131) 650-5155 FAX: (+44) (131) 667-7209

EMail: rb@dcs.ed.ac.uk

Dept. of Computer Science The King’s Buildings University of Edinburgh Edinburgh, EH9 3JZ, UK Dr Zhaohui Luo Telephone: (+44) (191) 374-3657

                                EMail: Z.Luo@durham.ac.uk

Dept. of Computer Science University of Durham South Road Durham, DH1 3LE, UK

Professor Jan Smith Telephone: (+46) (31) 772-1034 FAX: (+46) (31) 16 56 55

EMail: smith@cs.chalmers.se

Dept. of Computer Sciences Chalmers Univ. of Technology S-412 96, Goteborg, Sweden Dr Gilles Kahn Telephone: (+33) 93.65.78.01 FAX: (+33) 93.65.76.33

                                EMail: kahn@sophia.inria.fr

INRIA, 2004, route des Lucioles B. P. 93 Sophia–Antipolis 06902 France

Dr Thaddeus J. Kowalski Telephone: (+1) (800) 382-2613

EMail: frodo@grumpy.research.att.com

AT&T, Room ELC105 290 Davidson Avenue Somerset, NJ, 08875-6742, USA