Software Projects

I was a principal feature developer for AT&T CallVantage, together with Tom Smith. I developed Locate Me, n-Way Calling, Record and Send and other features, as well as a remote worker business application controlling multiple phone lines through a GUI.

As part of the AT&T CallVantage development, Greg Bond and I developed a hierarchical finite state machine for programming telephony features. An open source implementation of this language is available.

I was a co-supervisor of Conor McBride's PhD thesis, and I provided insight that led to an algorithm for constructor unification for dependent type theories. This algorithm is now at the heart of the implementation of Epigram.

Publications

• H. Goguen, C. McBride and J. McKinna. Eliminating Dependent Pattern Matching. Joseph Goguen Festschrift, Lecture Notes in Computer Science, vol. 4060, pp. 521-540. Springer-Verlag, June 2006.
  
  
• A. Compagnoni and H. Goguen. Anti-Symmetry of Higher-Order Subtyping. Mathematical Structures in Computer Science, vol. 16(1), pp. 41-65, Feb. 2006.
  
  
• C. McBride, H. Goguen and J. McKinna. A Few Constructions on Constructors. Proceedings of TYPES 2004, Lecture Notes in Computer Science, vol. 3839, pp. 186-200. Springer-Verlag, 2004.
  
  
• G. Bond, E. Cheung, H. Goguen, K. Hanson, D. Henderson, G. Karam, K. Purdy, T. Smith and P. Zave. Experience with component-based development of a telecommunication service. International Symposium on Component-Based Software Engineering, 2005.
  
  
• H. Goguen. Justifying Algorithms for beta-eta Conversion. Foundations of Software Science and Computational Structures, Lecture Notes in Computer Science, vol. 3441, pp. 410-424. Springer-Verlag, 2005.
  
  
• H. Goguen. A Syntactic Approach to Eta Equality in Type Theory. Proceedings of Principles of Programming Languages, pp. 75-84, 2005.
  
  
• P. Zave, H. Goguen and T. Smith. Component Coordination: A Telecommunication Case Study. Computer Networks, 45(5), pp. 645-664, Aug. 2004.
  
  
• A. Compagnoni and H. Goguen. Typed Operational Semantics for Higher-Order Subtyping. Information and Computation, Aug. 2003, vol. 184, pp. 242-297. An earlier version appears as LFCS Technical Report ECS-LFCS-97-361.
  
  
• G. Bond and H. Goguen. ECLIPSEcharts: A Visual Bridge from Design to Implementation. AT&T Software Symposium 2002 Proceedings.
  
  
• G. Bond and H. Goguen. ECharts: Balancing Design and Implementation. Proceedings of the 6th IASTED International Conference on Software Engineering and Applications, pp. 149-155. ACTA Press, 2002.
  
  
• H. Goguen. A Kripke-Style Model for the Admissibility of Structural Rules. TYPES 2000 Proceedings, Lecture Notes in Computer Science, vol. 2277, pp. 112-124. Springer-Verlag, 2002.
  
  
• H. Goguen, R. Brooksby and R. Burstall. An Abstract Formulation of Memory Management. TYPES 1999 Proceedings, Lecture Notes in Computer Science, vol. 1956, pp. 148-161. Springer-Verlag, 2000.
  
  
• A. Compagnoni and H. Goguen. Anti-Symmetry of Higher-Order Subtyping. Computer Science Logic, Lecture Notes in Computer Science, vol. 1683, pp. 420-438. Springer-Verlag, 1999.
  
  
• H. Goguen and J. Goubault-Larrecq. Sequent Combinators: A Hilbert System for the Lambda Calculus. Mathematical Structures in Computer Science (2000), vol. 10, pp. 1-79. Submitted in celebration of the 60th birthday of Roger Hindley, Nov. 1998.
  
  
• H. Goguen. Soundness of Typed Operational Semantics for the Logical Framework. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 1581, pp. 177-197. Springer-Verlag, 1999.
  
  
• H. Goguen and J. McKinna. Candidates for Substitution. LFCS Technical Report ECS-LFCS-97-358, University of Edinburgh, May 1997.a
  
  
• H. Goguen. The Metatheory of UTT. In Types for Proofs and Programs, Lecture Notes in Computer Science, vol. 996, pp. 60-82. Springer-Verlag, 1995.
  
  
• H. Goguen. Typed Operational Semantics. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Computer Science, vol. 902, pp. 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.
  
  
• 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.