John Launchbury

John Launchbury

Contact

Chief Scientist
Office: 503.626.6616 x104
Email: john (at) galois (dot) com
LinkedIn: http://www.linkedin.com/pub/john-launchbury/10/a9a/1b1

At Galois

Dr. John Launchbury is Chief Scientist of Galois, Inc. John founded Galois in 1999 to address challenges in Information Assurance through the application of Functional Programming and Formal Methods. Under his leadership, formerly as CEO, the company has grown strongly, successfully winning and delivering on multiple contract awards for more than a decade. John continues to lead Galois' growing stature for its thought leadership in high assurance technology development.

My Background

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, and 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).

Publications

 

  • Launchbury, J. and Elliott, T. 2010. Concurrent orchestration in Haskell. In Proceedings of the Third ACM Haskell Symposium on Haskell (Baltimore, Maryland, USA, September 30 - 30, 2010). Haskell '10. ACM, New York, NY, 79-90.
  • David Burke, Joe Hurd, John Launchbury, and Aaron Tomb. Trust relationship modeling for software assurance. In Proceedings of the 7th International Workshop on Formal Aspects of Security & Trust (FAST 2010), September 2010.
  • 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.
  • Erkök, L. and Launchbury, J. 2002. A recursive do for Haskell. In Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell (Pittsburgh, Pennsylvania). Haskell '02. ACM, New York, NY, 29-37.
  • 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.
  • Erkök, L. and Launchbury, J. 2000. Recursive monadic bindings. In Proceedings of the Fifth ACM SIGPLAN international Conference on Functional Programming ICFP '00. ACM, New York, NY, 174-185.
  • Lewis, J. R., Launchbury, J., Meijer, E., and Shields, M. B. 2000. Implicit parameters: dynamic scoping with static types. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Boston, MA, USA, January 19 - 21, 2000). POPL '00. ACM, New York, NY, 108-118.
  • Cook, B., Launchbury, J., Mathews, J., and Kieburtz, R. B. 1999. Formal Verification of Explicitly Parallel Microprocessors. In Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (September 27 - 29, 1999). L. Pierre and T. Kropf, Eds. Springer-Verlag, London, 23-36.
  • Launchbury, J., Lewis, J. R., and Cook, B. 1999. On embedding a microarchitectural design language within Haskell. In Proceedings of the Fourth ACM SIGPLAN international Conference on Functional Programming (Paris, France, September 27 - 29, 1999). ICFP '99. ACM, New York, NY, 60-69.
  • Matthews, J. and Launchbury, J. 1999. Elementary Microarchitecture Algebra. In Proceedings of the 11th international Conference on Computer Aided Verification (July 06 - 10, 1999). N. Halbwachs and D. Peled, Eds. Springer-Verlag, London, 288-300.
  • Matthews, J., Cook, B., and Launchbury, J. 1998. Microprocessor Specification in Hawk. In Proceedings of the 1998 international Conference on Computer Languages (May 14 - 16, 1998). IEEE Computer Society, Washington, DC, 90.
  • Peyton Jones, S., Shields, M., Launchbury, J., and Tolmach, A. 1998. Bridging the gulf: a common intermediate language for ML and Haskell. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, California, United States, January 19 - 21, 1998). POPL '98. ACM, New York, NY, 49-61.
  • Cook, B. and Launchbury, J. 1997. Disposable memo functions (extended abstract). In Proceedings of the Second ACM SIGPLAN international Conference on Functional Programming (Amsterdam, The Netherlands, June 09 - 11, 1997). A. M. Berman, Ed. ICFP '97. ACM, New York, NY, 310.
  • Launchbury, J. and Sabry, A. 1997. Monadic state: axiomatization and type safety. In Proceedings of the Second ACM SIGPLAN international Conference on Functional Programming (Amsterdam, The Netherlands, June 09 - 11, 1997). A. M. Berman, Ed. ICFP '97. ACM, New York, NY, 227-238.
  • Launchbury, J. and Paterson, R. 1996. Parametricity and Unboxing with Unpointed Types. In Proceedings of the 6th European Symposium on Programming Languages and Systems (April 22 - 24, 1996). H. R. Nielson, Ed. Springer-Verlag, London, 204-218.
  • Launchbury, J. and Peyton Jones, S. L. 1995. State in Haskell. Lisp Symb. Comput. 8, 4 (Dec. 1995), 293-341.
  • Launchbury, J. and Sheard, T. 1995. Warm fusion: deriving build-catas from recursive definitions. In Proceedings of the Seventh international Conference on Functional Programming Languages and Computer Architecture (La Jolla, California, United States, June 26 - 28, 1995). FPCA '95. ACM, New York, NY, 314-323.
  • 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.
  • King, D. J. and Launchbury, J. 1995. Structuring depth-first search algorithms in Haskell. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, California, United States, January 23 - 25, 1995). POPL '95. ACM, New York, NY, 344-354.
  • Launchbury, J. and Peyton Jones, S. L. 1994. Lazy functional state threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (Orlando, Florida, United States, June 20 - 24, 1994). PLDI '94. ACM, New York, NY, 24-35.
  • Hughes, J. and Launchbury, J. 1994. Reversing abstract interpretations. In Selected Papers of the Symposium on Fourth European Symposium on Programming (Rennes, France). B. Krieg-Brückner and M. Sintzoff, Eds. Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 307-326.
  • Peyton Jones, S. L., Hughes, J., and Launchbury, J. 1993. How to give a good research talk. SIGPLAN Not. 28, 11 (Nov. 1993), 9-12.
  • Gill, A., Launchbury, J., and Peyton Jones, S. L. 1993. A short cut to deforestation. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (Copenhagen, Denmark, June 09 - 11, 1993). FPCA '93. ACM, New York, NY, 223-232.
  • Launchbury, J. 1993. A natural semantics for lazy evaluation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, South Carolina, United States). POPL '93. ACM, New York, NY, 144-154.
  • 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.
  • Hughes, J. and Launchbury, J. 1992. Reversing Abstract Interpretations. In Proceedings of the 4th European Symposium on Programming (February 26 - 28, 1992). B. Krieg-Brückner, Ed. Springer-Verlag, London, 269-286.
  • 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.
  • Peyton Jones, S. L. and Launchbury, J. 1991. Unboxed Values as First Class Citizens in a Non-Strict Functional Language. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture (August 26 - 30, 1991). J. Hughes, Ed. Springer-Verlag, London, 636-666.
  • Kubiak, R., Hughes, J., and Launchbury, J. 1992. Implementing Projection-based Strictness Analysis. In Proceedings of the 1991 Glasgow Workshop on Functional Programming (August 12 - 14, 1991). R. Heldal, C. K. Holst, and P. Wadler, Eds. Springer-Verlag, London, 207-224.
  • 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= http://doi.acm.org/10.1145/101620.101630
  • 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.
  • Frost, R. and Launchbury, J. 1989. Constructing natural language interpreters in a lazy functional language. Comput. J. 32, 2 (Apr. 1989), 108-121.