With great commitment
from the below speakers, we are very excited to launch “Dr. TLA+ Series”.
Dr. TLA+ Series: learn an algorithm and protocol, study a
specification
Each one-hour session will focus on a single algorithm and
protocol, presented by a single speaker. The speaker will:
-- dive deep into how the algorithm and protocol works
-- illustrate in detail how the TLA+ specification is
written
-- share the learnings from writing/studying the TLA+
specification
Format: Sessions will be presented through live streaming
(with remote questioning) and open to anyone who is interested. The announcements
will be made in the TLA+ Google
group. All sessions will be recorded and made available online.
Audience: the series are for people who already know how to
write at least simple TLA+ specs. Rather than how to get started, the series
focus on learning new algorithms/protocols and techniques to write better
specifications.
Schedule: Details will be available soon. The below are the current
topics/speakers.
Time |
Topic |
Speaker |
June |
Paxos |
Andrew Helwer (Microsoft) |
July |
Raft |
Jin Li (Microsoft) |
July |
Logical Physical Clocks |
Prof. Murat Demirbas (U. of Buffalo, SUNY) |
August |
Fast Paxos |
Cheng Huang (Microsoft) |
TBD |
Serializable Snapshot Isolation |
Chris Newcombe (Oracle) |
Speaker:
This is a community effort. Everyone is welcome to volunteer as a speaker. Speakers
get to choose (or ask recommendation from us) which algorithm/protocol/specification
to present.
Stay
tuned …