Matthew Hennessy | 3 Jul 15:55 1995

Research positions at Sussex

                       UNIVERSITY OF SUSSEX


Two Research Fellows are required for a 3-year project entitled
``Foundations for the Integration of Concurrent Distributed and
Functional Computation'', under the direction of Prof. M. Hennessy and
funded by the EPSRC.

The aim of the project is to 

- provide a uniform coherent semantic foundation for concurrent,
distributed and functional behaviour;

- develop proof methodologies for establishing properties of process
descriptions expressed in specification languages using these

- develop prototypes of supporting verification systems.

The project will start on 1/10/95 and salary will be related to the
academic 1A scale. A Ph.D. in Computer Science or Mathematics or
equivalent experience is required. In addition to normal research
duties the successful candidate will be expected to provide some 
assistance to undergraduate teaching.

More details of the project and the conditions of service are available

(Continue reading)

Coq Team | 4 Jul 15:32 1995

Coq V5.10 Release

                  Coq V5.10 Release

This is the announcement for the release of the Coq Proof Assistant,
Version 5.10.

It may be taken as usual from machine, directory
INRIA/coq/V5.10, archive V5.10.tar.z and README file.

For users who are already using one of the beta-test versions of V5.10,
this final release has improved documentation, streamlining of tactics
(Some adaptation of your scripts may be necessary because the names
of inversion tactics have changed), and compressed theory files (.vo)
which keep the size of the installation much smaller and are uniform
across architectures. This substantial improvement necessitates
however the installation of the latest release of Caml Light; see
WARNING below. 

For users who are still using our old release V5.8, it is high time to
switch to this new system, which has been completely rebuilt, 
authorizes mutually recursive inductive families, compiled theory
modules, extensible parsers and pretty-printers, user-programmable
tactics, synthesis of implicit type arguments, and many other goodies.
The distribution also includes numerous new user-contributed

The current release works under most modern UNIX platforms.
A specialised interface with the Centaur environment, called CTCoq, is
under completion in Sophia-Antipolis and should be available soon
in beta-test. 
(Continue reading)

Max KANOVITCH | 3 Jul 14:09 1995

Second order Lambek is undecidable

 Undecidability of the Second Order Lambek Calculus

                    Max Kanovich

 In my previous message on the undecidability of non-commutative
 second order multiplicative linear logic the problem whether the
 second order Lambek calculus is decidable remained open.
 The point is that the Lambek calculus does not allow sequents with
 the empty antecedent, and, in particular, we meet problems with 1
 and Weakening.

 Nevertheless, we can improve constructions from my previous message
 to get also the undecidability for the second order Lambek calculus.

 Let "\" and "/" stand for left and right implications, respectively,
     "*" for non-commutative product.

 We define a 'self-reproductive' formula R as follows:

  R = forall C,A,T ( (C *  <at> C *  <at> A * T * A)/( <at> C *  <at> A * T) )

        <at> B = ( (f/(f*B)) * B)     (f is a fixed atom)

 Minsky machines with two counters x and y are simulated in the
 second order Lambek calculus as follows:

 Any configuration of a given Minsky machine M
(Continue reading)

Rosemary Soutar | 5 Jul 13:32 1995

Lectureships in Computer Science



Applications are invited for three Lectureships in Computer
Science available from October 1995, or as soon as possible thereafter.
One post is available for three years and the others for five years,
in the first instance. There is the possibility of a permanent
contract for an exceptionally well qualified candidate.

Applicants should be qualified to Ph.D. level and should be able to
teach across a range of topics and levels (including first-year)
within the subject. Successful candidates will have an excellent
research record. One post has been created in connection with the
recent appointment of Professor Samson Abramsky to a newly established
Chair in Theoretical Computer Science; for the second post, the
Department is anxious to strengthen its teaching in parallel and
distributed systems; the third is open to candidates well qualified in
teaching and research in any area of Computer Science.

Salary on the scale 15,154-19,848 pounds p.a. with placement according
to age, qualifications and experience.

Further particulars including details of the application procedure may
be obtained from our world-wide-web page or
from the Personnel Office, 1 Roxburgh Street, Edinburgh EH8 9TB or Tel
: 0131 650 2511 (24 hour answering service).  Please quote reference
xxxxxxxx.  Closing date for applications is Monday 31st July 1995.

(Continue reading)

Roy L. Crole | 10 Jul 18:24 1995

Chair in Computer Science



Chair in Computer Science

Applications are invited for a new Chair in Computer Science in the
Department of Mathematics and Computer Science, tenable from l January
1996, or as soon as possible thereafter. The creation of the chair
will consolidate and extend the work of the Computer Science Group
within the Department.  Applicants should have strong research records
in Computer Science, and be able to provide academic leadership to the
Computer Science Group.  The Department would particularly welcome
applications from people working in applicable areas of Computer
Science which would complement the existing research areas, while
making use of the expertise already available.  In addition to this
appointment, it has been agreed that a Lectureship in Computer Science
will subsequently be advertised, and the appointee should expect to
play a major role in the filling of this position.

Salary will be within the Professorial Range.

Informal enquiries are welcome and should be addressed to Professor
Will Light, Head of Department, telephone +44 (0)116 252 3884, or
email jobs@...

Further particulars may be obtained from the

Staffing Office (Academic Appointments),
(Continue reading)

Peter Clote | 13 Jul 23:14 1995

university positions

The following is an announcement for 3 positions
in computer science at the University of Munich.

             S t e l l e n a n g e b o t

Am Gerhard-Gentzen-Lehrstuhl (Prof. Clote)
der Ludwig-Maximilians-Universit"at M"unchen ist die Stelle 
eines wissenschaftlichen Mitarbeiters C1 zu besetzen. 

Neben der Erledigung der "ublichen Lehraufgaben wird 
die Erstellung einer Promotion (3 Jahre) bzw. Habilitationsschrift
(5 Jahre) auf den folgenden Forschungsgebieten 

	(1) Komplexit"atstheorie (parallele Algorithmen,
        Boolische Funktionen, Typentheorie, Komplexit"at von Beweissystemen) 
	(2) Computational Molecular Biology


Bewerbungen an:

VOR dem 25. Juli 1995

   Prof. Peter Clote
   Department of Computer Science
   Boston College
   Chestnut Hill, MA 02167 USA
(Continue reading)

Alan Mycroft | 14 Jul 18:21 1995

SAS 95 Call for Participation

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

[Apologies to those who receive this by multiple routes]
Call for participation:
International Static Analysis Symposium (SAS'95)
Kelvin Conference Centre, Glasgow, 25--27 September 1995

The programme, call-for-participation and registration information are
available on
If requested I will mail out latex sources to people who cannot access
WWW documents.

I look forward to seeing many of you in Glasgow.
The list of papers to be presented is attached.

Alan Mycroft, SAS'95 PC chair.
Invited speakers, refereed papers and system descriptions for SAS'95

Invited speakers:

David Schmidt (Kansas State)
Natural-Semantics-Based Abstract Interpretation

(Continue reading)

Vaughan Pratt | 18 Jul 19:02 1995

Linear logic in mathematical practice

I am looking for papers addressing the role of linear logic in
mathematical practice.  Of particular interest would be extracts from
the mathematical literature illustrating either the actual use of
linear logic or the improvement possible with linear logic.
Assessments of the benefits of linear logic for working mathematicians
would also be of interest.

Vaughan Pratt

J.A.Bayfield | 19 Jul 11:31 1995

Post for Research Fellow

This job advert has to go to the types mailing list. I believe
the way to do this is to post it to you. Thankyou.

     Computing Laboratory, University of Kent at Canterbury

Applications are invited for a post of Research Fellow available
immediately in the Computer Science Department, to work in
conjunction with the theoretical computer science group for a period
of up to three years in the first instance. Applicants should have a
doctorate in Computer Science (or equivalent publication record) and
research interests in one of the following areas   functional
programming, theoretical computer science, formal methods, computer
based theorem proving.

Salary on the Research scale 14,317-21,519 pounds. Further particulars are
available from The Personnel Office, The Registry, The University,
Canterbury, Kent, CT2 7NZ. Telephone (01227) 764000 ext. 3674 or
(01227) 475482 (24 hour answerphone) or email request to
M.A.Knapp@... Please quote reference number A95/115. 

Information about the posts and department is at URL:

Closing date: Friday 4 August 1995

The University is committed to implementing its Equal Opportunities

(Continue reading)

simonpj | 21 Jul 00:36 1995

Static Analysis Symposium '95

	International Static Analysis Symposium (SAS'95)
		Kelvin Conference Centre, Glasgow, 

		25--27 September 1995
		Second call for participation 

[This is the second announcement of this conference; this
version includes registration information at the end.]

Static Analysis is increasingly recognised as a fundamental tool for
high performance implementations and verification systems of
high-level programming languages. The last two decades have witnessed
substantial developments in this area, ranging from theoretical
frameworks to the design and implementation of analysers and their
application in optimising compilers.

The Second International Static Analysis Symposium takes place in
Glasgow, UK, from 25--27 September 1995. It follows the First
International Static Analysis Symposium in Namur (Belgium) and the
three previous international workshops Jtaspefl and WSA'92, which were
held in Bordeaux (France), and WSA'93 which took place in Padova

The aim of SAS'95 is to promote contacts and information exchange
among scientists who share common interests in static analysis for
different programming paradigms.  Researchers from the fields of
concurrent, constraint, functional, imperative, logic and
object-oriented programming constitute the audience of SAS.
(Continue reading)