Parametricity, interpolation and definability

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

Hello,

I'm wondering if parametricity (or type abstraction) has been related
to Craig interpolation (or Beth definability).  The concept of logical
relations, and mapping related arguments to related results, seems to me
tantalizingly similar to the notion of implicit definition, but I am
having trouble stating a concrete connection.

I will of course summarize the responses.

Thank you,
	Ken

--

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
BBC News: Universities face week of protest
http://news.bbc.co.uk/1/hi/education/3508209.stm

CFP: DALT 2004 - Second International Workshop on Declarative Agent Languages and Technologies

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

-------------------------------------------------------------
           C A L L   F O R   P A P E R S

      The Second International Workshop on
  Declarative Agent Languages and Technologies (DALT-2004)
http://centria.di.fct.unl.pt/~jleite/dalt04/index.htm

                 to be held at the
  The Third International Joint Conference on Autonomous
Agents & Multi-Agent Systems (AAMAS 2004) New York, USA
                July 19th, 2004
-------------------------------------------------------------

----------
Overview:
----------

Building multi-agent systems still calls for models and
technologies that ensure system predictability, enable feature
discovery and verification, and accommodate flexibility.
Declarative approaches offer to satisfy precisely these properties
of large-scale multi-agent systems. Recent advances in the area of
computational logics provide a strong foundation for declarative
languages and technologies. Equipped with such strong foundation,
declarative approaches can enable agents to reason about their
interactions and their environment and hence not only establish
the required tasks but also handle exceptions that arise in many
systems.

2nd International Doctoral School "Chambéry - Torino"

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

2nd International Doctoral School "Chambéry - Torino"
In Theoretical Computer Science and in Semantic Web

21-25, June 2004 Aussois (Savoie - France)

http://www.univ-savoie.fr/Portail/Groupes/DoctoralSchoolChyTurin/Index.html

contact: AussoisSchool@...

1. Objectives

The 2004 edition of the International Summer School of Aussois will 
concern students, researchers and engineers from both theoretical and 
applied computer science.

One of the aims of this school is also to encourage cross-border 
co-operation and to nurture the scientific work of the Ph.D. students 
who attend the courses.

2. Topics

The school will start with a common day on non-classical logic: we will 
introduce modal logics and present the background of the logic of 
knowledge with some of its applications.

The two main topics will be then studied in parallel.

The school in theoretical computer science will consist of two courses: 

Concur 2004: Invited speakers

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

15th International Conference on Concurrency Theory: CONCUR 2004

New information since first call for papers on the Types list:

Invited speakers

*  Sriram K. Rajamani (Microsoft Research): Invited Talk on Zing (a
    model-checking tool based on ideas from process algebra)

*  Peter O'Hearn (Queen Mary University of London) and Steve Brookes
    (Carnegie-Mellon): Tutorial on Local Reasoning about Concurrent
    Imperative Programs

*  Bengt Jonsson (Uppsala): Tutorial on Regular Model Checking

Submission is now open.

There will be a special issue of the journal Theoretical Computer 
Science associated with Concur 2004.

--------------------------------
Second Call for Papers for CONCUR 2004

CONCUR 2004, the 15th International Conference on Concurrency Theory,
takes place at the Royal Society, London, Tuesday 31 August - Friday 3
September 2004. As well as the main event, we will also hold many
workshops on Monday 30th August and Saturday 4th February, as detailed
below.  Further information is available at the conference's web site

ICFP Deadline 4/1; Submission site now open

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

International Conference on Functional Programming

Call for Papers
ICFP 2004
September 19-22, 2004
Snowbird, Utah

IMPORTANT DATES
Submission deadline   23:00  01 April, 2004 Apia, Samoan time (Thursday)
Author review period  23:00 17 May to 23:00 19 May, 2004, Apia, Samoan time
Author notification   26 May, 2004
Final paper due       07 July, 2004
Conference            19-22 September, 2004

SCOPE
ICFP 2004 seeks original papers on the full spectrum of the art,
science, and practice of functional programming. The conference
invites submissions on all topics ranging from principles to practice,
from foundations to features, and from abstraction to application. The
scope covers all languages that encourage functional programming,
including both purely applicative and imperative languages, as well as
languages that support objects and concurrency. Topics of interest
include, but are not limited to, the following:

Foundations: Formal semantics, lambda calculus, type theory, monads, continuations,
control, state, effects.

Design: Algorithms and data structures, modules and type systems,

CFP: Haskell Workshop 2004

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

Please find enclosed the Call For Papers for the 2004 Haskell Workshop,
to be held on 22 September in Snowbird, Utah, USA in association with
ICFP'04.

My apologies for multiple copies.

Best regards,

/Henrik

--

-- 
Henrik Nilsson
School of Computer Science and Information Technology
The University of Nottingham
nhn@...

			    2004 Haskell Workshop
		   Snowbird, Utah, USA, 22 September, 2004

		     http://www.cs.nott.ac.uk/~nhn/HW2004

			       Call For Papers

The Haskell Workshop 2004 is intended to form part of the 2004 International
Conference on Functional Programming (ICFP) as an associated, ACM SIGPLAN
sponsored workshop. It has been accepted by the ICFP'04 workshop committee;

ICFP Poster Session

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

The 2004 ICFP Poster Session
         http://abstract.cs.washington.edu/~djg/icfp-poster.html

Part of the 2004 International Conference on Functional Programming
        http://www.cs.indiana.edu/icfp04/

The 2004 International Conference on Functional Programming (ICFP) will
include a poster session during the first day of the conference. The
poster session aims to give students and professionals an opportunity to
gain experience presenting technical material to the research community,
and to get technical advice from leading researchers in the field.

PARTICIPANT OBLIGATIONS:

    * Sign-up via the on-line form below by June 30, 2004.
    * Submit a one-page abstract summarizing the poster topic by July 15, 2004.
    * Register for ICFP 2004. (There is no separate poster registration
      beyond the on-line sign-up form.)
    * Prepare a poster and attend the session on September 19, 2004. 

In addition, participants are strongly encouraged to prepare a short
article (roughly 2 or 3 pages) for peer feedback and to provide feedback
for some other participants' articles. This process should improve the
quality of the posters. Articles should be submitted by August 1, 2004.

NUMBER OF PARTICIPANTS:

    * We hope to accomodate everyone wishing to participate, but may

CFP: FORMATS+FTRTFT 2004 -- DEADLINE EXTENDED APRIL 15, 2004

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

[Sergio Yovine writes:  Contributions on type systems for 
object-oriented, real-time, concurrent, distributed, fault-tolerant, and 
mobile programming are welcome. --SCW ]

*--------------------------------------------------------------------*
*                          Call for Papers                           *
*                                                                    *
*                        Joint Conference on                         *
*      Formal Modelling and Analysis of Timed Systems (FORMATS)      *
*                                 and                                *
* Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT) *
*                                                                    *
*               September 22-24, 2004, Grenoble, France              *
*--------------------------------------------------------------------*
*                                                                    * 
* !!!!!!!!!!!   DEADLINE EXTENSION        APRIL 15, 2004 !!!!!!!!!!! *
*                                                                    * 
*--------------------------------------------------------------------*
*               Submission deadline:      April 15, 2004             *
*               Notification to authors:    June 1, 2004             *
*               Final version:             June 20, 2004             *
*--------------------------------------------------------------------*
* http://www-formats-ftrtft.imag.fr           FORMATS.FTRTFT@... *
*--------------------------------------------------------------------*

Computer systems are becoming increasingly widespread in real-time and
safety-critical applications such as embedded systems.  Such systems
are characterised by the crucial need to manage their complexity in

new book

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

Dear type theorists,

My book "Call-By-Push-Value" has been published by Kluwer in the "Semantic 
Structures in Computation" bookseries

http://www.wkap.nl/prod/b/1-4020-1730-8

- and I hope it will be of interest to many people on this list.  
Although it is based on my PhD thesis, subsequent research has led to a
great deal of simplification.  In particular, the introduction of a typing
judgement (and denotational semantics) for stacks has made both the
individual models and the categorical structure more straightforward and
less mysterious.

Here's the blurb:

"Call-By-Push-Value
A Functional/Imperative Synthesis

"Call-by-push-value is a programming language paradigm that, surprisingly,
breaks down the call-by-value and call-by-name paradigms into simple
primitives. This monograph, written for graduate students and researchers,
exposes the call-by-push-value structure underlying a remarkable range of
semantics, including operational semantics, domains, possible worlds,
continuations and games.

"After introducing basic ideas using domain semantics and a stack machine,
the book is layered to appeal to readers in a variety of fields. One

ICFEM 2004 -- Call for Papers, Tutorials, Workshops, Seattle, USA

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

ICFEM 2004 CALL FOR PAPERS, and Tutorials, Workshops 

[apologies for multiple copies]
Please help to distribute.

Sixth International Conference on 
Formal Engineering Methods (ICFEM 2004), 

November 8-12, 2004, Seattle,USA

http://research.microsoft.com/conferences/ICFEM2004

Important Dates: 
   Submission of paper:        15th May 2004 
   Notification of acceptance: 1st July 2004 
   Final copy for Proceedings: 1st August 2004
   Conference:                 8-12 November, 2004

Tutorials, Workshops:
   Submission of Proposals: 1 June 2004 
   Acceptance notification: 30 June 2004 

Formal engineering methods are changing the way that systems are 
developed. With language and tool support, these methods are being 
used for semi-automatic code generation, and for the automatic 
abstraction and checking of implementations. In the future, they 
will be used at every stage of development: requirements, 
specification, design, implementation, testing, and documentation.