DocumentCode
728957
Title
From Categorical Logic to Facebook Engineering
Author
O´Hearn, Peter
Author_Institution
Univ. Coll. London, London, UK
fYear
2015
fDate
6-10 July 2015
Firstpage
17
Lastpage
20
Abstract
I chart a line of development from category-theoretic models of programs and logics to automatic program verification/analysis techniques that are in deployment at Facebook. Our journey takes in a number of concepts from the computer science logician´s toolkit -- including categorical logic and model theory, denotational semantics, the Curry-Howard isomorphism, sub structural logic, Hoare Logic and Separation Logic, abstract interpretation, compositional program analysis, the frame problem, and abductive inference.
Keywords
category theory; formal logic; inference mechanisms; program diagnostics; program verification; Curry-Howard isomorphism; Facebook engineering; Hoare logic; abductive inference; abstract interpretation; automatic program verification/analysis technique; categorical logic; category-theoretic model; compositional program analysis; denotational semantics; model theory; separation logic; substructural logic; Cognition; Computer science; Facebook; Mathematical model; Semantics; Shape; Syntactics;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on
Conference_Location
Kyoto
ISSN
1043-6871
Type
conf
DOI
10.1109/LICS.2015.11
Filename
7174865
Link To Document