![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Tony Hoare, FRS FREng
Friday 04 May 2018, 14:00-15:00
Lecture 3: Logic for Program Development, Verification and Implementation.
- 👤 Speaker: Tony Hoare, FRS FREng
- 📅 Date & Time: Friday 04 May 2018, 14:00 - 15:00
- 📍 Venue: FW26
Abstract
Tony Hoare, FRS FR Eng, Hon Mem Cambridge University Computing Laboratory.
We start with a sufficient resume of previous lectures, so prior attendance at the lectures on Geometry and Algebra is not a requirement. Interested researchers may consult the lecture notes on my personal page of the Departmental Website.
We then derive from the algebra a set of logical rules of reasoning about concurrent programs. The derivation can be reversed: from the Rules to the Algebra.
We then give algebraic definitions of Milner/Plotkin transitions, and of Hoare/O’Hearn Triples, and by simple translation obtain the traditional rule of Operational Semantics and Verification Logic. They are simply duals of each other.
Series This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
Included in Lists
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- FW26
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- Martin's interesting talks
- School of Technology
- tcw57’s list
- Trust & Technology Initiative - interesting events
- yk373's list
- yk449
Note: Ex-directory lists are not shown.