Lawrence C Paulson | 10 May 10:57 1994
Picon
Picon

paper available (draft)


The following paper is available by anonymous ftp from the University of
Cambridge.  Instructions:

* Connect to host ftp.cl.cam.ac.uk [128.232.0.56]
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary") 
* go to directory ml (by typing "cd ml")
* "get" the file final.ps.gz from that directory.  

				Lawrence C Paulson, University Lecturer

				Computer Laboratory, University of Cambridge,
				Pembroke Street, Cambridge CB2 3QG, England
				Tel: +44(0)223 334623    Fax: +44(0)223 334678

     A Concrete Final Coalgebra Theorem for ZF Set Theory
                     by Lawrence C. Paulson

  A special final coalgebra theorem, in the style of Aczel's, is proved within
standard Zermelo-Fraenkel set theory.  Aczel's Anti-Foundation Axiom is
replaced by a variant definition of function that admits non-well-founded
constructions.  Variant ordered pairs and tuples, of possibly infinite length,
are special cases of variant functions.  Analogues of Aczel's Solution and
Substitution Lemmas are proved in the style of Rutten and Turi.

  The approach is less general than Aczel's; non-well-founded objects can be
modelled only using the variant tuples and functions.  But the treatment of
non-well-founded objects is simple and concrete.  The final coalgebra of a
functor is its greatest fixedpoint.  The theory is intended for machine
(Continue reading)

ohearn | 18 May 20:30 1994
Picon

Kripke Logical Relations and PCF


The following manuscript can is available by anonymous ftp from
top.cis.syr.edu in ohearn/pcf.dvi or ohearn/pcf.ps.

		 Kripke Logical Relations and PCF
		Peter W. O'Hearn and Jon G. Riecke

ABSTRACT: Sieber has described a model of PCF consisting of
continuous functions that are invariant under certain (finitary)
logical relations, and shown that it is fully abstract up to rank
three types.  We show that one may achieve full abstraction at ALL
types using a form of ``Kripke logical relations'' introduced by
Jung and Tiuryn to characterize lambda-definability.

HONSELL | 18 May 05:15 1994

School on Typed Lambda Calculus ( final announcement )


Please find below the text and LateX versions of
- the final Announcement of the "Advanced School on Typed Lambda Calculus and
  Functional Programming" to be held in Udine (ITALY) September 19-30, 1994
- Application Form
- Grant Application Form

[A preliminary announcement appeared earlier -- Moderator] 

 
                 A D V A N C E D   S C H O O L   O N
               T Y P E D   L A M B D A   C A L C U L U S
          A N D   F U N C T I O N A L   P R O G R A M M I N G

      S e p t e m b e r   1 9  -  S e p t e m b e r   3 0 , 1 9 9 4
             C I S M  ,  P a l a z z o   d e l   T o r s o
                 P i a z z a   G a r i b a l d i   1 8
                        U d i n e  -  I T A L Y

 

THE ADVANCED SCHOOL IS ORGANIZED UNDER THE AUSPICES OF THE ITALIAN CHAPTER OF

EATCS (EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE) AND UNESCO.

IT IS SPONSORED AND SUPPORTED BY:

- U N E S C O  PROJECT FUND IN TRUST WITH THE ITALIAN FOREIGN MINISTRY:
  "EDUCATION IN BASIC SCIENCES FOR INFORMATICS"

(Continue reading)

Paolo Mancarella | 24 May 13:51 1994
Picon
Picon

Complete Programme of META94 - LOPSTR 94 - Compunet Area Meeting


Please find enclosed the programme of the META 94 and LOPSTR 94 workshops
(June 20-21, 1994) and of the Compunet Program Development Area Meeting
(June 22), and the registration and accommodation forms.
We apologize if you receive this more than once.
-------------------------------------------------

 +---------------------------------------------------+
 |                                                   |
 |                     META 94                       |
 |         Fourth International Workshop on          |
 |           Meta Programming in Logic               |
 |                                                   |
 |                      and                          |
 |                                                   |
 |                   LOPSTR 94                       |
 |         Fourth Workshop on Logic Program          |
 |            Synthesis and Transformation           |
 |                                                   |
 |                  June 20-21                       |
 |                                                   |
 |                                                   |
 |     COMPUNET Program Development Area Meeting     |
 |                                                   |
 |                   June 22                         |
 |                                                   |
 |                                                   |
 |              Palazzo dei Congressi                |
 |                 via Matteotti, 1                  |
 |                  PISA, Italy                      |
(Continue reading)

Amy Felty | 31 May 01:39 1994
Picon

Reminder: LICS'94 Registration

[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list: send announcements or requests to subscribe to
THEORY-A@...  -- Philip Wadler, moderator, Types Forum.]

REMINDER:  THE DEADLINE FOR LICS EARLY REGISTRATION IS JUNE 6.

                      LOGIC IN COMPUTER SCIENCE                   
                   ********************************
                     Ninth Annual IEEE Symposium
                    July 3-7, 1994, Paris, France

NOTE: Advance payment for registration by credit card is not possible.
However, it is possible to pay by credit card or cash in French Francs
on location at CNAM.  In order to get the early registration rate,
send the registration form so that it is received before June 6,
circle the reduced rate (and the banquet fee if you wish to attend the
banquet), and indicate that you will pay on site with cash or one of
the following authorized cards: Visa international, Eurocard,
MasterCard.  If you choose to pay by this method and are subsequently
unable to attend, you are requested to send mail to symposia@...

Other forms of payment (as stated in the brochure, but with some
clarification) are as follows.  Payment must be in French currency.

1. Bank check (also called foreign draft in the US) or postal check
made payable to Agent Comptable de l'INRIA.

2. Bank transfer.
Beneficiary: Agent Comptable de l'INRIA
(Continue reading)

Andreas Hense | 30 May 16:02 1994
Picon

Thesis on type inference for object-oriented languages available


I am pleased to announce the publication of my thesis:

POLYMORPHIC TYPE INFERENCE FOR OBJECT-ORIENTED PROGRAMMING LANGUAGES

                       Andreas V. Hense
                 Universit"at des Saarlandes, 1994

        (Supervisors: Prof. Dr. G. Smolka, Prof. Dr. R. Wilhelm)

Object-oriented programming languages enjoy an ever growing
popularity.  These languages promise an increased productivity by
favorizing code reuse.  Object-oriented languages undoubtedly have the
reputation of leading to main- tainable and expandable systems.
However, they are not regarded as very safe in the sense that
object-oriented programs are free of errors.  They are well- suited
for rapid prototyping, not for end products. A major part of the
errors in a dynamically typed language are type errors, in
object-oriented terminol- ogy they translate by "message not
understood".  Such errors cannot always be eliminated by testing.
Static type inference analyzes programs at compile time and guarantees
their absence at runtime. Whereas monomorphic type dis- ciplines
restrain reusability, polymorphic type inference provides the
necessary flexibility.

Despite its apparent urgency, the problem of inferring types for
object- oriented languages has still not been solved satisfactorily.
This work is con- cerned with the type inference for a complete
object-oriented language, thus showing the multiple facets of the
problem.  The type inferencer is of direct practical use but the work
(Continue reading)


Gmane