John Launchbury is an American and British computer scientist who is currently Chief Scientist at Galois, Inc. Previously, he directed one of DARPA’s technical offices, where he oversaw nation-scale scientific and engineering research in

cybersecurity Computer security, cybersecurity (cyber security), or information technology security (IT security) is the protection of computer systems and networks from attack by malicious actors that may result in unauthorized information disclosure, the ...

, data analysis, and

artificial intelligence Artificial intelligence (AI) is intelligence—perceiving, synthesizing, and inferring information—demonstrated by machines, as opposed to intelligence displayed by animals and humans. Example tasks in which this is done include speech re ...

. He is known for research and entrepreneurship in the implementation and application of functional programming languages. In 2010, Launchbury was inducted as a Fellow of the

Association for Computing Machinery The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional member ...

Education

Launchbury received first-class honors in mathematics from

Oxford University Oxford () is a city in England. It is the county town and only city of Oxfordshire. In 2020, its population was estimated at 151,584. It is north-west of London, south-east of Birmingham and north-east of Bristol. The city is home to the ...

in 1985, and an M.Sc. in computation in 1986. He holds a Ph.D. in computing science from the

University of Glasgow , image = UofG Coat of Arms.png , image_size = 150px , caption = Coat of arms Flag , latin_name = Universitas Glasguensis , motto = la, Via, Veritas, Vita , ...

. In 1991, the Cambridge University Press published his thesis, ''Projection Factorizations in Partial Evaluation'', after it won the British Computer Society's distinguished dissertation prize.

Career and research

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 Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...

. 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 Monad may refer to: Philosophy * Monad (philosophy), a term meaning "unit" **Monism, the concept of "one essence" in the metaphysical and theological theory ** Monad (Gnosticism), the most primal aspect of God in Gnosticism * ''Great Monad'', an ...

” 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 The Oregon Graduate Center was a unique, private, postgraduate-only research university in Washington County, Oregon, on the west side of Portland, from 1963 to 2001. The center was renamed the Oregon Graduate Institute in 1989. The Institute m ...

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 Cryptol is a domain-specific programming language for cryptography developed by the Portland, Oregon based software development firm, Galois, Inc. The language was originally developed for use by the United States National Security Agency. The lang ...

domain-specific language for specifying and verifying cryptographic implementations. Originally designed for use by the

National Security Agency The National Security Agency (NSA) is a national-level intelligence agency of the United States Department of Defense, under the authority of the Director of National Intelligence (DNI). The NSA is responsible for global monitoring, collecti ...

, 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. Launchbury led programs in homomorphic cryptography
PROCEED
, cybersecurity for vehicles and other

embedded systems An embedded system is a computer system—a combination of a computer processor, computer memory, and input/output peripheral devices—that has a dedicated function within a larger mechanical or electronic system. It is ''embedded'' as ...

HACMS
, and

data privacy Information privacy is the relationship between the collection and dissemination of data, technology, the public expectation of privacy, contextual information norms, and the legal and political issues surrounding them. It is also known as data pr ...

Brandeis
. In 2017, Launchbury rejoined Galois as Chief Scientist.

Other publications

Launchbury published a theological perspective on the Moral Exemplar interpretation of the doctrine of atonement, entitled ''Change Us, Not God: Biblical Meditations on the Death of Jesus''.

References

{{DEFAULTSORT:Launchbury, John British emigrants to the United States Alumni of the University of Oxford Alumni of the University of Glasgow Oregon Graduate Institute people Fellows of the Association for Computing Machinery Programming language researchers Living people Year of birth missing (living people) Place of birth missing (living people)