IMPORTANT NOTE!: This is a mirror of Lamport's TLA+ lecture videos with some chapter markers in the video description from Lamport's site for ease of viewing on mobile devices, or other platforms and connection setups where KZfaq is the most optimal "format". For the original files, resources, errata, and more, please visit lamport.azurewebsites.net/vide... or the original page which is linked below.
Original Description: A two-part lecture that explains the general meaning of implementation, which involves refinement mappings.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:04 - Prologue
00:44 - Recursive Definitions
03:44 - Substitution
09:19 - The AB2 Protocol
14:14 - Checking AB2
16:43 - Liveness of AB2
19:20 - Epilogue