Lecture Leslie Lamport (Microsoft Corporation)

Title: The PlusCal Algorithm Language Leslie Lamport made various fundamental contributions to distributed systems, fault-tolerant computing, cryptography, and program verification. He also created the LaTeX system.  For his research Lamport received numerous awards including the IEEE John von Neumann Medal. Everybody is welcome to attend this lecture.
  • Lecture Leslie Lamport (Microsoft Corporation)
  • 2011-06-16T14:00:00+02:00
  • 2011-06-16T15:00:00+02:00
  • Title: The PlusCal Algorithm Language Leslie Lamport made various fundamental contributions to distributed systems, fault-tolerant computing, cryptography, and program verification. He also created the LaTeX system.  For his research Lamport received numerous awards including the IEEE John von Neumann Medal. Everybody is welcome to attend this lecture.
  • When 16-06-2011 from 14:00 to 15:00 (Europe/Amsterdam / UTC200)
  • Where Turing room
  • Add event to calendar iCal

Title: The PlusCal Algorithm Language

Leslie Lamport made various fundamental contributions to distributed systems, fault-tolerant computing, cryptography, and program verification. He also created the LaTeX system.  For his research Lamport received numerous awards including the IEEE John von Neumann Medal.

Everybody is welcome to attend this lecture.

Abstract:  

Algorithms are different from programs and should not be described  with programming languages.  For example, algorithms are usually best  described in terms of mathematical objects like sets and graphs  instead of the primitive objects like bytes and integers provided by  programming languages.  Until now, the only simple alternative to  programming languages has been pseudo-code.  PlusCal is an algorithm language based on TLA+.  A PlusCal algorithm  is automatically translated to a TLA+ specification that can be  checked with the TLC model checker or reasoned about formally.  (No knowledge of TLA+ is assumed.)   PlusCal makes pseudo-code obsolete.