headers
Lawrence C Paulson | 1 Dec 1993 13:15
Picon
Picon
Favicon

Summer course on Isabelle


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

Dear Colleague,

Please forward the attached course announcement.  The course will be held one
week after LICS and two weeks after CADE, to facilitate travel arrangements. 
Please send technical questions to Larry.Paulson@... and
administrative ones to rt10005@...

I apologize for multiple copies.

							Larry Paulson

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

UNIVERSITY OF CAMBRIDGE
Programme for Industry

Introduction to Theorem Proving, using "Isabelle"

11-13 July 1994
Course fee 650 pounds sterling (350 pounds sterling for academic participants)

AIM OF THE COURSE

Theorem proving systems are growing in popularity and are demonstrating
(Continue reading)

Permalink | Reply | 0 comments |
headers
Amy Felty | 1 Dec 1993 17:46
Picon

REMINDER: LICS'94 submission deadline


[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.]

                    Ninth Annual IEEE Symposium on
                      LOGIC IN COMPUTER SCIENCE
		    July 4-7, 1994, Paris, France

		SUBMISSION DEADLINE: December 13, 1993

10 hard copies of a detailed abstract (not a full paper) and 20
additional copies of the cover page should be received by December 13,
1993 by the program chair.  This is a FIRM DEADLINE: late submissions
will not be considered.

Program Chair: Samson Abramsky, Attn: LICS, Department of Computing,
Imperial College of Science, Technology and Medicine, 180 Queen's Gate,
London SW7 2BZ, United Kingdom,	sa@...,
Phone: (010-44) 71-589-5111 ext. 5005, Fax: (010-44) 71-581-8024

The full announcement can be obtained by anonymous ftp from
research.att.com, directory /dist/lics, or by emailing
lics-request@...
Permalink | Reply | 0 comments |
headers
Allen Stoughton | 8 Dec 1993 18:35
Favicon

Announcement of MFPS X


[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.]

                           Workshop Announcement

                                  MFPS X 

                        The Tenth Workshop on the 
              Mathematical Foundations of Programming Semantics 

                             March 20 - 23, 1994 
                             Manhattan, KS, USA 

The Tenth Workshop on the Mathematical Foundations of Programming Semantics
will be held at Kansas State University, Manhattan, KS, USA from March 20 to
March 23, 1994.  The workshop will consist of six one-hour invited talks and
talks contributed by participants.  There also will be a Special Session on
Tools for Semantic Analysis, as well as a Special Session on the language ML.
The MFPS workshops are devoted to those areas of mathematics, logic and
computer science which are related to the semantics of programming languages.
The series has particularly stressed providing a forum where both
mathematicians and computer scientists can meet and exchange ideas about
problems of common interest.  We also welcome submissions by researchers in
neighboring areas, since we have attempted to maintain some breadth in the
scope of the series.

The invited speakers for MFPS X are:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andrew Pitts | 9 Dec 1993 16:04
Picon
Picon
Favicon

paper available


The following is an advert for a tech report which is an expanded of my LICS'93
paper on relational properties of recursively defined domains. It is somewhat
different in emphasis and broader in scope than the LICS paper. It also has a
shorter title! 

It is available by anonymous ftp from
theory.doc.ic.ac.uk as papers/Pitts/rpd.{dvi,ps}.Z

or from ftp.cl.cam.ac.uk as 
reports/TR321-ap-relational-properties-of-domains.ps.gz

Andy Pitts

-------------------
Relational Properties of Domains
Andrew M. Pitts 
Univ. Cambridge Computer Laboratory 
TR No. 321, December 1993, 37pp

  New tools are presented for reasoning about properties of
  recursively defined domains. We work within a general,
  category-theoretic framework for various notions of `relation' on
  domains and for actions of domain constructors on relations.
  Freyd's analysis of recursive types in terms of a property of mixed
  initiality/finality is transferred to a corresponding property of
  "invariant" relations. The existence of invariant relations is
  proved under completeness assumptions about the notion of relation.
  We show how this leads to simpler proofs of the computational
  adequacy of denotational semantics for functional programming
(Continue reading)

Permalink | Reply | 0 comments |
headers
David M. Jones | 10 Dec 1993 21:51
Picon

TACS '94: Final program and registration form


[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.]

                       PROGRAM AND REGISTRATION

                      International Symposium on
               Theoretical Aspects of Computer Software
                              (TACS'94)

                          April 19-22, 1994
                   Tohoku University, Sendai, Japan

                                   
                             Sponsored by
                      Tohoku University, Sendai

                       in cooperation with the

               Information Processing Society of Japan,
          Japan Society for Software Science and Technology,
                   Association for Symbolic Logic,
           IEEETC on Mathematical Foundations of Computing,
           and Association for Computing Machinery--SIGACT

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

                      International Symposium on
(Continue reading)

Permalink | Reply | 0 comments |
headers
Zuber | 11 Dec 1993 18:32
Picon

Question on coherence semantics


Can anybody tell me something about applications of the coherent space semantics
of (e.g. classical first order) linear logic? (e.g. independence results for LL)

Wolfgang Zuber
Permalink | Reply | 0 comments |
headers
Simon L Peyton Jones | 14 Dec 1993 10:11
Picon
Picon
Favicon

State in functional languages


The following four related papers, all on the topic of mutable state in
non-strict functional languages, are available by FTP.  The first two are as
yet unpublised; the last two are published.  

I'm posting this to the types mailing list as well as the functional
programming ones because there is an interesting use of rank-2 polymorphism
to ensure safe encapsulation of state; this shows up mainly in the
first-mentioned paper.  The other point of interest from a typing point of
view is that the usual unfortunate interaction of polymorphism with
assignment doesn't occur (see the last-mentioned paper)

All can be got from the FTP site ftp.dcs.glasgow.ac.uk.

Simon

		Lazy Functional State Threads
	J Launchbury and SL Peyton Jones, Glassgow University

	FTP: pub/glasgow-fp/drafts/state.ps.Z

Some algorithms make critical internal use of updatable state, even
though their external specification is purely functional.  Based on
earlier work on monads, we present a way of securely encapsulating
such stateful computations, in the context of a non-strict,
purely-functional language.  

There are two main new developments in this paper.  First, we show how
to use the type system to securely encapsulate stateful computations,
including ones which manipulate multiple, named, mutable objects.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Simon L Peyton Jones | 14 Dec 1993 10:11
Picon
Picon
Favicon

State in functional languages


The following four related papers, all on the topic of mutable state in
non-strict functional languages, are available by FTP.  The first two are as
yet unpublised; the last two are published.  

I'm posting this to the types mailing list as well as the functional
programming ones because there is an interesting use of rank-2 polymorphism
to ensure safe encapsulation of state; this shows up mainly in the
first-mentioned paper.  The other point of interest from a typing point of
view is that the usual unfortunate interaction of polymorphism with
assignment doesn't occur (see the last-mentioned paper)

All can be got from the FTP site ftp.dcs.glasgow.ac.uk.

Simon

		Lazy Functional State Threads
	J Launchbury and SL Peyton Jones, Glassgow University

	FTP: pub/glasgow-fp/drafts/state.ps.Z

Some algorithms make critical internal use of updatable state, even
though their external specification is purely functional.  Based on
earlier work on monads, we present a way of securely encapsulating
such stateful computations, in the context of a non-strict,
purely-functional language.  

There are two main new developments in this paper.  First, we show how
to use the type system to securely encapsulate stateful computations,
including ones which manipulate multiple, named, mutable objects.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Zuber | 11 Dec 1993 18:32
Picon

Question on coherence semantics

Can anybody tell me something about applications of the coherent space semantics
of (e.g. classical first order) linear logic? (e.g. independence results for LL)

Wolfgang Zuber
Permalink | Reply | 0 comments |
headers
gdp | 15 Dec 1993 18:51
Picon

EUROFOCS Advert


                          EUROFOCS
European Institute in the Logical Foundations of Computer Science
                     Fellowship Programme

         (Closing date for applications - 5th January 1994)

The European Institute in the Logical Foundations of Computer Science 
invites applications for PostDoctoral Fellowships. These can be held for 
periods ranging from six months to one year. The goal of the work in the 
Institute is to achieve a unified and applicable theory of the semantics 
and logic of languages used to describe, design and program computing 
systems. The research of the Insititute is characterised by a unified 
approach to foundational problems that emphasises the combination of ideas 
arising in design and practice with ideas originating in logic and allied 
mathematical areas. The applicability of the ideas developed is 
demonstrated by producing experimental systems for specification, 
verification and development. 

The research has both national and EC support, with involvement in several 
ESPRIT Basic Research Actions, including CONFER, CONCUR, COMPASS, 
Categorical Logic in Computer Science and Types for Proofs and Programs. 
Research Topics of Interest include: Semantics of Programming Languages; 
Logic Programming Theory; Object-Oriented Programming; Functional 
Programming Theory; Lambda-Calculus; Formal Development of Programs and 
Systems; Concurrency Theory. 

The Institute sites and contact points are: 

CWI, Amsterdam
(Continue reading)

Permalink | Reply | 0 comments |

Gmane