Roman Garcia | 1 Aug 05:53 1996

First Workshop on FP in Argentina: IMPORTANT CHANGES

[------ The Types Forum ------- ------]

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:

For questions or more information, contact:
        Roman Garcia
        LIFIA. Universidad Nacional de La Plata.
        Tel/Fax : +54  (21) 22- 8252
        e-mail: roman@...

Martin Odersky | 2 Aug 11:43 1996

Job advert: 3 Lecturer B Positions in Adelaide, Australia

[------ The Types Forum ------- ------]

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.


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

(Continue reading)

Allen Stoughton | 6 Aug 21:28 1996

Logic/Semantics Tools from Kansas State University

[------ The Types Forum ------- ------]

          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
(Continue reading)

Benjamin C. Pierce | 6 Aug 23:14 1996

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

[------ The Types Forum ------- ------]

[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.
-- Philip Wadler, moderator, Types Forum (wadler@...)]

                      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.

(Continue reading)

Matthew Hennessy | 7 Aug 11:46 1996

Faculty Position

[------ The Types Forum ------- ------]

University of Sussex

School of Cognitive and Computing Sciences


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

Sandra Jenks
Staffing Services Office
(Continue reading)

Jakob Rehof | 8 Aug 14:34 1996

Minimal Typings in Atomic Subtyping

[------ The Types Forum ------- ------]

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 
and also by ftp 

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
(Continue reading)

Zhaohui.Luo | 7 Aug 21:31 1996

Research Fellowship

[------ The Types Forum ------- ------]

		    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.

(Continue reading)

Marco Temperini | 8 Aug 20:46 1996

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

[------ The Types Forum ------- ------]

this is to let you know that I have made available, 
via either ftp or web the following technical report
(about which I'll be very happy to receive comments and criticisms)

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

Authors: P. Di Blasio, M. Temperini

Keywords: specialization, covariance, method lookup

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. 
(Continue reading)

dat | 13 Aug 19:58 1996

research post at Kent

[------ The Types Forum ------- ------]

                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,
  Kent, CT2 7NZ.

(Continue reading)

Moshe Vardi | 13 Aug 19:58 1996

Kanellakis Award

[------ The Types Forum ------- ------]

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
practitioners to adopt it.

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
(Continue reading)