Peter D. Mosses | 1 Sep 11:26 1994

CFP: TAPSOFT'95 (short reminder)

[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

[The full CFP was sent previously to the same mailing list,   22 June 1994.]

CALL FOR PAPERS                                              CALL FOR PAPERS
22--26 MAY 1995                                              AARHUS, DENMARK

>>>>>>>>>>>>>>>>> DEADLINE FOR SUBMISSION: 15 OCTOBER 1994 <<<<<<<<<<<<<<<<<

TAPSOFT'95 is  the Sixth  International Joint Conference  on the  Theory and
Practice of  Software Development.   It  will be held  at the  University of
Aarhus, Denmark.   TAPSOFT is traditionally divided into three sections:

     CAAP:           Colloquium on Trees in Algebra and Programming
                     -- covering a wide range of topics in theoretical
                     computer science

     FASE:           Colloquium on Formal Approaches in Software Engineering
                     -- with the emphasis on practical applicability

     Invited talks:  on a variety of relevant topics.

TOOLS   In  recognition of  the importance  of support  tools for  practical 
use of  formal  approaches, TAPSOFT'95  will also have a session where tools  
are demonstrated.


(Continue reading)

Philipp Suenderhauf | 2 Sep 13:54 1994

Thesis: Discrete Approximation of Spaces

My thesis "Discrete Approximation of Spaces" is now available by
anonymous ftp from the site as file
in the directory /papers/Suenderhauf/.

In denotational semantics of higher programming languages, abstract
data types are represented by certain mathematical objects, the {\em
semantic domains.\/} For discrete datatypes such as {\tt integer} or
{\tt boolean}, and for higher types derived from these employing the
function space and product type constructors, this works fine in the
setting of domain theory. But for the datatype {\tt real} there is no
satisfying approach so far. This problem of finding a semantic domain
for the reals comes hand in hand with the question how to implement
the real line in a computer. This thesis gives an approach to solve
these problems.

The thesis may be divided into two parts. One part is concerned with
the problem of finding a good computational model of the real numbers,
the other part extends this construction to a fairly general class of
spaces and handles the type constructors `product' and `function

The computational model of the reals has the following salient
features. It is a countably based quasicontinuous domain which
contains a homeomorphic copy of the usual real line as its maximal
elements. The remaining elements are the {\em partial elements.\/}
They can be stratified into certain {\em levels of totality\/} each of
which can be seen as a discrete approximation of the real line. The
whole domain is constructed as a subspace of the upper power space of
(Continue reading)

Horst Reichel | 7 Sep 07:38 1994


[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

                 Fundamentals of Computation Theory, FCT'95

                    Dresden, Germany, August 22--25, 1995

(LaTeX and other versions of this Call for Papers are available by anonymous
ftp at URL:,.tex,.dvi,.ps)

   The conference is the tenth in the series of FCT conferences
organized every odd year. The papers selected by the Program Committee
are expected to to contribute to the following topics: Algorithms and
data structures, Automata and formal languages, Categories and types,
Computability and complexity, Computational logics, Computational
geometry, Foundations of system specifications, Learning theory,
Parallelism and concurrency, Rewriting and high-level replacement
systems, Semantics.

   In addition to three days of invited and selected lectures there
will be a one-day MINISYMPOSIUM at the end of FCT'95 dealing with

                     Specification of time-critical systems

with following invited speakers (Preliminary List): M.Abadi (DEC,
USA), J.Bergstra (Amsterdam), M.Broy (Munich), Z.Chaochen (Macau).

   Conference Chairman: Horst Reichel (Dresden).
   Program Committee: J. Balcazar (Barcelona), R.G. Bukharajev (Kazan),
(Continue reading)

Michael Main | 8 Sep 20:27 1994

MFPS Call for Papers

[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

                              Call for Papers 

                                  MFPS XI

                       The Eleventh Conference on the 
              Mathematical Foundations of Programming Semantics 

                           March 29 - April 1, 1995 
                          New Orleans, Louisiana USA 

The Eleventh Conference on the Mathematical Foundations of Programming 
Semantics will be held at Tulane University, New Orleans, LA USA from March 29
to April 1, 1995. The conference will consist of six one-hour invited talks
and of talks selected from submissions. There also will be a special session
on the Semantics of Object-Oriented Languages. The MFPS conferences
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
strive to maintain breadth in the scope of the series. 

The invited speakers for MFPS XI are: 

 Andreas Blass (Michigan)              Robin Milner (Edinburgh)
 Edmund Clarke (CMU)                   John Reynolds (CMU)
 Neil Jones (Copenhagen)               Robert Tennent (Queen's, Kingston)
(Continue reading)

Jan Herman Geuvers | 8 Sep 14:46 1994

SYMPOSIUM `The Influence of Automath'

[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

################### Second Announcement #############################



		The Influence of Automath

Eindhoven University of Technology (Netherlands) October 6, 1994

At the occasion of the publication of the book

		'Selected Papers on Automath' 

(Studies in Logic and the Foundations of Mathematics, North-Holland, 
eds. R.P. Nederpelt, J.H. Geuvers and R.C. de Vrijer), there will be 
a symposium at the Van Trierzaal, Bestuursgebouw, Eindhoven University
of Technology, on October 6, 1994.

The program of the symposium is as follows:

11.00 -- 12.00	H.P. Barendregt (University of Nijmegen, CWI Amsterdam):
		'Two level reasoning for lean proof checking' 
12.00 -- 13.30 	lunch break 
13.30 -- 14.30 	G. Huet (INRIA Paris): 'Proof engine design' 
14.30 -- 15.00 	tea break 
15.00 -- 16.00 	R.L. Constable (Cornell University): 'The influence of 
(Continue reading)

Serge Vorobyov | 10 Sep 11:44 1994

Extensions of Fsub with Decidable Typing

Dear Phil,

I'd greatly appeciate it if you would announce the following paper.



The following paper

	Extensions of Fsub with Decidable Typing

		    by Sergei Vorobyov

is now available by anonymous ftp.

FTP instructions:

    login: anonymous
    password: <your mail address>
    cd pub/loria/prograis/vorobyov
    get FsubDecTyping.dvi.Z  (or


(Continue reading)

Healfdene Goguen | 12 Sep 14:58 1994

A Typed Operational Semantics for Type Theory

I would like to announce that my thesis, entitled ``A Typed
Operational Semantics for Type Theory,'' is available
electronically and will be available soon as an LFCS report.
The addresses for accessing it are enclosed at the end of
this message.

Healfdene Goguen


A Typed Operational Semantics for Type Theory

Untyped reduction provides a natural operational semantics for
type theory.  Normalization results say that such a semantics
is sound.  However, this reduction does not take type information
into account and gives no information about canonical forms for terms.
We introduce a new operational semantics, which we call typed
operational semantics, which defines a reduction to normal form
for terms which are well-typed in the type theory.

The central result of the thesis is soundness of the typed operational
semantics for the original system.  Completeness of the semantics is
straightforward.  We demonstrate that this equivalence between the
declarative and operational presentations of type theory has important
metatheoretic consequences:  results such as strengthening, subject
reduction and strong normalization follow by straightforward induction
on derivations in the new system.

We introduce these ideas in the setting of the simply typed lambda
(Continue reading)

Jean-Yves GIRARD | 13 Sep 14:17 1994

Re: Exponentials in linear logic

Answer to Clemens H. CAP (mail of August 1st)

The question of duality of ! and ? is exactly the same as the  
question of the unicity of !. By nature ! cannot be unique :

1st reason : ! controls infinity in logic ; we get usual infinity by  
means of the familiar rules, but another choice of rules can yield  
weaker notions of infinity, eg polytime. In this respect, there is no  
a priori unicity of !, and this is far from being a weakness...

2nd reason : just write twice the same set of rules (eg in an  
intuitionistic style) for ! and -say- $ ; it will be impossible to  
prove the equivalence between !A and $A. If we want to prove $A -o !A  
then we must allow contexts $Gamma,!Delta in the !S-rule. In general  
we can handle several !, partially ordered, etc. But one should use  
this latter possibility with extreme care : multimodal logics are  
close relatives of non-monotonic "logics". 


Jean-Yves GIRARD
Directeur de Recherche

CNRS, Laboratoire de Mathematiques Discretes
163 Avenue de Luminy, case 930
13288 Marseille cedex 9

(33) 91 82 70 25
(Continue reading)

Andrew Wright | 14 Sep 15:43 1994

Practical Soft Typing

I would like to announce the completion of my dissertation at Rice
University titled Practical Soft Typing.  The thesis is available
by ftp from in public/languages/

The abstract follows:

Soft typing is an approach to type checking for dynamically typed
languages.  Like a static type checker, a soft type checker infers
syntactic types for identifiers and expressions.  But rather than
reject programs containing untypable fragments, a soft type checker
inserts explicit run-time checks to ensure safe execution.

Soft typing was first introduced in an idealized form by Cartwright
and Fagan.  This thesis investigates the issues involved in designing
a practical soft type system.  A soft type system for a purely
functional, call-by-value language is developed by extending the
Hindley-Milner polymorphic type system with recursive types and
limited forms of union types.  The extension adapts Remy's encoding of
record types with subtyping to union types.  The encoding yields more
compact types and permits more efficient type inference than
Cartwright and Fagan's early technique.  Correctness proofs are
developed by employing a new syntactic approach to type soundness.  As
the type inference algorithm yields complex internal types that are
difficult for programmers to understand, a more familiar language of
presentation types is developed along with translations between
internal and presentation types.  To address realistic programming
languages like Scheme, the soft type system is extended to incorporate
assignment, continuations, pattern matching, data definition, records,
modules, explicit type annotations, and macros.  Imperative features
(Continue reading)

Uday S. Reddy | 15 Sep 07:07 1994

Final CFP: State in Programming Languages

[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

                         Call for Papers

	        The Second ACM SIGPLAN Workshop on 
	       STATE in Programming Languages (SIPL)

                            Jan 22, 1995
                           San Francisco
                  Held in conjunction with POPL '95

Programming languages have been state-based since their inception.
After a period of relative unpopularity, when research focused on
declarative languages, interest in the treatment of state has been
renewed.  Research is increasingly devoted to finding a symbiotic
relationship between the semantic foundations of declarative languages
and the pragmatic handling of state in more conventional languages.
This workshop brings together researchers from various areas,
interested in the common issues of state manipulation in high-level
programming languages.

The first workshop in this series (SIPL '93) was held in Copenhagen in
conjunction with FPCA '93.  The proceedings are available as a Yale
technical report YALEU/DCS/RR-968.  A special issue of the Journal of
Lisp and Symbolic Computation is being published as a follow-up to 
SIPL '93. 

Submissions are invited for the second workshop to be held in
(Continue reading)