headers
berline | 3 Jun 1996 17:31
Picon
Favicon

A kappa-denotational semantics of Map Theory.


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The following paper is now available by ftp and by WWW :

"A kappa-denotational semantics for Map Theory in ZFC+SI"
         by Chantal Berline and Klaus Grue

It is a revised and considerably augmented version of a preprint which
circulated previously and was entitled "A simple consistency proof for
Map Theory, based on xsi-denotational semantics".

This has been added in the new paper :
A presentation of Map Theory and many motivations and intuitions ;
 comprehensive treatment of the set-theoretic properties of the models
The proof of the computational adequacy of the canonical models ;
A comparison with Flagg-Myhill's system.

Furthermore, the consistency proof, which formerly followed a bottom-up
approach, has been considerably restructured.

The paper is available in .ps and .dvi versions on both of the
following sites :

1) WWW page (at DIKU in Denmark) :

 http://www.diku.dk/research-groups/topps/personal/grue/consis960415.html

2) by ftp (in Paris)
(Continue reading)

Permalink | Reply | 0 comments |
headers
fairouz | 4 Jun 1996 19:50
Picon
Picon
Favicon

International School on Type Theory and Term Rewriting


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

\documentstyle[11pt,fleqn,a4wide]{article}
\title{International School on Type Theory and Term Rewriting\\
Glasgow University\\
Sept 12-15 1996}
\author{}
\date{}
\begin{document}
\maketitle
\thispagestyle{empty}

In the past twenty years, a very rich body of results has emerged in
{\em type theory} and {\em term rewriting systems}.  This is
unsurprising since these topics are at the heart of the theory and
implementation of programming languages.  Type theory enables
increasing expressiveness in programming languages and in theorem
proving, whilst retaining strong theoretical and applied properties.
Understanding {\em termination} and {\em reduction strategies} in Term
rewriting systems provides insights into increasingly efficient
implementations with safe theoretical foundations.  Furthermore, the
two notions of type theory and term rewriting are very general and
cover various topics including termination, calculi of substitutions,
subtyping, reduction, unification, interaction and process calculi,
the logic of programs and theorem proving.

\noindent
Unfortunately, collaboration between type theory and term rewriting
systems is not as strong as it should be despite their common goals
(Continue reading)

Permalink | Reply | 0 comments |
headers
Doug Howe | 5 Jun 1996 05:49
Picon

FLoC'96: Second Call for Participation


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

                   1996 FEDERATED LOGIC CONFERENCE

                               FLoC'96

    July 27 - August 3, 1996, Rutgers University, New Jersey, USA

   CADE: 13th International Conference on        July 30 - August 3
         Automated Deduction 

   CAV:  8th International Conference on         July 31 - August 3
         Computer-Aided Verification 

   LICS: 11th Annual IEEE Symposium on           July 27 - July 30
         Logic in Computer Science 

   RTA:  7th International Conference on         July 27 - July 30
         Rewriting Techniques and Applications 

     +---------------------------------------------------------+
     |                                                         |
     |                       *DEADLINES*                       |
     |                                                         |
     | Early Registration                          21 Jun 1996 |
     | On-Campus Housing Reservation               21 Jun 1996 |
     | Hotel Reservation                           28 Jun 1996 |
     |                                                         |
     +---------------------------------------------------------+
(Continue reading)

Permalink | Reply | 0 comments |
headers
Eelco Visser | 7 Jun 1996 13:01
Picon
Picon

Multi-Level Specifications (new papers)


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Multi-level specification is an extension of first-order many-sorted
algebraic specification that incorporates the definition of types in
the formalism itself. The following papers, available from

	http://adam.fwi.uva.nl/~visser/types/mls/ 

, discuss the design and implementation of the modular, applicative,
multi-level equational specification formalism MLS. Comments are
welcome.

regards,
	Eelco Visser

---
mail:visser@...
http://adam.fwi.uva.nl/~visser/

Multi-Level Specifications
--------------------------

Abstract. This chapter introduces a modular, applicative, multi-level
equational specification formalism that supports algebraic
specification with user-definable type constructors, polymorphic
functions and higher-order functions. Specifications consist of one or
more levels numbered 0 to n. Level 0 defines the object level
terms. Level 1 defines the types used in the signature of level 0. In
general, the terms used as types in level n are defined in level
(Continue reading)

Permalink | Reply | 0 comments |
headers
David Lujun Shang | 7 Jun 1996 20:00
Picon

Subtypes vs. Convertible Types


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

My recent paper titled "Subtypes and Convertible Types" tries to answer
the following questions:

	* What are subtypes after all?
	* When should subtype rules be used?
	* Are subclasses subtypes?
	* Can we have more subclasses and hence more subtypes?
	* Can we have more convertible types?

For detail, go to

	http://www.sigs.com/publications/docs/oc/9606/oc9606.c.shang.html

Your comments are welcome!

David Shang

David Lujun Shang                        email: shang@...
Software Systems Research Laboratory     Voice: (708)538-3738
Motorola Corparate Software Center       Fax:   (708)576-2025
1303 East Algonquin Road, Annex 2        MD:    IL01/ANX2
Schaumburg, Illinois 60196
Permalink | Reply | 0 comments |
headers
Roland Yap Hock Chuan | 11 Jun 1996 14:07
Picon

CFP reminder: ASIAN'96


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

[We apologize if you receive this multiple times]

                        CALL FOR PAPERS --- ASIAN'96

                     ASIAN COMPUTING SCIENCE CONFERENCE

                       Singapore, December 2-5, 1996

                                 BACKGROUND
                                 ----------

The  first  conference  ASIAN'95 (also called ACSC'95 last year) was held
in Bangkok, Thailand, in December 1995, organized by the Asian Institute
of Technology in partnership with INRIA, France, and the UNU/IIST, Macau.
Its main purpose was to provide a local forum for Asian researchers in
Computer Science.  Its scope was a  broad coverage of CS, though there was
a focus on the more conceptual areas of algorithms, concurrency and
knowledge.  Its proceedings appeared as  Springer-Verlag's LNCS 1023.

                                   SCOPE
                                   -----

The  1996  conference will continue to emphasize the conceptual areas of CS,
though papers in all areas will be considered.  The following themes
represent the areas of focus for this year.

* Programming (semantics, languages, systems, paradigms, ...)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Sophia Drossopoulou | 11 Jun 1996 14:06
Picon
Picon
Favicon

Soundness of the C++ or Java type system


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Does anybody know of any formal proofs, or informal arguments
that show that C++ or Java have a sound type system?

If I get any replies, I will compile the answers and post
on this news group.

Thanks in advance,

Sophia Drossopoulou,
Imperial College,
London
Permalink | Reply | 0 comments |
headers
bellin | 11 Jun 1996 15:07
Picon
Favicon

paper announcement for linear mailing list


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

The following paper is available by anonymous ftp boole.logique.jussieu.fr    

SUBNETS OF PROOF-NETS IN MULTIPLICATIVE LINEAR LOGIC WITH MIX

                      by GIANLUIGI BELLIN
             (Equipe de Logique -- Universite' de Paris 7) 

ABSTRACT: The paper studies the properties of the subnets of a proof-net for
first order Multiplicative Linear Logic without propositional constants (MLL-),
extended with the rule of Mix:

                      |- Gamma      |- Delta
                      -----------------------
                          |- Gamma, Delta

Asperti's correctness criterion and its interpretation in terms of concurrent
processes are extended to the first order case.
The notion of *kingdom* and *empire* of a formula are extended from MLL- to
MLL- + MIX. A new proof of the sequentialization theorem is given.
As a corollary, a system of proof-nets is given for De Paiva and Hyland's
Full Intuitionistic Linear Logic with Mix; this result gives a general method
to translate Abramsky-style term assignments into proof-nets, and viceversa.

To appear in Mathematical Structures in Computer Science. 

                              ---- * ----
(Continue reading)

Permalink | Reply | 0 comments |
headers
Magne.Haveraaen | 12 Jun 1996 14:26
Picon
Picon

8th Nordic Workshop on Programming Theory (short announcement)


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Although not explicitly mentioned in the list of typical topics, the
programming theory notion encompasses the topics covered by the ``types''
list, and in previous years many ``types'' related topics have been
presented at the NWPT meetings.

Magne

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

              First Announcement and Call for Participation

                 8th Nordic Workshop on Programming Theory
                    Oslo, Norway, 4-6 December 1996

The objective of the workshop is to bring together researchers from the
Nordic and Baltic countries interested in programming theory, in order to
improve mutual contacts and cooperation.  Typical topics of the workshop
include (but are not limited to):

  -  Semantics of programs
  -  Programming logics
  -  Program verification
  -  Formal specification of programs
  -  Program synthesis
  -  Program transformation and program refinement
  -  Modeling of concurrency
  -  Programming methods
(Continue reading)

Permalink | Reply | 0 comments |
headers
Benjamin C. Pierce | 16 Jun 1996 15:34
Picon
Picon
Favicon

FOOL 4: Call for papers / appel `a communications


[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

                         Call for Papers

                The Fourth International Workshop on
             Foundations of Object-Oriented Languages
                             FOOL 4

                         18 January, 1997
                          Paris, France
                 Held in conjunction with POPL '97

While object-oriented programming languages have swept the programming
community over the last decade, it has taken longer for the language
theory community to develop sound theoretical foundations for these
languages.  However, work over the last several years has provided a
better understanding of the key concepts of object-oriented languages
and has led to important developments in the type theory, semantics,
and verification of object-oriented languages.  The FOOL workshops
bring together researchers to share new ideas and results.

FOOL 3 will be held this summer, July 24-25, in conjunction with LICS
'96 and the Federated Logic Conference.  Details of the program and
information about registration can be found through the FOOL 3 home
page, http://www.cs.williams.edu/~kim/FOOL.

The next workshop, FOOL 4, will take place on 18 January, 1997, the
day following POPL '97, in Paris.  Submissions for this event are
invited in the general area of theoretical foundations of object-
(Continue reading)

Permalink | Reply | 0 comments |

Gmane