Tuesday, August 15, 2006

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.

Monday, August 07, 2006

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.