Re: Semantics of Intersection Type

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

Hongseok Yang wrote:

>[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>Would anyone point out the literature on the semantics of 
>intersection types? 
>  
>

as far as I can see, the answers you got on the TYPES list all interpret 
your question as "what is the use of intersection types in semantics?" 
And the obvious answer is that they provide, by means of the "filter 
models", a concrete presentation of some well-know domains for 
interpreting lambda-calculi, where the types determine the compact 
elements (I myself wrote a paper on this topic, published in Information 
and Computation, Vol. 108, No. 1, 1994).

But one could understand your question in another way, namely : "what 
can be a semantical interpretation of (intersection) types". Then an 
obvious answer is: a set of expressions of some calculus (the 
"realizability" interpretation of types), or more generally a set of 
elements in some model of the calculus. Generalizing this to predicates 
indexed by types, one gets the notion of a "logical relation".  Some 
good references from this point of view are Krivine's book on 
"Lambda-Calculus, Types and Models" (Ellis Horwood, 1993), Mitchell's  
"Foundations for Programming Languages" (MIT Press, 1996), and Amadio 
and Curien's "Domains and Lambda-Calculi" (Cambridge University Press, 
1998), which also contains a chapter on filter models.

Re: Semantics of Intersection Type

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

>
> Interestingly, combining these two viewpoints on types is most  
> fruitful,
> in establishing for instance full abstraction results, like the
> classical one by Wadsworth regarding Scott's interpretation of the  
> pure
> lambda-calculus. A nice presentation of this is in Ronchi's lectures
> notes on "Basic Lambda Calculus" (1998? I don't know whether these  
> notes
> have been published).
>

The book "The Parametric Lambda Calculus", by Luca Paolini and myself
(texts in Theoretical Computer Science, Springer 2004) is partially  
based on these
notes.
A chapter in the book is dedicated to the interpretation of  
intersection types
as compact elements of Scott's models, and moreover some construction
of filter models is shown.

Best regards
Simona Ronchi

[Fwd: Re: Semantics of Intersection Type]

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

I am resending this message that was accidentally blocked by the types 
mailing list.

Adriana

Positions in IT Security at Siemens Corporate Technology, Munich, Germany

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

For extending our IT security applications & methods team,
we are currently seeking candidates for applied research and consulting
in areas including evaluation & certification of system security, and
analysis & design for Web service security and related areas.

Candidates should be available ideally at the beginning of 2006 or soon
thereafter. Particularly important requirements are strong analytic
abilities and the flexibility and readiness to adapt to new topics.
Familiarity with IT security, modelling (for instance in UML), and/or
formal methods, is desirable. Moreover, at least basic knowledge of
German would be very helpful, although our team has already become
rather international.

In case you are interested, please contact me and/or Dr. Jorge Cuellar
(Jorge.Cuellar@...).  If you should know e.g. colleagues or
students at master or PhD level who would be suited and potentially
interested, we ask you to pass this information on.

+----------------------------------------------------------------<><-+
|  Dr. David von Oheimb        Senior Research Scientist             |
|  Siemens AG - CT IC 3        Phone: +49 89 636 41173               |
|  Otto-Hahn-Ring 6            Fax  : +49 89 636 48000               |
|  D-81730 München, Germany    EMail: David.von.Oheimb@...   |
|  http://w4.siemens.de/ct/en/technologies/ic/     http://ddvo.net/  |
+--------------------------------------------------------------------+

Re: Semantics of Intersection Types

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

> I am resending this message that was accidentally blocked by the types 
> mailing list.
>
> Adriana
>
> ------------------------------------------------------------------------
>
> Subject:
> Re: [TYPES] Semantics of Intersection Type
> From:
> Adriana Compagnoni <abc@...>
> Date:
> Mon, 28 Nov 2005 22:06:28 -0500
> To:
> Hongseok Yang <hyang@...>, types@...
>
> To:
> Hongseok Yang <hyang@...>, types@...
>
>
>
> In chapter 5 of my PhD thesis you can find a PER model for an 
> extension of F-omega with intersection types.
>
> http://www.cs.stevens.edu/~abc/publications-kind.html
>
> The work is based on earlier joint work with Benjamin Pierce.
>

SPACE 2006: Call for Participation

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

This is the final call for participation for SPACE 2004. Apologies for any 
duplication.

SPACE 2006 

Third workshop on 
SEMANTICS, PROGRAM ANALYSIS, AND 
COMPUTING ENVIRONMENTS FOR MEMORY MANAGEMENT 

January 14, 2006
Charleston, South Carolina 

Sponsored by ACM/SIGPLAN 

http://www.itu.dk/research/plt/space2006/

Early registration deadline: 10 December 2005

------------------------------------------------------------------------

Memory management is a difficult engineering task. We desperately need
new tools and analyses that can identify memory management errors in
low-level C/C++ code, such as dereferencing a pointer to an object
that has been recycled or failing to reclaim an object. We also need
new data structures and algorithms to avoid overheads such as
fragmentation and synchronization. High-level languages such as Java
or ML insulate the programmer from many of these problems through
automatic memory management techniques (e.g., garbage collection). But

CMCS 2006

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

This is the 2nd Call for Papers for CMCS 2006

                           CMCS 2006

8th International Workshop on Coalgebraic Methods in Computer Science
          http://conferences.inf.ed.ac.uk/cmcs06/cmcs06.html

                         Vienna, Austria
                        March 25-27, 2006

The workshop will be held in conjunction with the 9th European Joint
Conferences on Theory and Practice of Software ETAPS 2006
                        March 25 - April 2, 2006

Aims and Scope

During the last few years, it has become increasingly clear that a
great variety of state-based dynamical systems, like transition
systems, automata, process calculi and class-based systems, can be
captured uniformly as coalgebras.  Coalgebra is developing into a
field of its own interest presenting a deep mathematical foundation, a
growing field of applications and interactions with various other
fields such as reactive and interactive system theory, object oriented
and concurrent programming, formal system specification, modal logic,
dynamical systems, control systems, category theory, algebra,
analysis, etc. The aim of the workshop is to bring together
researchers with a common interest in the theory of coalgebras and its
applications.

CfP: International Conference on Emerging Trends in Information and Communication Security 2006

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

============================== Call for Papers =============================

                          International Conference on
            Emerging Trends in Information and Communication Security
    /\
    ||__^_  /\                   ETRICS 2006
_/\_|     \_||______________________________________________________________
                       June 6-9, 2006, FREIBURG, GERMANY
                             http://www.etrics.org

----------------------------------------------------------------------------
IN COOPERATION WITH:
 ACM SIGSAC
 IEEE
 DFG (German Research Foundation)
 GI (German Society for Computer Science)

----------------------------------------------------------------------------
CONFERENCE SCOPE:
 Protecting information and communication systems and services from
malicious use is essential for their deployment and acceptance. In addition
to applying techniques from traditional security research and security
engineering, it is necessary to take into account the vulnerabilities
originating from increased mobility at application level and the integration
of security requirements into business processes. ETRICS solicits research
contributions focusing on emerging trends in security and privacy.
Submissions may present foundational research in security and privacy,
report experiences from novel applications of security technologies, as well

goedel prize 2006 (deadline for nominations Jan. 31, 2006)

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

I'd like to draw your attention on the call for nominations for

GOEDEL Prize 2006

(deadline January 31, 2006)

All information on the nomination process  can be found on the 
following url:

http://www.eatcs.org/

or

http://sigact.acm.org/prizes/godel/

 From both sites you can retrieve the pdf file of the 2006 call which 
has all details about how to submit a nomination.

Best regards,

On behalf of the Award Committee

Pierre-Louis Curien (chair for 2006)

Extended Deadline: QAPL'06 (ETAPS Satellite, Vienna)

[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]

*************** Extended Deadline: 22 Dec 05 ********************

                    Last Call for Papers
                          QAPL 2006
  4th Workshop on Quantitative Aspects of Programming Languages
                       April 1-2, 2006

                       Vienna, Austria
                Satellite Event of ETAPS 2006

            *** Extended Deadline: 22 Dec 05 ***

-----------------------------------------------------------------
Scope:

Quantitative aspects of computation are important and sometimes
essential in characterising the behaviour and determining the
properties of systems. They are related to the use of physical
quantities (storage space, time, bandwidth, etc.)  as well as
mathematical quantities (e.g. probability and measures for
reliability, risk and trust). Such quantities play a central role in
defining both the model of systems (architecture, language design,
semantics) and the methodologies and tools for the analysis and
verification of system properties.

The aim of this workshop is to discuss the explicit use of
quantitative information such as time and probabilities either
directly in the model or as a tool for the analysis of systems. In