Peter William O'Hearn (born 13 July 1963 in Halifax, Nova Scotia), formerly a research scientist at Meta, [15] is a Distinguished Engineer at Lacework [16] and a Professor of Computer science at University College London (UCL). [17] He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases. [13]
O'Hearn attained a BSc degree in computer science from Dalhousie University, Halifax, Nova Scotia (1985), followed by MSc (1987) and PhD (1991) degrees from Queen's University, Kingston, Ontario, Canada. His dissertation was on Semantics of Non-interference: A natural approach, supervised by Robert D. Tennent. [14] [18]
O'Hearn is best known for separation logic, [1] a theory he developed with John C. Reynolds that unearthed new domains for scaling logical reasoning about code. This built on prior research from O'Hearn and David Pym on logic for resources, termed bunched logic. [2] With Stephen Brookes, Carnegie Mellon University, O'Hearn created Concurrent Separation Logic (CSL), extending the theory further. Tony Hoare, in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation". [19]
He conducted a study of programming languages which were similar to ALGOL, with his former doctoral advisor Robert D. Tennent, which became the book Algol-Like Languages. [20]
Separation logic has given rise to the Infer Static Analyzer (Facebook Infer), a static program analysis utility developed by O'Hearn's team at Facebook. [3] After 20 plus years in academia, O'Hearn began working at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded. [21] Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production. [22] It was open sourced in 2016, and is used by Amazon Inc, Spotify, Mozilla, Uber, and others. [3] In 2017, O'Hearn and the team open sourced RacerD, an automated static race condition detection tool that reduces the time it takes to flag potential problems in concurrent software, as part of the Infer platform. [23]
O'Hearn was an assistant professor at Syracuse University, New York, United States, from 1990 to 1995. He was a reader in computer science at Queen Mary University of London from 1996 to 1999 and then a full professor at Queen Mary until his move to University College London. At UCL he was granted a chair sponsored by the Royal Academy of Engineering and Microsoft Research. [24] In 1997 he was a visiting scientist at Carnegie Mellon University and in 2006 he was a visiting researcher at Microsoft Research Cambridge. [18] He now shares his time working as a Distinguished Engineer at Lacework and a professor at UCL. [16]
In 2007, O'Hearn was granted a Royal Society Wolfson Research Merit Award. [8] In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award. [12] With Stephen Brookes, Carnegie Mellon University, he was co-recipient of the 2016 Gödel Prize, for the invention of Concurrent Separation Logic. [9] Also in 2016, he was elected Fellow of the Royal Academy of Engineering (FREng) and co-received the annual CAV (Computer Aided Verification) award. [10] [11] In 2018, he was elected Fellow of the Royal Society (FRS), and was bestowed with an Honorary Doctor of Laws from Dalhousie University. [7] [8] [6] January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues. [5] The Institute of Electrical and Electronics Engineers (IEEE) granted O'Hearn and three of his Facebook colleagues an IEEE Cybersecurity Award for Practice at their annual awards ceremony in October, 2021. [4]
ALGOL is a family of imperative computer programming languages originally developed in 1958. ALGOL heavily influenced many other languages and was the standard method for algorithm description used by the Association for Computing Machinery (ACM) in textbooks and academic sources for more than thirty years.
Sir Charles Antony Richard Hoare, also known as Tony Hoare or by his initials C. A. R. Hoare is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and concurrent computing. His work earned him the Turing Award, usually regarded as the highest distinction in computer science, in 1980.
Samson Abramsky is a British computer scientist who is a Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 to 2021.
Bunched logic is a variety of substructural logic proposed by Peter O'Hearn and David Pym. Bunched logic provides primitives for reasoning about resource composition, which aid in the compositional analysis of computer and other systems. It has category-theoretic and truth-functional semantics, which can be understood in terms of an abstract concept of resource, and a proof theory in which the contexts Γ in an entailment judgement Γ ⊢ A are tree-like structures (bunches) rather than lists or (multi)sets as in most proof calculi. Bunched logic has an associated type theory, and its first application was in providing a way to control the aliasing and other forms of interference in imperative programs. The logic has seen further applications in program verification, where it is the basis of the assertion language of separation logic, and in systems modelling, where it provides a way to decompose the resources used by components of a system.
Benjamin Crawford Pierce is the Henry Salvatori Professor of computer science at the University of Pennsylvania. Pierce joined Penn in 1998 from Indiana University and held research positions at the University of Cambridge and the University of Edinburgh. He received his Ph.D. from Carnegie Mellon University in 1991. His research includes work on programming languages, static type systems, distributed programming, mobile agents, process calculi, and differential privacy.
John Charles Reynolds was an American computer scientist.
Philip Lee Wadler is a UK-based American computer scientist known for his contributions to programming language design and type theory. He is holds the position of Personal Chair of theoretical computer science at the Laboratory for Foundations of Computer Science at the School of Informatics, University of Edinburgh. He has contributed to the theory behind functional programming and the use of monads; and the designs of the purely functional language Haskell and the XQuery declarative query language. In 1984, he created the Orwell language. Wadler was involved in adding generic types to Java 5.0. He is also author of "Theorems for free!", a paper that gave rise to much research on functional language optimization.
Robert William Harper, Jr. is a computer science professor at Carnegie Mellon University who works in programming language research. Prior to his position at Carnegie Mellon, Harper was a research fellow at the University of Edinburgh.
Peter Thomas Kirstein was a British computer scientist who played a role in the creation of the Internet. He made the first internetworking connection on the ARPANET in 1973, by providing a link to British academic networks, and was instrumental in defining and implementing TCP/IP alongside Vint Cerf and Bob Kahn.
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.
In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI). A CACM review article by O'Hearn charts developments in the subject to early 2019.
Randal E. Bryant is an American computer scientist and academic noted for his research on formally verifying digital hardware and software. Bryant has been a faculty member at Carnegie Mellon University since 1984. He served as the Dean of the School of Computer Science (SCS) at Carnegie Mellon from 2004 to 2014. Dr. Bryant retired and became a Founders University Professor Emeritus on June 30, 2020.
Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.
Jonathan Andrew Crowcroft is the Marconi Professor of Communications Systems in the Department of Computer Science and Technology, University of Cambridge, a visiting professor at the Department of Computing at Imperial College London, and the chair of the programme committee at the Alan Turing Institute.
Mark James Handley is Professor of Networked Systems in the Department of Computer Science of University College London since 2003, where he leads the Networks Research Group.
George Ciprian Necula is a Romanian computer scientist, engineer at Google, and former professor at the University of California, Berkeley who does research in the area of programming languages and software engineering, with a particular focus on software verification and formal methods. He is best known for his Ph.D. thesis work first describing proof-carrying code, a work that received the 2007 SIGPLAN Most Influential POPL Paper Award.
Infer, sometimes referred to as "Facebook Infer", is a static code analysis tool developed by an engineering team at Facebook along with open-source contributors. It provides support for Java, C, C++, and Objective-C, and is deployed at Facebook in the analysis of its Android and iOS apps.
Jade Alglave is a French computer scientist whose research involves concurrency control, consistency models, weak hardware memory models, the relation between computer hardware and programming languages, and the "cat" domain-specific language for consistency models. She is a professor of computer science at University College London and a distinguished engineer at British semiconductor firm Arm.
“All text published under the heading 'Biography' on Fellow profile pages is available under Creative Commons Attribution 4.0 International License.” -- "Terms, conditions and policies | Royal Society". Archived from the original on 11 November 2016. Retrieved 7 June 2018.{{cite web}}: CS1 maint: bot: original URL status unknown (link)
Media related to Peter O'Hearn at Wikimedia Commons 
This article incorporates text available under the CC BY 4.0 license.
| International | |
|---|---|
| National | |
| Academics | |
| Other | |
