|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
An Embedding of Abstract Separation Logic in HOL
If you have a question about this talk, please contact Thomas Tuerk.
Speaker: Thomas Tuerk
During my last ARG Lunch talk I presented work on formalising parts of Smallfoot inside HOL . Now I will present the continuation of this work: a formalisation abstract separation logic as introduced by Calcagno, O’Hearn and Yang. However, the main part of the talk will not consist of the HOL formalisation, but a presentation of abstract separation logic.
This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsBoris Lenhard seminar CARET Educational Technology Seminar Faraday Institute
Other talksReal wages and the household: Quantifying the economy of makeshifts of the poor in 18th-century England A Heisenberg Miscellany Regulation of membrane dynamics by phosphatidylinositol 3-phosphate What's happening to the world? Fiction and Reality of Mobility in Africa PLACE Book Launch