[Fwd: [Church-announce] Church Seminar this Thursday [with Abstract]]

dvanhorn <[email protected]>
Newsgroups gmane.org.ballistichelmet.lambda
Message-ID <[email protected]>

-------- Original Message --------
Subject: [Church-announce] Church Seminar this Thursday [with Abstract]
Date: Wed, 18 Feb 2004 12:50:26 -0500
From: Mark A. Sheldon <sheldon-TThHoi1dxff2fBVCVOL8/[email protected]>
Reply-To: church-active-TThHoi1dxff2fBVCVOL8/[email protected]
Organization: Boston University Computer Science Department
To: church-announce-TThHoi1dxff2fBVCVOL8/[email protected]
CC: sheldon-TThHoi1dxff2fBVCVOL8/[email protected]

The previous announcement went out without Joe's abstract.  To further
entice you to come, here is a more detailed announcement:

When:    Thursday 19 February 2004, 2:30--4:30pm
Where:   Boston University, Room MCS 180
          111 Cummington Street, Boston
Speaker: Joe Wells, Heriot-Watt University
Title:   A Brief Tutorial on Expansion in Intersection Types

ABSTRACT:

     The operation of <em>expansion</em> on typings was introduced at
     the end of the 1970s by Coppo, Dezani, and Venneri for reasoning
     about the possible typings of a term with intersection types.
     Since then, it has remained somewhat mysterious and unfamiliar,
     even though it is essential for carrying out compositional type
     inference.  The fundamental idea of expansion is to be able to
     calculate the effect on the final judgement of a typing derivation
     of inserting a use of the intersection introduction rule at some
     (possibly deeply nested) position, without actually needing to
     build the new derivation.  Recently, we have improved on this by
     introducing <em>expansion variables</em> (E-variables), which make
     the calculation straightforward and understandable.  E-variables
     make it easy to postpone choices of which typing rules to use
     until later constraint solving gives enough information to allow
     making a good choice.  We can also now do expansion for other type
     constructors such as the ! of Linear Logic.


--
Mark A. Sheldon
Boston University Computer Science Department
sheldon-TThHoi1dxff2fBVCVOL8/[email protected]
617-358-1141
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.