announcement for Bohm's thm workshop

	     Workshop on Bohm's theorem: applications to
		       Computer Science Theory

		     July 13, 2001, Crete, Greece


Bohm's theorem is central to the study of the untyped lambda
calculus. It shows that disctinct normal forms, up to eta conversion,
cannot be identified in any consistent model of the lambda
calculus. This first separability result has been generalised to non
normal forms and is the underlying concept for the introduction of
finite or infinite trees of head normal forms, also known as Bohm

In the semantics of programming languages, Bohm's theorem corresponds
to the notion of full abstraction in models, and gave the initial
hints towards the construction of models for sequentials languages; in
the theory of concurrency, it is the notion of observability and is
used for building bisimulations; in the semantics of security, it
gives a strong meaning to the notion of safe computations.

Thirty years later, on the occasion of Corrado Bohm's EATCS
Distinguished Service Award, this workshop attempts to provide a
synthetic view as well as the most recent works on Bohm trees,
sequentiality and game semantics, logic, security, fully abstract
translations, action calculi, abstract rewriting systems, based on the
very preliminary work of Bohm.

Papers will appear in the ENTCS (electronic notes of Elsevier) with a
printed version to be distributed to the participants on site.


Henk Barendregt (Univ. of Nijmegen)
Mariangiola Dezani (Univ. of Torino)

Program Committee

Pierre-Louis Curien (CNRS, Univ. of Paris 7) 
Jan-Willem Klop (Free University, Amsterdam)
Gerard Huet (INRIA, France)
Jean-Jacques Levy (INRIA, France, chair)
Harry Mairson (Boston University)
Gordon Plotkin (Univ. of Edinburgh)
Simona Ronchi (Univ. of Torino)


Submission of Papers       : April 9, 2001
Notification of Acceptance : April 27, 2001
Final Version due          :   May 15, 2001

Home page of the workshop: 
Home page of ICALP'01: