John Launchbury

Chief Scientist


John Launchbury is the Chief Scientist at Galois, collaborating with government and industry leaders to fundamentally improve the security of software and cyber-physical systems though applied formal mathematical techniques.

Prior to rejoining Galois in 2017, John was the Director of the Information Innovation Office (I2O) at DARPA, where he led nation-scale investments in cybersecurity and artificial intelligence.

Before founding Galois in 1999, Dr. Launchbury was a full professor in Computer Science, and he is internationally recognized for his work on the analysis and semantics of functional programming languages.

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.