As a lecturer at the University of Glasgow, Launchbury focused his early research on the semantics and analysis of lazy functional languages and was one of the contributing designers of the
Haskell programming language. In 1993, Launchbury provided a formal description of lazy evaluation, addressing challenges in analyzing a program’s storage requirements. The operational semantics is widely cited in later research on Haskell. In the context of the Glasgow Haskell Compiler team, Launchbury established an effective partnership with
Simon L. Peyton Jones to write a number of papers that dramatically influenced the design of Haskell. Their 1995 paper on State in Haskell introduced the “IO
monad” as a mathematically-clean practical way of expressing effects on the external world, and solidified the “
do-notation” Launchbury had introduced earlier. Their papers on unboxed values and removal of intermediate data structures addressed many of the efficiency challenges inherent in lazy evaluation. In 1994, Launchbury relocated to the West Coast of the United States, becoming a full professor at the
Oregon Graduate Institute in 2000. His research there addressed the creation and optimization of
domain-specific programming languages (DSLs) ranging from fundamental research in combining disparate semantic elements, through embedding DSLs in Haskell, to applied research for modeling and reasoning about
very-large scale integration (VLSI) micro-architectures. Launchbury founded Galois Inc. in 1999 to address challenges in information assurance through the application of functional programming and formal methods. He served as the company’s CEO and Chief Scientist from 2000 to 2014. Under Launchbury’s direction, Galois Inc. developed the
Cryptol domain-specific language for specifying and verifying cryptographic implementations. Originally designed for use by the
National Security Agency, the language was made available to the public in 2008. Launchbury is the holder of two patents on cryptographic structures in data storage and one on effective mechanisms for configuring programmable cryptographic components. In 2014, Launchbury joined DARPA, initially as a program manager, and then as director of the
Information Innovation Office (I2O) in 2015. While at DARPA, Launchbury led programs in
homomorphic cryptography (PROCEED), cybersecurity for vehicles and other
embedded systems (HACMS), and
data privacy (Brandeis). He also defined and described the "Three Waves of AI": Handcrafted Knowledge, Statistical Learning, and Contextual Adaptation. In 2017, Launchbury rejoined Galois as Chief Scientist. == Other publications==