headers
Workshop unif03 | 1 Apr 2003 14:49
Picon

UNIF'03 second call for papers


             Call for Papers/Abstracts/System descriptions
                              UNIF 2003
               17th International Workshop on Unification
                           June 8-9, 2003
                          Valencia,  Spain
            Affiliated with RTA'03 and TLCA'03, Part of RDP'03

                    http://www.iiia.csic.es/~unif03

UNIF is the main international meeting on unification. Unification is
concerned with the problem of identifying given terms, either
syntactically or modulo a given logical theory. Syntactic unification
is the basic operation of most automated reasoning systems, and
unification modulo theories can be used, for instance, to build in
special equational theories into theorem provers.

The aim of UNIF 2003, as that of the previous meetings, is to to bring
together people interested in unification, present recent (even
unfinished) work, and discuss new ideas and trends in unification and
related fields. In particular, it is intended to offer a good
opportunity for young researches and researchers working in related
areas to get an overview of the current state of the art in
unification theory and get in contact with the experts in the field.

----------------------------------------------------------------------
TOPICS OF INTEREST
----------------------------------------------------------------------

    * Unification
(Continue reading)

Permalink | Reply | 0 comments |
headers
Jean-Marie JACQUET | 2 Apr 2003 17:50
Picon
Favicon

Foclasa: 1st Call for Papers

                      2nd International Workshop on
                  Foundations of Coordination Languages and
                          Software Architectures
                              (Foclasa 2002)

                   September 2, 2003, Marseille, France
           Workshop affiliated to CONCUR'2003, 02 - 06 September 2003.

              http://www.info.fundp.ac.be/~jmj/Foclasa03.html 

======================================================================

SCOPE AND TOPICS

    Modern  information  systems  rely  more  and  more  on  combining
    concurrent, distributed, mobile and heterogenous components.  This
    move from  old systems, typically conceived  in isolation, induces
    the  need  for  new   languages  and  software  architectures.  In
    particular, coordination  languages have been  proposed to cleanly
    separate  computational aspects  and communication.  On  the other
    hand,  software  architects face  the  problem  of specifying  and
    reasoning  on non-functional requirements.   All these  issues are
    widely perceived as  fundamental to improve software productivity,
    enhance maintainability, advocate modularity, promote reusability,
    and  lead   to  systems  more  tractable  and   more  amenable  to
    verification and global analysis.         

    The aim of  the workshop is to bring  together researchers working
    on the foundations of component-based computing, coordination, and
    software architectures.  Topics of  interest include (but  are not
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe Castagna | 3 Apr 2003 12:45
Picon
Picon
Favicon

types as set of values

Dear typers,

   interpreting a type of a language as the set of the _values_ of the
language that have that type is an idea that belongs to the type
folklore. I am trying to trace back this idea, and the oldest paper I
was able to find that mentions it is the Amadio and Cardelli paper on
subtyping recursive types, but I am pretty sure that older references
must exist. Has anyone a better (i.e. older) reference?

Thanks in advance

---Beppe---
Permalink | Reply | 0 comments |
headers
frb | 3 Apr 2003 13:54
Picon
Picon
Favicon

FMCO 2003: Call for Participation

ANNOUNCEMENT OF
The Second International Symposium on 
Formal Methods for Components and Objects (FMCO 2003)

DATES 4 - 7 November, 2003
PLACE Lorentz Center, Leiden University, Leiden, The Netherlands
URL http://fmco.liacs.nl/fmco03.html

OBJECTIVE
The objective of this symposium is to bring together researchers
and practioners in the areas of software engineering and formal methods
to discuss the concepts of reusability and modifiability in
component-based and object-oriented software systems.

FORMAT
The symposium is a four days event in the style of the former 
REX workshops,organized to provide an atmosphere that fosters 
collaborative work, discussions and interaction.
The program consists of keynote and technical presentations,
and contains an exquisite social event.
Speakers' contributions will be published after the symposium in
Lecture Notes in Computer Science by Springer-Verlag.

KEYNOTE SPEAKERS
Desmond D'Souza (Kinetium, Austin, USA)
E. Allen Emerson (University of Texas at Austin, USA)
Andrew D. Gordon (Microsoft Research, UK)
Yuri Gurevich (Microsoft Research, USA)
Tony Hoare (Microsoft Research, UK)
David Parnas  (University of Limerick, IE)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Uwe.Nestmann | 3 Apr 2003 16:45
Picon
Picon
Favicon

Re: types as set of values


>>>>> "GC" == Giuseppe Castagna <Giuseppe.Castagna@...> writes:

GC>    interpreting a type of a language as the set of the _values_ of the
GC> language that have that type is an idea that belongs to the type
GC> folklore. I am trying to trace back this idea, and the oldest paper I
GC> was able to find that mentions it is the Amadio and Cardelli paper on
GC> subtyping recursive types, but I am pretty sure that older references
GC> must exist. Has anyone a better (i.e. older) reference?

You find links to older references on
http://doi.acm.org/10.1145/512927.512938
of the paper "Types are not sets" :-)

One by Reynolds apparently of 1969 ...

== Uwe ==
Permalink | Reply | 0 comments |
headers
Robert Harper | 3 Apr 2003 18:04
Picon
Favicon

RE: types as set of values

Martin-Loef's Constructive Mathematics and Computer Programming is founded
on the notion of the canonical forms of a type, which would correspond to
the values of that type in a PL setting.  Roughly speaking, a type is
defined by the canonical forms that inhabit it (and by what counts as
equality between them).  A variant of this semantics was used as the basis
for the NuPRL type theory.  The formulation of type safety as
progress+preservation is also based on this conception of type; the crux of
the progress lemma is to identify the canonical forms of each type.

Bob Harper

-----Original Message-----
From: Uwe.Nestmann@... [mailto:Uwe.Nestmann <at> epfl.ch]
Sent: Thursday, April 03, 2003 9:45 AM
To: Giuseppe Castagna
Cc: types@...
Subject: Re: types as set of values

[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

>>>>> "GC" == Giuseppe Castagna <Giuseppe.Castagna@...> writes:

GC>    interpreting a type of a language as the set of the _values_ of the
GC> language that have that type is an idea that belongs to the type
GC> folklore. I am trying to trace back this idea, and the oldest paper I
GC> was able to find that mentions it is the Amadio and Cardelli paper on
GC> subtyping recursive types, but I am pretty sure that older references
GC> must exist. Has anyone a better (i.e. older) reference?

You find links to older references on
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ed Lowry | 3 Apr 2003 17:43
Picon
Favicon

Re: types as set of values

This reponds to Giuseppe Castagna's request (below) for old
references on type ideas. The NATO Science Committee Conference
"Techniques in Software Engineering" In Rome, October 1969
distributed a book of "Working Material Volume II" dated
September 1969. It includes 2 papers:

  - "The programming language PASCAL and its design criteria"
by N. Wirth

  - "Proposed language extensions to aid coding and analysis of large
programs" by E. S. Lowry. It was also published with the same
title as IBM Poughkeepsie Lab Technical Report TR 00.1940-1,
November 21, 1969.

Both papers present the idea of types as sets of values. In my
paper they were called ranges rather than types. The extensions
in my language "Extended Systems Language" were built onto the
"Basic Systems Language" used internally at IBM and later called
PL/S.

I gather that Niklaus Wirth and I were both developing the ideas
independently during 1968.

I continued  by including more comprehensive executable set
referencing and removing machine oriented ideas in order to
improve simplicity of expression in an integrated programming and
data base language. That was first published as "PROSE
Specification" IBM Poughkeepsie Lab Technical Report TR 00.2909,
Nov 1977.
(Continue reading)

Permalink | Reply | 1 comment |
headers
Jason Hickey | 4 Apr 2003 00:30
Picon
Favicon

Re: Course materials using "Types and Programming Languages"

I've taught a course using Pierce's book, an excellent book indeed. 
Lecture notes and homeworks are online at

http://www.cs.caltech.edu/~jyh/classes/cs101/index.html

This was an introductory undergraduate/graduate level course.  One note: 
you'll see a moderate bias toward interpreting type systems using 
intuitionistic logic.  Let me know if you find it helpful or need 
clarification on any of the course material.

Jason

James Riely wrote:
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> I am teaching an introductory semantics course concentrating on
> operational semantics and type systems using "Types and Programming
> Languages" by Pierce, and I am prowling for course materials.  I am
> aware of Pierce's notes for CIS500 at http://www.seas.upenn.edu/~cis500/
> 
> If you have developed materials for any class that uses the book and
> would not mind to share, please drop me a line.  I will post a summary
> if I get any responses!
> 
> Cheers,
> James.
> 
> [ I can also add links to the TAPL home page.  -BCP ]
>
(Continue reading)

Permalink | Reply | 0 comments |
headers
MERLIN'03 | 4 Apr 2003 12:40
Picon
Favicon

CfP: ACM SIGPLAN MERLIN 2003


                            Call for Papers
                      Second ACM SIGPLAN Workshop
      MEchanized Reasoning about Languages with variable bINding

                              MERLIN 2003

      Uppsala, Sweden, 26 August 2003 in association with PLI 2003

                   **********************************
                   *  http://merlin.dimi.uniud.it/  *
                   **********************************

KEYWORDS

Induction and Coinduction, Logical Frameworks, Mechanization,
Metaprogramming, Operational Semantics, Programming Languages, Theorem
Proving, Variable Binding.

SCOPE AND AIMS

Currently, there is  considerable interest in the use  of computers to
encode (operational)  semantic descriptions of  programming languages.
Such encodings  are often  done within the  metalanguage of  a theorem
prover  or related  system.   The  encodings may  require  the use  of
variable   binding  constructs,  inductive   definitions,  coinductive
definitions, and associated schemes  of (co)recursion.  The broad aims
are to  run a  short, but highly  focused meeting, which  will provide
researchers and practitioners with a  forum to review state of the art
results and techniques, and to  present recent and new progress in the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Pierre-Louis Curien | 4 Apr 2003 22:34
Picon

symposium announcement

Preliminary Announcement ISDT'03

The 3rd International Symposium on Domain Theory

September 19-23, 2003, Xi'an, China

PURPOSE
The International symposium on Domain Theory 2003 will take place on 
the campus of
Shaanxi Normal University in Xi'an, China, from September 19 to 
September 23, 2003
(the first ISDT was held in Shanghai, October 17-24, 1999, and the 
second ISDT was held
in  Chengdu, China, October 22-26, 2001). This conference is intended 
to be a forum for
researchers in domain theory and its applications. The conference 
series also aims
to broaden its scope of applications in computer science and 
mathematics.

INVITED SPEAKERS (CONFIRMED)

          Samson Abramsky, Oxford University, England
          Jimmie Lawson, Louisiana State University, USA
          Prakash Panangaden, McGill University, Canada
          Gordon Plotkin, University of Edinburgh, UK
          Vaughan Pratt, Stanford University, USA
          Glynn Winskel, University of Cambridge, England
          Guo-Qiang Zhang, Case Western Reserve University, USA
(Continue reading)

Permalink | Reply | 0 comments |

Gmane