Biography:John Launchbury
Dr. John Launchbury | |
|---|---|
 | |
| Nationality | British, American |
| Alma mater | Oxford University, University of Glasgow |
| Known for | Functional Programming Languages |
| Scientific career | |
| Fields | Cybersecurity, Data Analysis, Artificial Intelligence |
| Institutions | Oregon Graduate Institute School of Science and Engineering, Galois Inc., DARPA |
| Thesis | Projection Factorizations in Partial Evaluation |
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, data analysis, and artificial intelligence. 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.[1]
Education
Launchbury received first-class honors in mathematics from Oxford University in 1985, and an M.Sc. in computation in 1986. He holds a Ph.D. in computing science from the University of Glasgow. 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.[2]
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.
In 1993, Launchbury provided a formal description of lazy evaluation, addressing challenges in analyzing a program’s storage requirements.[3] The operational semantics is widely cited in later research on Haskell. In the context of the Glasgow Haskell Compiler team,[4] 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[5] 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.[6] Their papers on unboxed values[7] and removal of intermediate data structures[8] 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.[9] [10] 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.[11]
Launchbury is the holder of two patents on cryptographic structures in data storage and one on effective mechanisms for configuring programmable cryptographic components.[12]
In 2014, Launchbury joined DARPA, initially as a program manager,[13] and then as director of the Information Innovation Office (I2O) in 2015.[9] [14] 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.[15] [16]
In 2017, Launchbury rejoined Galois as Chief Scientist.[17]
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.[18]
References
- ↑ "ACM Fellows". Association for Computing Machinery. http://awards.acm.org/award_winners/launchbury_4652509.cfm.
- ↑ Launchbury, John (1991). Projection Factorizations in Partial Evaluation. New York, NY, USA: Cambridge University Press. pp. 163. ISBN 978-0-521-41497-5. http://dl.acm.org/citation.cfm?id=129094&CFID=890726098&CFTOKEN=83528104.
- ↑ Launchbury, John (1993). "A Natural Semantics for Lazy Evaluation". Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '93. ACM. pp. 144–154. doi:10.1145/158511.158618. ISBN 0897915607.
- ↑ "The Glasgow Haskell Team: Other Wonderful Past Contributors". https://ghc.haskell.org/trac/ghc/wiki/TeamGHC#Otherwonderfulpastcontributors.
- ↑ Launchbury, John; Jones, Simon L Peyton (December 1, 1995). State in Haskell. Boston, MA: Kluwer Academic Publishers. pp. 51. http://research-srv.microsoft.com/en-us/um/people/simonpj/papers/state-lasc.pdf.
- ↑ Launchbury, John (1993). Lazy Imperative Programming. Yale University. pp. 46–56. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5271. Retrieved 19 January 2017.
- ↑ Simon L Peyton Jones; John Launchbury (1991). Unboxed values as first class citizens in a non-strict functional language. New York, NY, USA: Springer-Verlag New York, Inc.. pp. 145–164. ISBN 978-0-387-54396-3. http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.231.
- ↑ Andrew Gill; John Launchbury; Simon L Peyton Jones (June 1993). A short cut to deforestation. Copenhagen, Denmark: Conference FPCA '93 Conference on Functional Programming Languages & Computer Architecture. http://research.microsoft.com/en-us/um/people/simonpj/Papers/deforestation-short-cut.pdf.
- ↑ 9.0 9.1 "Dr. John Launchbury". DARPA. http://www.darpa.mil/staff/dr-john-launchbury.
- ↑ McKinney, Laura (2011). "Statement by Laura McKinney, CEO, Galois, Inc. Prepared for the hearing on Small Business and Job Creation: The SBIR and STTR programs". https://republicans-science.house.gov/_cache/files/b/b/bb0ee6eb-03a7-4eed-9573-e68eb129c607/BF40A23E8FB27EC168330F266025F71E.mckinney-final-written-testimony-2-.pdf.
- ↑ "Cryptol, the language of cryptography, now available". December 24, 2008. http://galois.com/blog/2008/12/cryptol-the-language-of-cryptography-now-available/.
- ↑ "Patents by Inventor John Launchbury". http://patents.justia.com/inventor/john-launchbury.
- ↑ Spencer, Malia (2014). "Defense department taps Portland security expert to help make computer systems safer". https://www.bizjournals.com/portland/blog/2014/06/defense-research-taps-portland-security-expert-to.html.
- ↑ Metz, Cade. "Will Humans or Bots Rule Cybersecurity? The Answer Is Yes" (in en-US). Wired. ISSN 1059-1028. https://www.wired.com/2016/08/will-humans-bots-rule-cybersecurity-answer-yes/. Retrieved 2023-08-30.
- ↑ "Understanding the limits of deep learning" (in en-US). 2017-04-03. https://venturebeat.com/ai/understanding-the-limits-of-deep-learning/.
- ↑ "An excellent talk from DARPA on the three waves of Artificial Intelligence (AI) – The Contextual Adaptation is the right direction to go: Explainable AI" (in en-GB). https://blogs.cardiff.ac.uk/ai-robotics/an-excellent-talk-on-the-three-waves-of-artificial-intelligence-ai-the-contextual-adaptation-is-a-way-to-go-explainable-ai/.
- ↑ "New Dayton cyber-security firm celebrating new home" (in English). https://www.daytondailynews.com/business/new-dayton-cyber-security-firm-have-open-house/GOc271DKH0YcmoixbZd7zJ/.
- ↑ John Launchbury (August 1, 2009). Change Us, Not God. WCF Publishing. pp. 200. ISBN 978-0982409299. https://books.google.com/books?id=KeYvQAAACAAJ.
 |  |
