gmh | 2 Jun 16:49 2000

Four lectureships in Nottingham



	School of Computer Science and Information Technology

			  Four lectureships

Applications are  invited for the  above posts in a  rapidly expanding
School   based   at   one   of   the   UK's   strongest   research-led
universities. The School was graded  4 in the 1996 Research Assessment
Exercise and is  now building up its research  strengths for a further
improvement in  grade.  These posts are  part of a  steady increase in
the  size of the  School accompanied  by a  move to  new purpose-built
accommodation  in September 1999.  Although the  successful candidates
will have the opportunity of  teaching within their specialist area at
undergraduate and postgraduate level, there will also be a requirement
to teach  general computer science and  information technology modules
outside of any particular specialisation.

Candidates should already  have a PhD in computer  science, or another
closely related discipline, together  with strong evidence of existing
research  work  and the  potential  for  future  research at  Grade  5
level.  Outstanding  candidates will  be  welcomed  from  any area  of
computer science.

Salary will  be within  the range #17,238  - #30,065 per  annum (under
review), depending on qualifications and experience.

Informal enquiries  may be addressed to  Professor P H  Ford, tel: +44
(Continue reading)

Samson Abramsky | 2 Jun 19:39 2000

TLCA 2001

*                    TLCA 2001
*          5th International Conference on
*        Typed Lambda Calculi and Applications
*                 May 2 -- 5, 2001
*                  Krakow, Poland
*                 CALL FOR PAPERS

The TLCA series of conferences aims at providing a forum for the
presentation and discussion of current research in a field which was
originally rather restricted, but has now expanded considerably.
Typical areas include, but are not limited to:

Proof theory: 
Natural Deduction and Sequent Calculi, Cut elimination and
Normalization, Computational interpretations of Classical Logic, 
Linear Logic and Proof Nets, Bounded systems capturing complexity

Denotational semantics, Operational semantics, Game  semantics,
Realizability, Categorical models, Logical Relations, Full Completeness

Abstract machines, Parallel execution, Optimal Reduction
(Continue reading)

Yves Bertot | 5 Jun 15:54 2000

PhD grant at INRIA Sophia Antipolis

See the second part of this message for a translation in English.

  Bourse de doctorat à l'INRIA Sophia Antipolis
                Projet Lemme

le projet Lemme de l'INRIA Sophia Antipolis propose une bourse de
doctorat centrée sur les méthodes formelles basées sur Coq et sur la
description de langages de programmation adaptés aux cartes à puces.
Cette thèse s'intègrera dans le cadre d'une collaboration avec GemPlus,
entreprise à la pointe du développement des cartes à puces, Les
techniques étudiées devront permettre de développer des vérificateurs
de byte-code formellement certifiés pour des langages approximant le
langage JavaCard.  L'objectif à terme est de fournir un vérificateur
de byte-code entièrement prouvé correct pour le langage JavaCard tel
qu'il est défini par JavaSun.

L'étudiant travaillant avec cette bourse doctorale aura l'occasion
d'approfondir ses compétences dans un domaine à l'intersection des
domaines théoriques les plus ambitieux de la logique et de
l'informatique fondamentale et des champs d'applications les plus
dynamiques de l'évolution récente des technologies de l'information et 
de la communication (authentification, sécurité sur les réseaux,
commerce électronique...).

Les candidats intéressés devront envoyer un curriculum vitae et une
lettre de motivation à Yves Bertot (Yves.Bertot <at>

Liens utiles:
(Continue reading)

RFC Walters | 5 Jun 18:26 2000

CT 2000 Call for Posters


July 16-22, 2000
Centro di Cultura Scientifica "Alessandro Volta" di Villa Olmo
Como, Italy

The programme of talks for the conference is now available at the web page
for the conference

We are now calling for submissions to a Poster Session. Abstracts of the
posters will be collected with those of the talks in the form of a booklet
to be distributed at the conference.
Submissions for abstracts of posters should be made in the form of a
TeX/LaTeX file, and sent to ct2000 <at> The size limit is
10 pages. The DEADLINE for submission is 30th June 2000.

Accommodation in Como may be booked through the
Centro di Cultura Scientifica "A. Volta", Villa Olmo,
at the web page
The deadline for such a booking is 12th June 2000.

We are planning to publish proceedings of the conference in an international
journal. Details will appear shortly.
(Continue reading)

Peter Williams | 6 Jun 16:20 2000

Faculty post in foundations of computer science



Lecturer/Senior Lecturer in Foundations of Computer Science (Ref 358)

Applications are invited for a permanent faculty position within the
Subject Group of Computer Science and Artificial Intelligence. The
expected start date is 1 October 2000 or as soon thereafter as

The Subject Group currently has active research groups in the
Semantics of Computation and in Software Systems and Networks.
Candidates should be able to show evidence of significant research
achievement related to these research areas.  Ideally they should be
able to mediate between the two research groups, facilitating and
encouraging joint research activity.  Applicants with research
interests in programming language design for distributed systems, from
either a practical or theoretical perspective, would be particularly
welcome.  Details of the School of Cognitive and Computing Sciences
are available at

The post can be discussed informally with Professor Matthew Hennessy,
phone +44 1273 678101, email matthewh <at>

Salary will be in the range: £17,238 to £22,579 (Grade A) or £23,521
to £30,065 (Grade B) on the Lecturer scale, or £31,563 to £35,670 on
the Senior Lecturer scale.  The level of appointment will be
(Continue reading)

Etaps 2001 | 6 Jun 16:06 2000


                              ETAPS 2001
                          APRIL 2 - 6, 2001
                           GENOVA - ITALY

The European Joint Conferences on Theory and Practice of Software
(ETAPS) is a loose and open confederation of conferences and other
events that has become the primary European forum for academic and
industrial researchers working on topics relating to Software Science.


5 Conferences - Tutorials - Tool Demonstrations - 7 Satellite Events

CC 2001: International Conference on Compiler Construction
Chair: Reinhard Wilhelm

ESOP 2001, European Symposium On Programming
Chair: David Sands

FASE 2001, Fundamental Approaches to Software Engineering
Chair: Heinrich Hußmann

Foundations of Software Science and Computation Structures
(Continue reading)

Nuno Barreiro | 8 Jun 14:54 2000

LINEAR Summer School (Last call)

Please forward. We apologize for any duplication of this message in your
mailbox.                           Best regards,
                                                    Nuno Barreiro
=                              =                  =  Deadline for
applications:  =                  =                              =
                 =                              =
=           JUNE 15th          =
=                              =
================================              The LINEAR International
Summer School                  (Linear Logic and Applications)
                 August 30 to September 7, 2000         Hotel Terra
Nostra, S.Miguel, Azores, Portugal The Linear TMR research network
( is proud to announce its first
International Summer School on Linear  Logic and Applications. The
school is directed to everyone doing postgraduate work in  Computer
Science or Mathematics with an interest in the field  of Formal Logic
and its applications. The school lasts one week and comprises both
lectures and  thematic sessions. The lectures are in the tradition of
summer  schools and cover one topic, from basic material to more
advanced  issues. The topics and lecturers are the following:
Samson Abramsky --- Game Semantics       Jean-Yves Girard -- Linear
Logic and Ludics       Stefano Guerrini -- Proof-Nets and
Lambda-Calculus       Yves Lafont ------- Phase Semantics and Decision
Problems       Phil Scott -------- Category Theory and Concrete Models
The thematic sessions will cover state-of-the-art research in  Linear
Logic. Each session has an organiser responsible for  inviting speakers
who will talk about their work. The themes  and organisers are the
following:       Andrea Asperti ---- Applications       Vincent Danos
(Continue reading)

Pedro Manuel Resende | 8 Jun 19:12 2000

symmetric frame of a suplattice: question

The symmetric frame of a sup-lattice L is the frame freely generated by L
with sups being preserved in the presentation. Classically (ie, with the
truth value object being 2) it is easy to show that the injection of
generators is 1-1. Does anyone know whether this also holds in an
arbitrary topos?


Pedro Resende

Departamento de Matemática     Tel.:   +351 218 417 149
Instituto Superior Técnico     Fax:    +351 218 417 048 / 598
Av. Rovisco Pais               E-mail: pmr <at>
1049-001 Lisboa, Portugal      WWW:

Paul Taylor | 12 Jun 17:05 2000

lifting and non-Artin gluing

                     Non-Artin Gluing in Recursion Theory
                   and Lifting in the Abstract Stone Duality

                       for "Category Theory 2000", Como


    The analogy between `open' and `recursively enumerable' sets has long
    been a mainstay of theoretical computer science, but the traditional
    axiomatisation of general topology involving arbitrary unions is an
    obstacle to the formal unification of these disciplines.

    In particular, whilst Artin showed how to glue an open subspace
    to its closed complement using a comma square of frames, we give
    a diagonalisation argument to show that this representation fails for
    any recursively enumerable subset of $\mathbb N$ that is not decidable.

    Abstract Stone Duality is a re-axiomatisation based on the monadic
    adjunction between the dual categories of `frames' and `spaces'. Despite
    the failure of Artin gluing, we show in this formulation that the lift
    or scone, constructed using a comma square, still provides the classifier
    for partial maps with open domain of definition.  As the axiomatisation
    is not given in terms of finite intersections and arbitrary unions,
    a careful study of the modular law is needed to prove this.

I would very much like to receive comments and references to relevant work on
 *  Artin gluing and the partial map classifier FOR LOCALES (not toposes),
 *  modular lattices and the (Goursat?) equation  ab=bab  for idempotents.

I will be preparing an abridged version for the Como proceedings during the
(Continue reading)

Catuscia Palamidessi | 12 Jun 19:20 2000

CONCUR 2000: Call for Participation and Final Program

                          CALL FOR PARTICIPATION
                              FINAL PROGRAM

                               CONCUR 2000
          11th International Conference on Concurrency Theory
            State College, Pennsylvania, USA, August 22--25, 2000.

                    E-mail: concur2000 <at>

(apologies for multiple copies)

It is now time to register for CONCUR 2000. See the above mentioned WWW
pages for the registration procedure. Early registration ends on July 12, 2000.

The purpose of the CONCUR conferences is to bring together researchers,
developers and students in order to advance the theory of concurrency,
and promote its applications.


Monday 21 August

9:00 - 5:30 
(Continue reading)