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
TAPSOFT'95
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.

INVITED SPEAKERS



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 theory.doc.ic.ac.uk as file discrete.ps.Z
in the directory /papers/Suenderhauf/.

ABSTRACT.
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
space'.

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


7 Sep 07:38 1994

### FCT'95


[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: ftp://ithif10.inf.tu-dresden.de/fct95/fctcall.txt,.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),


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)


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 #############################

CALL FOR PARTICIPATION

SYMPOSIUM

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


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.

Sincerely,
Sergei

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

The following paper

Extensions of Fsub with Decidable Typing

by Sergei Vorobyov

is now available by anonymous ftp.

FTP instructions:

ftp ftp.loria.fr
cd pub/loria/prograis/vorobyov
binary
get FsubDecTyping.dvi.Z  (or FsubDecTyping.ps.Z)

MOSAIC:
ftp://ftp.loria.fr/pub/loria/prograis/vorobyov



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


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

<girard@...>
(33) 91 82 70 25


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 cs.rice.edu in public/languages/thesis-wright.ps.Z.

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


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
`