1 Aug 05:53 1996

### First Workshop on FP in Argentina: IMPORTANT CHANGES


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

This is a very short post. Please, excuse me if it is duplicated.
----------

1st Workshop of Functional Programming
September 12 of 1996, Buenos Aires, Argentina

The Organizing Committee have changed workshop's date to September 12 of
1996. You can find updated information (invited talks, acepted papers, ftp
server to available papers, etc) from these following WWW page:
http://www-lifia.info.unlp.edu.ar/ingles/jaiio-fp.htm

Roman Garcia
LIFIA. Universidad Nacional de La Plata.
Tel/Fax : +54  (21) 22- 8252
e-mail: roman@...


2 Aug 11:43 1996


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

The following job advert might be of interest to people on this list.
I'm not completely selfless posting this -- I'll be joining the
faculty of uni SA and am looking for like-minded people. I hope that
with so many new openings we can get a strong group going.

If you want to find out more about the announced positions, I'd be
happy to tell you what I know. But hurry, deadline for applications is
August 16th.

Cheers

-- Martin Odersky

> From roddick@... Mon Jul 22 19:14:56 1996
> Date: Mon, 22 Jul 1996 18:49:27 +1030
> To: it-announce@...
> From: roddick@... (John Roddick)
> Subject: Lecturer Positions at U-SA

University of South Australia
School of Computer and Information Science

Lecturer Level B (3 positions)
Tenurable / 5 year contract
$43,042-$51,113 per annum

WOMEN ARE ENCOURAGED TO APPLY


6 Aug 21:28 1996

### Logic/Semantics Tools from Kansas State University


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

Logic/Semantics Tools from Kansas State University

******************************************************************************

Version 1.0 of Porgi, a Proof-Or-Refutation Generator for
Intuitionistic propositional logic, is now available.

Given a sequent Gamma |- phi, Porgi either finds a minimally sized,
normal natural deduction of phi from the assumptions in Gamma, or it
finds a finite, tree-based Kripke model whose root node forces all of
the formulas in Gamma but does not force phi.  Although an attempt is
made to minimize the size of the Kripke countermodels, such
countermodels are not always minimally sized.  On the other hand:

(a) Classical models are produced whenever possible.  Thus, if a
model with more than one node is produced, one can conclude that
the sequent is provable classically.

(b) In Porgi's countermodels, child nodes always force strictly more
subformulas of the formulas of the sequent than do their parents.

(c) In one of Porgi's countermodels, all nodes other than the root
node force the formula phi.

Porgi can also handle minimal logic, is capable of generating typed
lambda terms instead of natural deductions, and can display the
subformulas of a sequent that are forced at each node of a Kripke


6 Aug 23:14 1996

### Fool workshop: 2nd call for papers / 2me appel aux communications


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

[Moderator's note:  It is becoming more and more common to
distribute more than one call for papers.  I generally refuse
a second call if it is too close to the first call, but haven't
yet devised a hard and fast rule.  Should I pass all calls in
the subject area of the Types Forum, refuse to pass any second
call, or do something in between?  I'll post a summary of replies.

Second 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.



7 Aug 11:46 1996

### Faculty Position


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

University of Sussex

School of Cognitive and Computing Sciences

LECTURER IN COMPUTER SCIENCE

Applications are invited for a Lectureship in the Computer
Science & A.I. group.
The person appointed would ideally take up the post from 1 January 1997;
a later start may be possible by negotiation.

Candidates should be able to show evidence of serious research achievement
in Foundations of Computation, preferably in an area close to the
research interests of Professor Hennessy and Dr Jeffrey, and should be
willing to teach in areas other than their research speciality.

The post can be discussed informally with Professor Hennessy,
matthewh@..., tel. 01273 678101.

The appointment will be made on the Lecturer A scale,
for which salaries run from #15,154 to #19,848 p.a.

Application forms and further particulars of this post are available
from

Sandra Jenks
Staffing Services Office


8 Aug 14:34 1996

### Minimal Typings in Atomic Subtyping


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

This is to inform the Types Forum that I have written a
technical report "Minimal Typings in Atomic Subtyping",
which is available from my homepage (and by ftp from DIKU.)

We prove that systems of atomic subtyping have
logically most succinct typings, and we use this result to
prove an exponential lower bound on the dag-size of coercion
sets as well as of types in most general typings, relative to
the notion of "lazy instance" defined by Fuh and Mishra.

The report can be obtained from
http://www.diku.dk/research-groups/topps/
personal/rehof/publications.html
and also by ftp
<ftp://ftp.diku.dk/diku/semantics/papers/D-278.ps.gz>

A summary of the report has been submitted for publication.

The abstract follows:

----------------------------------------------------------
We study the problem of simplifying typings
and the size-complexity of most general typings in
typed programming languages with subtyping. We define a notion
of minimal typings relating all typings which are
equivalent with respect to instantiation.
The notion of instance is that of Fuh and Mishra


7 Aug 21:31 1996

### Research Fellowship


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

Department of Computer Science
University of Durham

Research Fellowship

Applications are invited for a two-year research fellowship in the
above department, funded under the research project

"Computer-assisted reasoning with natural language:
implementing a mathematical vernacular".

The project is to study and develop a theory and the associated
techniques based on type theory for implementing proof systems that
assist mathematicians to reason in their own mathematical vernacular,
that is, a mathematical and natural language suitable for ordinary
mathematical practice and implementable based on a formal theory.

The research fellowship is for a period of two years and available
from October 1996.  The appointment will be on the AR1A scale
(starting salary up to 16,628 pounds per annum, according to
experience).  Candidates would normally be expected to have a PhD or
equivalent experience in computer science, computational linguistics,
or mathematics.  Experience or background in areas such as typed
lambda calculi, functional programming, computational linguistics, or
formal proof systems based on type theory, is considered to be
desirable, though not necessary.



8 Aug 20:46 1996

### Tech. Rep. on specialization inheritance and lambda-&-calculus


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

Hallo,
this is to let you know that I have made available,
via either ftp or web the following technical report

--------------------------------------------------------------
Title: $\lambda$\&ESI-Calculus for Enhanced Strict Inheritance

Authors: P. Di Blasio, M. Temperini

Keywords: specialization, covariance, method lookup
Abstract:

We present a specialization inheritance mechanism for a
strongly typed object-oriented language, called "Enhanced
Strict Inheritance" (ESI).
It is a mechanism of classification in which the subclassing
relation between classes reflects the subtyping relationship
between the corresponding types.
The definition of ESI is based on a covariant redefinition rule
for methods.
ESI is modeled via the lambda&ESI-calculus, a modification
of the lambda&-calculus of overloaded functions due to
Castagna, Ghelli and Longo.
In ESI hierarchies the only constraint to attribute redefinition
is covariance; any other restriction in redefinition rule and
compatibility of result types in confusable methods is relaxed.


13 Aug 19:58 1996

### research post at Kent


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

University of Kent at Canterbury

Computing Laboratory

Postdoctoral Research Post in Computer Science

Applications are invited for the above post, funded  by  the  EPSRC,  to
work  with Professor D A Turner on a project entitled "Elementary Strong
Functional Programming". The  aim  of  the  project  is  to  investigate
disciplines of functional programming which ensure termination.

Applicants should have a doctorate in Computer Science  or  Mathematics,
or   an   equivalent  publication  record,  and  research  interests  in
functional programming  and/or  mathematical  logic.   Experience  of  a
strongly  typed  lazy  functional  language, such as Miranda or Haskell,
will be an advantage.  The post is for a three year fixed  term  from  1
October 1996.

Salary on the  1A  Research  scale  14,317  -  19,848  pounds.   Further
particulars are available from

The Personnel Office,
The Registry,
The University,
Canterbury,
Kent, CT2 7NZ.



13 Aug 19:58 1996

### Kanellakis Award


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

Kanellakis Theory and Practice Award

The Kanellakis Theory and Practice Award is given to an individual or
group for a specific theoretical accomplishment that has had a
significant and demonstrable effect on the practice of computing.  The
nature of the theoretical accomplishment may be either an invention
itself or a major analytic study of an existing technique that led

The Award has been established in memory of the late Paris C. Kanellakis,
whose tragic death in late 1995 cut short a distinguished
research career.  The monetary amount of the award will be \$5,000, to
be paid from an endowment established for this purpose.  The frequency
of the award will depend on the size of the endowment, but should be at
least once every three years.  The first award will be made in 1997.

Winners of the award will be chosen by a 5-member committee appointed
by the ACM Awards Committee Chair.  Membership on the committee will be
on a rotating basis, with 5-year terms.  The current committee consists
of David Johnson, Tom Leighton, Christos Papadimitriou, Moshe Vardi,
and Peter Wegner (Chair).  The committee will actively solicit
nominations from the research and practitioner communities, as well as
outside advice on questions of practical and theoretical significance
and of priority.  Nominations from previous years will typically be
carried forward.  The committee also reserves the right to make its own
nominations.  Winners will be selected based on both the importance of
the practical impact and the quality of the theoretical