[Prev][Next][Index][Thread]

Papers available: game semantics for lazy lambda calculus.


We wish to announce the availability of two papers concerning game
semantics for languages with recursive types. They are:

Games for Recursive Types

and

Games and Full Abstraction for the Lazy Lambda-Calculus

by Samson Abramsky and Guy McCusker.

Games for Recursive Types:

  We present results concerning the solution of recursive
  domain equations in the category G of games, previously used to
  construct a fully abstract model of PCF. Namely, we show how to
  construct solutions to equations of the form D = F(D,D) for a large
  class of functors F: G^{op} x G --> G  and verify that these
  solutions  satisfy Freyd's minimal invariant  property. 
  
  New constructions corresponding to lifting
  and separated sum for games are presented, and are used to generate
  games for two simple recursive types: the vertical and lazy natural
  numbers.

  To appear in proceedings of the Second Workshop of the Theory and
  Formal Methods Section, Department of Computing, Imperial College,
  1994.

Available by anonymous ftp from

theory.doc.ic.ac.uk:/papers/{Abramsky,McCusker}/g4rt.{dvi,ps}.gz 

or on the world wide web from

http://theory.doc.ic.ac.uk/~gam

or

http://theory.doc.ic.ac.uk/people/Abramsky

Games and Full Abstraction for the Lazy Lambda Calculus (extended abstract):

  We define a category of games G, and its extensional
  quotient E. A model of the lazy lambda-calculus, a type-free
  functional language based on evaluation to weak head normal form, is
  given in G, yielding an extensional model in E. This
  model is shown to be fully abstract with respect to applicative
  simulation. This is, so far as we know, the first purely semantic
  construction of a fully abstract model for a reflexively-typed 
  sequential language.

  To appear in proceedings of 10th annual IEEE symposium on Logic in
  Computer Science, 1995.

Available by anonymous ftp from

theory.doc.ic.ac.uk:/papers/{Abramsky,McCusker}/lics95.{dvi,ps}.gz 

or on the world wide web from

http://theory.doc.ic.ac.uk/~gam

or 

http://theory.doc.ic.ac.uk/people/Abramsky