John Launchbury


I founded Galois in 1999 to address challenges in building trustworthy systems through the application of the science of computing, particularly through formal methods. I am currently pursuing the same agenda as a program manager at DARPA via an IPA from Willamette University.


John has variously served the company as CEO, Chief Scientist, and Chair of the Board of Directors. Under his leadership, the company has grown, successfully winning and delivering on multiple contract awards, and advanced in intellectual and engineering stature.

Prior to founding Galois, John was a full professor in Computer Science and Engineering at the Oregon Graduate Institute School of Science and Engineering at OHSU. His instruction style earned him several awards for outstanding teaching, and he is internationally recognized for his work on the analysis and semantics of programming languages,  on the Haskell programming language in particular.

John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society’s distinguished dissertation prize. In 2010, John was inducted as a Fellow of the Association for Computing Machinery (ACM).

Other Publications

  • Launchbury, J. 2009. Functional Programming As A Means, Not An End. In Proceedings of the 2009 Video Workshop on Commercial Users of Functional Programming: Functional Programming As A Means, Not An End (Edinburgh, Scotland, September 04 – 04, 2009). CUFP ’09. ACM, New York, NY, 1.
  • Launchbury, J. 2008. Industrial functional programming. In Proceedings of the 10th international Conference on Practical Aspects of Declarative Languages (San Francisco, CA, USA, January 07 – 08, 2008). P. Hudak and D. S. Warren, Eds. Springer-Verlag, Berlin, Heidelberg, 1-1.
  • Launchbury, J. 2007. Cross-domain WebDAV server. In Proceedings of the 4th ACM SIGPLAN Workshop on Commercial Users of Functional Programming (Freiburg, Germany, October 04 – 04, 2007). CUFP ’07. ACM, New York, NY, 1-2.
  • Launchbury, J. 2004. Galois: high assurance software. In Proceedings of the Ninth ACM SIGPLAN international Conference on Functional Programming (Snow Bird, UT, USA, September 19 – 21, 2004). ICFP ’04. ACM, New York, NY, 3-3.
  • Devanbu, P., Balzer, B., Batory, D., Kiczales, G., Launchbury, J., Parnas, D., and Tarr, P. 2003. Modularity in the new millenium: a panel summary. In Proceedings of the 25th international Conference on Software Engineering (Portland, Oregon, May 03 – 10, 2003). IEEE Computer Society, Washington, DC, 723-724.
  • Krstic, S., Launchbury, J., and Pavlovic, D. 2001. Categories of Processes Enriched in Final Coalgebras. In Proceedings of the 4th international Conference on Foundations of Software Science and Computation Structures (April 02 – 06, 2001). F. Honsell and M. Miculan, Eds. Springer-Verlag, London, 303-317.
  • Launchbury, J. 1995. Graph Algorithms with a Functional Flavous. In Advanced Functional Programming, First international Spring School on Advanced Functional Programming Techniques-Tutorial Text (May 24 – 30, 1995). J. Jeuring and E. Meijer, Eds. Springer-Verlag, London, 308-331.
  • Launchbury, J., Gill, A., Hughes, J., Marlow, S., Peyton Jones, S. L., and Wadler, P. 1993. Avoiding Unnecessary Updates. In Proceedings of the 1992 Glasgow Workshop on Functional Programming (July 06 – 08, 1992). J. Launchbury and P. M. Sansom, Eds. Springer-Verlag, London, 144-153.
  • Launchbury, J. 1991. A Strongly-Typed Self-Applicable Partial Evaluator. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture (August 26 – 30, 1991). J. Hughes, Ed. Springer-Verlag, London, 145-164.
  • Launchbury, J. 1991. Strictness and binding-time analyses: two for the price of one. In Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation (Toronto, Ontario, Canada, June 24 – 28, 1991). PLDI ’91. ACM, New York, NY, 80-91.
  • Launchbury, J. 1991 Projection Factorisations in Partial Evaluation. Cambridge University Press.
  • Argo, G., Hughes, J., Trinder, P., Fairbairn, J., and Launchbury, J. 1990. Implementing functional databases. In Advances in Database Programming Languages, F. Bancilhon and P. Buneman, Eds. ACM, New York, NY, 165-176. DOI=
  • Launchbury, J. 1990. Dependent Sums Express Separation of Binding Times. In Proceedings of the 1989 Glasgow Workshop on Functional Programming (August 21 – 23, 1989). K. Davis and J. Hughes, Eds. Springer-Verlag, London, 238-253.