tag:blogger.com,1999:blog-297642602011-10-24T12:24:46.874-04:00I'm a software engineer at Google, working on large-scale infrastructure. Formerly I worked at AT&T Labs, where I was the primary feature developer for AT&T CallVantage. I have a PhD from the University of Edinburgh on type theory, and I was a researcher at France's INRIA and at the University of Edinburgh. My wife is Adriana Compagnoni, at Stevens Institute of Technology. We have two children, Nicholas and Kaitlin.hhghttp://www.blogger.com/profile/12671002162357946985noreply@blogger.comBlogger21100tag:blogger.com,1999:blog-29764260.post-32940566311715494832006-08-15T17:35:00.000-04:002006-08-15T17:44:04.604-04:00I was a principal feature developer for <a href="http://www.callvantage.att.com">AT&amp;T CallVantage</a>, 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.<br /><br />As part of the AT&amp;T CallVantage development, Greg Bond and I developed a hierarchical finite state machine for programming telephony features. An <a href="http://echarts.org">open source implementation</a> of this language is available.<br /><br />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 <a href="http://e-pig.org">Epigram</a>.<div class="blogger-post-footer"><img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/29764260-3294056631171549483?l=healf.blogspot.com' alt='' /></div>hhghttp://www.blogger.com/profile/12671002162357946985noreply@blogger.com48tag:blogger.com,1999:blog-29764260.post-1154991956043909112006-08-07T18:53:00.000-04:002006-08-07T19:08:26.793-04:00<ul><br /><br /><li> H. Goguen, C. McBride and J. McKinna. <a href="http://www.dcs.st-andrews.ac.uk/~james/RESEARCH/concon.pdf">Eliminating Dependent Pattern Matching</a>. Joseph Goguen Festschrift, <i>Lecture Notes in Computer Science</i>, vol. 4060, pp. 521-540. Springer-Verlag, June 2006.<br /><br /><li> A. Compagnoni and H. Goguen. <a href="http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=412869&fulltextType=RA&fileId=S0960129505005086">Anti-Symmetry of Higher-Order Subtyping</a>. Mathematical Structures in Computer Science, vol. 16(1), pp. 41-65, Feb. 2006.<br /><br /><li> C. McBride, H. Goguen and J. McKinna. <a href="http://www.e-pig.org/downloads/goguen.pdf">A Few Constructions on Constructors</a>. <i>Proceedings of TYPES 2004</i>, <i>Lecture Notes in Computer Science</i>, vol. 3839, pp. 186-200. Springer-Verlag, 2004.<br /><br /><li> G. Bond, E. Cheung, H. Goguen, K. Hanson, D. Henderson, G. Karam, K. Purdy, T. Smith and P. Zave. <a href="http://www.springerlink.com/index/10.1007/11424529_20">Experience with component-based development of a telecommunication service</a>. <i>International Symposium on Component-Based Software Engineering</i>, 2005.<br /><br /><li> H. Goguen. <a href="http://www.esnips.com/doc/667cf214-8247-40d1-b74e-36f796377aa1/fossacs05.pdf">Justifying Algorithms for beta-eta Conversion</a>. <i>Foundations of Software Science and Computational Structures</i>, <i>Lecture Notes in Computer Science</i>, vol. 3441, pp. 410-424. Springer-Verlag, 2005.<br /><br /><li> H. Goguen. <a href="http://esnips.com/doc/b2dcac4c-aa57-4047-925d-abb8ba01d333/eta.pdf">A Syntactic Approach to Eta Equality in Type Theory</a>. Proceedings of <i>Principles of Programming Languages</i>, pp. 75-84, 2005.<br /><br /><li> P. Zave, H. Goguen and T. Smith. <a href="http://portal.acm.org/citation.cfm?id=1031822&dl=GUIDE&coll=&CFID=15151515&CFTOKEN=6184618">Component Coordination: A Telecommunication Case Study</a>. <i>Computer Networks</i>, 45(5), pp. 645-664, Aug. 2004.<br /><br /><li> <a href="http://www.cs.stevens-tech.edu/~abc"> A. Compagnoni</a> and H. Goguen. <a href="http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=AUTHORALERT&_method=citationSearch&_piikey=S0890540103000622&_version=1&md5=d5eb41430d3d6b49f728c81c57fee511">Typed Operational Semantics for Higher-Order Subtyping</a>. <i>Information and Computation</i>, Aug. 2003, vol. 184, pp. 242-297. An earlier version appears as <a href="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/97/ECS-LFCS-97-361/index.html">LFCS Technical Report ECS-LFCS-97-361</a>.<br /><br /><li> <a href="http://www.research.att.com/info/bond"> G. Bond</a> and H. Goguen. ECLIPSEcharts: A Visual Bridge from Design to Implementation. AT&T Software Symposium 2002 Proceedings.<br /><br /><li> <a href="http://www.research.att.com/info/bond"> G. Bond</a> and H. Goguen. ECharts: Balancing Design and Implementation. Proceedings of the 6th IASTED <i>International Conference on Software Engineering and Applications</i>, pp. 149-155. ACTA Press, 2002.<br /><br /><li> H. Goguen. A Kripke-Style Model for the Admissibility of Structural Rules. TYPES 2000 Proceedings, <i>Lecture Notes in Computer Science</i>, vol. 2277, pp. 112-124. Springer-Verlag, 2002.<br /><br /><li> H. Goguen, R. Brooksby and <a href="http://www.dcs.ed.ac.uk/~rb">R. Burstall</a>. An Abstract Formulation of Memory Management. TYPES 1999 Proceedings, <i>Lecture Notes in Computer Science</i>, vol. 1956, pp. 148-161. Springer-Verlag, 2000.<br /><br /><li> <a href="http://www.cs.stevens-tech.edu/~abc">A. Compagnoni</a> and H. Goguen. Anti-Symmetry of Higher-Order Subtyping. <i>Computer Science Logic</i>, <i>Lecture Notes in Computer Science</i>, vol. 1683, pp. 420-438. Springer-Verlag, 1999.<br /><br /><li> H. Goguen and <a href="http://www.lsv.ens-cachan.fr/~goubault/">J. Goubault-Larrecq</a>. Sequent Combinators: A Hilbert System for the Lambda Calculus. <a href="http://uk.cambridge.org/journals/journal_catalogue.asp?mnemonic=MSC">Mathematical Structures in Computer Science</a> (2000), vol. 10, pp. 1-79. Submitted in celebration of the 60th birthday of <a href="http://www-maths.swan.ac.uk/staff/jrh/"> Roger Hindley</a>, Nov. 1998.<br /><br /><li> H. Goguen. Soundness of Typed Operational Semantics for the Logical Framework. In <i> Proceedings of the International Conference on Typed Lambda Calculi and Applications</i>, <i>Lecture Notes in Computer Science</i>, vol. 1581, pp. 177-197. Springer-Verlag, 1999.<br /><br /><li> H. Goguen and <a href="http://www.dur.ac.uk/j.h.mckinna"> J. McKinna</a>. <a href="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/97/ECS-LFCS-97-358/index.html">Candidates for Substitution</a>. LFCS Technical Report ECS-LFCS-97-358, University of Edinburgh, May 1997.a<br /><br /><li> H. Goguen. The Metatheory of UTT. In <i>Types for Proofs and Programs</i>, <i>Lecture Notes in Computer Science</i>, vol. 996, pp. 60-82. Springer-Verlag, 1995.<br /><br /><li> H. Goguen. Typed Operational Semantics. In <i> Proceedings of the International Conference on Typed Lambda Calculi and Applications</i>, <i>Lecture Notes in Computer Science</i>, vol. 902, pp. 186-200. Springer-Verlag, 1995.<br /><br /><li> H. Goguen. <a href="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/94/ECS-LFCS-94-304/index.html">A Typed Operational Semantics for Type Theory</a>. PhD thesis, University of Edinburgh, Aug. 1994. LFCS Report ECS-LFCS-94-304.<br /><br /><li> H. Goguen and <a href="http://www.cs.rhul.ac.uk/~zhaohui"> Z. Luo</a>. <a href="http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/92/ECS-LFCS-92-209/index.html">Inductive Data Types: Well-ordering Types Revisited</a>. In G. Huet and G. Plotkin, editors, <i>Logical Environments</i>. Cambridge University Press, 1993.<br /><br /></ul><div class="blogger-post-footer"><img width='1' height='1' src='https://blogger.googleusercontent.com/tracker/29764260-115499195604390911?l=healf.blogspot.com' alt='' /></div>hhghttp://www.blogger.com/profile/12671002162357946985noreply@blogger.com21