"The PlusCal Algorithm Language"

W.T.Young Library Auditorium [info]

Leslie Lamport
Researcher, Microsoft Corporation


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.


Biography:

Dr. Lamport received a doctorate in mathematics from Brandeis University, with a dissertation on singularities in analytic partial differential equations. This, together with a complete lack of education in computer science, prepared him for a career as a computer scientist at Massachusetts Computer Associates, SRI, Digital, and Compaq. He claims that it is through no fault of his that of those four corporations, only the one that was supposed to be non-profit still exists. He joined Microsoft in 2001, but that company has not yet succumbed.

Dr. Lamport's initial research in concurrent algorithms made him well-known as the author of LaTeX, a document formatting system for the ever-diminishing class of people who write formulas instead of drawing pictures. He is also known for writing

"A distributed system is one in which the failure of a computer you didn't even know existed can render your own computer unusable"

which established him as an expert on distributed systems. Among his other contributions is the TLA+ specification language, which represents a Quixotic attempt to overcome computer scientists' antipathy towards mathematics.

Despite having received five honorary doctorates from European universities, having been sent by the IEEE to Italy to receive the 2004 Piore Award, and being required to go to Quebec to receive its 2008 von Neumann medal, Dr. Lamport has not taken the hint and continues to return to his home in California.

Host: Professor Ken Calvert