Wednesday June 1 Seminar

• To: attend-types@THEORY.LCS.MIT.EDU
• Subject: Wednesday June 1 Seminar
• From: Bard Bloom <bard@THEORY.LCS.MIT.EDU>
• Date: Tue, 24 May 88 14:20:19 edt

  On Wednesday, June 1, at 1:00, in the third floor conference room, Jon
Riecke and Bard Bloom will present Luke Ong's recent work on "Fully Abstract
Models of the Lazy Lambda Calculus."
  This is a semantic theory considering termination as the essential
observable, in an interpreter that (quite reasonably) stops at terms that
begin with lambdas.  So, the interpreter diverges on Omega, but stops
immediately on (\x.Omega).  Many familiar models identify these terms.  
  This distinction can be made repeatedly; for example, \x\y.Omega and
\x.Omega can be distinguished by applying each of them to something.  Ong
defines "applicative bisimulation", which captures this idea precisely.  He
gives a model, proof system, and so forth that make all the appropriate
distinctions.

  -- Bard the \x.gargoyle

• Prev: Re: typing in ML+
• Next: [sieber: denotational versus operational semantics]
• Index(es):
  • Main
  • Thread