Roy L. Crole | 1 May 14:23 1999
Picon
Picon

Lectureship in Computer Science


Dear Colleagues,

I would like to announce a Lectureship in Computer Science, which
may be of interest to CATEGORIES and TYPES readers. 

Leicester has a research group in Semantics which includes myself,
Simon Ambler and Neil Ghani. Current research areas include
Operational Semantics, Mechanized Reasoning, and Categorical Models of
Programming Languages. Further, the Distributed Systems group is
working on Security.  All are directly or indirectly connected with
the theory and practice of categories and types.

Please note the tight deadline for applications: 14 May 1999.

Roy Crole

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

LEICESTER UNIVERSITY

DEPARTMENT OF MATHEMATICS AND COMPUTER SCIENCE

LECTURESHIP (GRADE A/B) IN COMPUTER SCIENCE (1 POST)

Applications are invited for a permanent Lectureship in Computer Science in
the Department of Mathematics and Computer Science at the University of
Leicester.  There is no restriction regarding the area of research and
applicants with expertise in any area of Computer Science are welcomed.
The lectureship is tenable from as soon as possible.
(Continue reading)

Andrei Voronkov | 4 May 23:47 1999
Picon
Picon

LPAR'99 deadline extension


***** LPAR submission deadline has been extended to May 15 *****


                             LPAR'99
           6th International Conference on Logic for Programming
                         and Automated Reasoning

                     Tbilisi, Republic of Georgia
                         September 6-10, 1999

                http://www.csd.uu.se/~voronkov/lpar99.html

Topics

  automated reasoning
  logic in databases
  logic and complexity
  logic and concurrency
  programming and logic
  model checking
  formal methods
  programming languages and complexity
  knowledge representation and reasoning
  reasoning about actions
  rewriting
  logic programming
  constraints
  specification and verification using logics
  modal logic and computing
(Continue reading)

Fairouz Kamareddine | 5 May 20:11 1999
Picon
Picon

visiting fellowships:

Attachment: application/octet-stream, 2184 bytes
Matthew Hennessy | 6 May 12:30 1999
Picon
Picon

Research positions


                       UNIVERSITY OF SUSSEX

            RESEARCH FELLOWS IN THE FOUNDATIONS OF COMPUTING

Two Research Fellows are required for a 2-year project entitled ``The
Semantic Foundations of Mobile Computation'', under the direction of
Prof. M. Hennessy and funded by the EPSRC. At least one appointment
will require expertise in type theories for programming languages.

The project objectives include

- the development of abstract foundational calculi for mobile 
systems in which the concepts of location, mobility, failure 
and security play an central role

- the elaboration of behavioural equivalences for these calculi, 
and their associated  algebraic theories

- the construction of proof systems and methodologies for
establishing properties of mobile systems.

The project will start on 1/10/99 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.

To apply please submit applications to 

Matthew Hennessy
School of COGS
University of Sussex
Falmer
Brighton BN1 9QH
UK

Tel: +44 01273 678101                      
email: matthewh@...

from whom more details of the project and the conditions of service
are available.

Applications should include 
    - a detailed curriculum vitae, 
    - names of three referees with their email addresses, 
    - a statement  outlining the candidates proposed contribution
      to the goals of the project,
    - copies (or URL references) of any relevant publications.

J.G.Smaus | 6 May 12:52 1999
Picon

ICLP'99 Workshop: Verification in Logic Programming: CFP

ICLP'99 Workshop: Verification in Logic Programming

Call for Contributions

URL: http://www.cs.ukc.ac.uk/people/staff/jgs5/workshop99/
For further information, contact Jan-Georg Smaus (jgs5@...) or
Sandro Etalle (etalle@...)

Scope
-----
This workshop aims at hosting a discussion centred on the verification
of logic and (concurrent) constraint logic programs. The goal of
program verification is to provide tools for proving that programs
meet their specifications, i.e. that the actual program behaviour
coincides with the desired one.  In particular, we are interested in
tools and methods for verification regarding issues such as:
- termination,
- absence of deadlock and failure,
- absence of runtime errors for programs with built-ins,
- groundness of answers,
- type correctness,
- model checking.

The proof methods we are interested in include but are not limited to:
modes, types, abstract interpretation, methods developed in other
programming paradigms like process algebras and Hoare logics. The
workshop will also include a discussion on techniques for the design
and the development of (constraint) logic programs.

Contributions are especially welcome that present practical tools
or discuss the relationships existing among the various
methodologies.

Call for Contributions
----------------------
We invite papers (in English) of up to 15 pages describing original
completed work, work in progress, or interesting problems to be
solved.

Parallel submissions elsewhere are allowed. 

At least one author of each contribution is expected to present the
paper at the workshop.  A presentation can also take the form of a
demonstration of an implemented system.

The proceedings will be published as a technical report of 
New Mexico State University (http://www.cs.nmsu.edu/).

Submissions must include a cover page containing: an abstract,
keywords, postal and electronic mailing addresses, and phone
and fax numbers of one of the authors.

Please email your contribution as a Postscript file to jgs5@...
 or etalle@... or, if electronic submission is impossible,
 send two hard copies of your paper to Jan-Georg Smaus.

Important Dates
---------------
2nd August     Deadline for paper submission 
13th September Notification of acceptance 
25th October   Deadline for camera-ready versions 

Principal Organisers
--------------------
Jan-Georg Smaus (University of Kent) 
Sandro Etalle (Universiteit Maastricht)

Organising and Programme Committee
----------------------------------
Patricia Hill (University of Leeds)
Naomi Lindenstrauss (The Hebrew University of Jerusalem)
Frederic Mesnard (Universite de la Reunion)
Femke van Raamsdonk (Vrije Universiteit Amsterdam)
Salvatore Ruggieri (Universita di Pisa)

Anuj Dawar | 6 May 16:09 1999
Picon
Picon

British Logic Colloquium 1999


                  British Logic Colloquium 1999
                     - First Announcement - 

The 1999 meeting of the British Logic Colloquium will be held from
23 to 25 September at the University of Wales conference centre,
Gregynog.

Programme
---------

The meeting will include a celebration of Roger Hindley's
contributions to logic, on the occasion of his retirement from the
Department of Mathematics at the University of Wales Swansea.
The speakers on this occasion are:

 Robin Milner (Cambridge)
 Henk Barendregt (Nijmegen)
 Roger Hindley (Swansea)
 Giuseppe Longo (CNRS and ENS, Paris)
 Mariangiola Dezani (Turin)
 Jonathan Seldin (Concordia)

In addition, there will be lectures covering a wide variety of areas of
mathematical and philosophical logic as well as the history of logic,
with the following confirmed to speak:

 Ivor Grattan-Guinness (Middlesex)
 David Miller (Warwick)
 Mirna Dzamonja (East Anglia)
 Richard Kaye (Birmingham)
 Jens Blanck (Uppsala/Swansea)

Location
--------

The meeting will take place in the conference centre of the University
of Wales at Gregynog.  Gregynog is a large Victorian country house in
mid-Wales, standing in 750 acres of wooded parkland.  It is located
five miles north of Newtown, Powys, with a regular train link to
Birmingham (taking approximately 1h45m).  All participants will be
offered rooms in the house.  The number of places is limited.  To
guarantee a place, please register before 1 July 1999.

Cost
----

The cost of participation, including registration, two days lodging 
at Gregynog with full board and the conference banquet is as follows:

 non-BLC members        140 GBP
 BLC members            120 GBP
 students                70 GBP

As the number of subsidised student places is limited, early
registration is advised.

Registration
------------

To register, please complete the form below and send it, with the 
appropriate payment (cheques should be made payable to the University
of Wales Swansea) to:

Jill Edwards
Department of Computer Science
University of Wales Swansea
Singleton Park
Swansea SA2 8PP, U.K.

Enquiries may be addressed to the organisers:

Anuj Dawar     anuj.dawar@...
John Tucker    j.v.tucker@...

See also: http://www.cl.cam.ac.uk/~ad260/blc99.html

Form
----

NAME:

AFFILIATION:

ADDRESS:

EMAIL ADDRESS:

PAYMENT:

 non-BLC member        140 GBP
 BLC member            120 GBP
 student                70 GBP

SPECIAL DIETARY REQUIREMENTS:

Support
-------
The meeting is generously supported by grants from the London
Mathematical Society and the British Logic Colloquium.

Joelle Despeyroux | 11 May 16:16 1999
Picon
Picon

last CFP Types Summer School'99 - dead-line extension


** To be consistent with our first call, we extend the dead-line
** of application to May 17th.

__________________________________________________________________________
     Please distribute the following announcement to your colleagues
                     Apologies for multiple copies
__________________________________________________________________________

         L A S T   C A L L   F O R    P A R T I C I P A T I O N

              --------------------------------------------
               The 2nd International Types Summer School:

                   THEORY AND PRACTICE OF FORMAL PROOFS
              Giens, France, 30 August - 10 September 1999
              --------------------------------------------

              http://www-sop.inria.fr/types-sum-school.html

is organized by the Esprit Working Group: Types for proofs and programs.

During the last few years major achievements have been made in using 
computers for interactive proof developments to produce secure software.

This two weeks' course is for postgraduate students, researchers and
industrials who want to learn about interactive proof development.
There will be introductory and advanced lectures on lambda calculus,
type theory, logical frameworks, program extraction, and other topics
which give relevant theoretical background.  Several talks will be
devoted to the presentation of applications.

The proof assistants presented in the school represent the current
state-of-the-art in interactive theorem proving.  Participants will
get extensive opportunities to use the systems in a workstation
environment for developing their own proofs.

The DEADLINE FOR APPLICATION is Monday May 17, 1999.

Ruy de Queiroz | 13 May 14:58 1999
Picon

WoLLIC'99 - Call for Participation

PROGRAMME AND CALL FOR PARTICIPATION

6th Workshop on Logic, Language, Information and Computation (WoLLIC'99)
May 25-28, 1999

http://www.di.ufpe.br/~wollic/wollic99/

Hotel Simon,
Itatiaia National Park, Rio de Janeiro, Brazil

(In conjunction with "XII Encontro Brasileiro de Logica - EBL'99")

SCIENTIFIC SPONSORSHIP
Interest Group in Pure and Applied Logics
European Association for Logic, Language and Information (FoLLI)
Association for Symbolic Logic (ASL)
Sociedade Brasileira de Computaco (SBC)
Sociedade Brasileira de Logica (SBL)

FUNDING
CAPES, CNPq, Facolta di Scienze, Univ. di Verona

ORGANISATION
Departamento de Informatica, Universidade Federal de Pernambuco
Facolta` di Scienze, Universita` degli Studi di Verona
Centro de Logica, Epistemologia e Historia da Ciencia, Univ.Campinas

PROGRAMME

TUESDAY MAY 25th, 1999 (Tutorial Day)

Tutorials:

08:00-10:00 (with a 10min break)
  Introduction to Game Semantics
  by Samson Abramsky

10:00-10:15 Coffee/tea break

10:15-12:15 (with a 10min break)
  Markov Decision Processes and Bayesian Networks
  by Craig Boutilier

12:15-14:00 Lunch break

14:00-16:00 (with a 10min break)
  A Crash Course in Distributive Lattices
  by Francisco Miraglia

16:00-16:15 Coffee/tea break

16:15-18:15 (with a 10min break)
  Stability and Finite Model Theory
  by John Baldwin

18:15-18:30 Coffee/tea break

18:30-20:30 (with a 10min break)
  Bounded Arithmetic, Nonstandard Models
  by Alan Woods

WEDNESDAY MAY 26th, 1999

Morning: Logic and Computation

08:30 OPENING

09:00-10:00 (Invited talk WoLLIC'99/EBL'99)  Chair: John Baldwin
  Concurrent Games and Full Completeness
  by Samson Abramsky, Division of Informatics, Edinburgh University, UK

10:00-10:15 Coffee/tea break

10:15-11:15 3 contributed papers (20min each)  Chair: Ruy de Queiroz

   10:15-10:35 omega-continuos cpo's, omega-algebraic cpo's, SFP domains and
               retract of SFP domains as information systems
               by Benjamin Callejas Bedregal, Departamento de Informatica e
                  Matematica Aplicada, Universidade Federal do Rio Grande do
                  Norte, Brazil

   10:35-10:55 Alpha Conversion in Simply Typed Lambda Calculus
               by Ana Bove, Department of Computing Science, Chalmers
                  University of Technology, Goteborg, Sweden, and
                  Paula Severi, Centro de Matematica, Facultad de Ciencias,
                  Universidad de la Republica, Uruguay

   10:55-11:15 Dependence Analysis Through Type Inference
               by Ozan Hafizogullari and Christoph Kreitz, Department of
                  Computer Science, Cornell University, USA

11:15-11:30 Coffee/tea break

11:30-12:30 (Invited talk EBL'99/WoLLIC'99)  Chair: Valeria de Paiva
            (TBA)
            by Paulo Veloso, Departamento de Informatica, Pontificia
               Universidade Catolica do Rio de Janeiro, Brazil

12:30-14:00 Lunch break

Afternoon: Logic and Information

14:00-15:00 (Invited talk)  Chair: Alan Woods
            Abstraction and Decomposition Techniques for Markov Decision
            Processes
            by Craig Boutilier, Department of Computer Science, University
               of British Columbia, Canada

15:00-15:15 Coffee/tea break

15:15-16:15 3 contributed papers (20min each)  Chair: Ana Teresa C. Martins

   15:15-15:35 A little note about Maxichoice and Epistemic Entrenchment
               by Eduardo Ferme, Departamento de Computacion, Universidad
                  de Buenos Aires, Argentina  

  15:35-15:55 Irrevocable Belief Revision and Epistemic Entrenchment
               by Eduardo Ferme, Departamento de Computacion, Universidad
                  de Buenos Aires, Argentina  

   15:55-16:15 A logic-based system for controlling inconsistencies in
                 evolutionary databases
               by Walter A. Carnielli, Centro de Logica, Universidade
                  Estadual de Campinas, Brazil, and
                  Sandra de Amo, Departamento de Informatica, Universidade
                  Federal de Uberlandia, Minas Gerais, Brazil

THURSDAY MAY 27th, 1999

Morning: Logic, Model Theory and Complexity Theory

09:00-10:00 (Invited talk WoLLIC'99/EBL'99)  Chair: Francisco Miraglia
            Finite and Infinite Model Theory
            by John Baldwin, Department of Mathematics, Statistics and
               Computer Science, University of Illinois at Chicago, USA

10:00-10:15 Coffee/tea break

10:15-11:15 3 contributed papers (20min each)  Chair: E. Hermann Hauesler

   10:15-10:35 Model theory of the recursively enumerable many-one degrees
               by Andre O. Nies, Department of Mathematics, University of
                  Chicago, USA

   10:35-10:55 On clausal models
               by Dusan Guller, Institute of Informatics, Comenius University,
                  Slovakia

   10:55-11:15 (tba)
               by (tba)

11:15-11:30 Coffee/tea break

11:30-12:30 (Invited talk)  Chair: Craig Boutilier
            Intrinsic theories: a methodology for reasoning about functional
            programs and their computational complexity
            by Daniel Leivant, Department of Computer Science,
               Indiana University, USA

12:30-14:00 Lunch break

Afternoon: Categorical Logic and Non-Classical Logics

14:00-15:00 (Invited talk WoLLIC'99/EBL'99)  Chair: Samson Abramsky
           A Lattice-Theoretic Concept of Logical Connective
           by Francisco Miraglia, Instituto de Matematica e Estatistica,
              Universidade de Sao Paulo, Brazil

15:00-15:15 Coffee/tea break

15:15-16:15 3 contributed papers (20min each)  Chair: Mario Benevides

   15:15-15:35 Hybrid logic is the bounded fragment of first order logic
               by Carlos Areces, University of Amsterdam, The Netherlands,
                  Patrick Blackburn, Universitaet des Saarlandes, Germany, and
                  Maarten Marx, University of Amsterdam, The Netherlands

   15:35-15:55 A Dynamic Modal Arrow Logic for the Interpretation of
                 Verb Stems and Voice Affixes in Tagalog
               by Ralf Naumann and Anja Latrouite, Seminar fuer Allgemeine
                  Sprachwissenschaft, Universitaet Duesseldorf, Germany

   15:55-16:15 The Taming (Timing) of the States
               by Angelo Montanari, Adriano Peron and Alberto Policriti,
                  Dipartimento di Matematica e Informatica, Universita`
                  di Udine, Italy

FRIDAY MAY 28th, 1999

Morning: Logic and Proof Theory

09:00-10:00 (Invited talk WoLLIC'99/EBL'99)  Chair: Daniel Leivant
            Bounded Arithmetic from a Rational Perspective
            by Alan Woods, Department of Mathematics, University of
               Western Australia, Australia

10:00-10:15 Coffee/tea break

10:15-11:15 3 contributed papers (20min each)  Chair: Luiz Carlos Pereira

   10:15-10:35 A Cut-Free Gentzen Formulation of Modal Logic S5
               by Torben Brauner, Centre for Philosophy and Science-Theory,
                  Aalborg University, Denmark

   10:35-10:55 A Sequent Calculus for a Paraconsistent Default Logic
               by Ana Teresa de C. Martins, Tarcisio Pequeno and
                  Marcelino Pequeno, Departamento da Computacao,
                  Universidade Federal do Ceara', Brazil

   10:55-11:15 A sequent calculus for Lukasiewicz's three-valued logic based
               on Suszko's bivalent semantics
               by Jean-Yves Beziau, LNCC/CNPq, National Laboratory for
                  Scientific Computing, Rio de Janeiro, Brazil

11:15-11:30 Coffee/tea break

11:30-12:30 (Invited talk EBL'99/WoLLIC'99)  Chair: (tba)
            (TBA)
            by (to be announced)

12:30 CLOSING

------

Philip Wadler | 14 May 21:24 1999

Recursive types in polymorphic lambda calculus

Attachment: application/octet-stream, 836 bytes
Martin Buechi | 16 May 13:02 1999
Picon

Type soundness issues in Java

Type soundness in Java has received quite a bit of attention, with a number
of proofs both for the language and the byte code. However, I recently
stumbled over two practical type soundness problems that don't seem to be
covered by the above work or by any binary compatibility publications that
I am aware of:

1.Failure of type soundness in combination with binary compatibility
--------------------------------------------------------------------
I have stumbled over what I consider to be a failure of type soundness in
Java. The problem is exposed in combination with binary compatibility.
However, since Java even defines an exception for this case, I am wondering
how type soundness is really defined in Java. Or is this just an
implementation error, that is present in all JVM's that I have tested?

Here goes the example:

-- I.java

interface I {
	int c=4;
	void m();
}

-- A.java

public class A implements I { // "implements I" commented out for recompilation
	public void m() {
		System.out.println("m");
	}
}

-- Main.java

public class Main {

	public static void main(String args[]) {
		A a = new A();
		I i;
		System.out.println("I've been started");
		if(a instanceof I)
			System.out.println("a is instance of I!");
		else
			System.out.println("a Is NOT instance of I");
		i=a;
		System.out.println("Cast succeeded!");
		System.out.println(java.lang.Integer.toString(i.c,10));
		i.m();
	}
}

--

I have tested this under JDK 1.2 on Solaris 2.6 (as well as JDK 1.1.7 on
Solaris and under Netscape 4.07 and on the Mac MRJ 2.0):

First we compile everything:

% /opt/jdk_1.2/bin/javac Main.java

Then we comment out "implements I" in A.java, save it, and recompile only
A.java.

% /opt/jdk_1.2/bin/javac A.java

Then we run it.

% /opt/jdk_1.2/bin/java Main
I've been started
a Is NOT instance of I
Cast succeeded!
4
Exception in thread "main" java.lang.IncompatibleClassChangeError: class A does
not implement interface I
        at Main.main(Compiled Code)

--

The interesting thing is that the assignment i=a succeeds, even though the
run-time type of a is A and A does not implement I, as correctly noted by
the previous output statement. At this point I consider type soundness to
be broken.

That i.c doesn't cause any error isn't really surprising because its value
is independent of the value of i. It works even if i is null.

The method call i.m() finally produces the expect error message. So the
type system indicates the problem and prevents any damage from happening.
However, I think that this error message should occur at the point where we
(try to) assign a to i.

This issue is actually discussed in Sect. 13.4.4 of the Java Language
Specification:

"Changing the direct superclass or the set of direct superinterfaces of a
class type will not break compatibility with pre-existing binaries,
provided that the
total set of superclasses or superinterfaces, respectively, of the class
type loses no members."

"If a change to the direct superclass or the set of direct superinterfaces
results in any class or interface no longer being a superclass or
superinterface, respectively, then link-time errors may result if
pre-existing binaries are loaded with the binary of the modified class."

A similar example follows, but with an explicit superclass removed/replaced
by Object. The manual claims that in this case: "... then a VerifyError is
thrown at link time."

However, the case of removing an interface is not explicitly mentioned.
Although I believe it should be treated similarly.

Have I just overlooked something else in the manuals, or has this problem
been documented before? (I checked the type soundness and binary
compatibility papers of Drossopoulou, Eisenbach, Wragg, von Oheimb, and
Nipkow, but didn't find anything.)

2. Practical undermining of type soundness by "bad" programming practice
------------------------------------------------------------------------
The second issue concerns the advocated programming style of the Java
Collections Framework  (JCF)
(http://java.sun.com/products/jdk/1.2/docs/guide/collections/overview.html):

"All of the modification methods in the collection interfaces are labeled
optional. Some implementations may not perform one or more of these
operations, throwing a runtime exception (UnsupportedOperationException) if
they are attempted. Implementations must specify in their documentation
which optional operations they support. Several terms are introduced to aid
in this specification."

What is the difference from the client's perspective between an object
explicitly throwing a UnsupportedOperationException as advocated in JCF and
an automatically generated "no such method" in an untyped/not type sound
language?
(UnsupportedOperationException being a subclass of
java.lang.RuntimeException, methods are not even required to declare in
their throws clause that this type of exceptions might be thrown during the
execution of the methods but not caught. Anyhow, I am not sure if it would
make a big practical difference if UnsupportedOperationException would have
to be listed in the throws clause.)

I don't believe too much in the "Implementations must specify in their
documentation which optional operations they support" either because the
documentation is not fed to the compiler and, therefore, easily ignored.

In a strongly type language with by-name equivalence for types, I would
like to use types to stand for explicit external specifications (behavioral
typing). If we introduce UnsupportedOperationException's we have to reduce
the specifications to "does the desired thing or throws an exception",
where the "or" stands for a demonic choice. Hence, no meaningful properties
can be proved anymore. Therefore, I personally believe that the much
acclaimed JCF sets a bad example by promoting the practical undermining of
type soundness.

I think that the solution to the JCF design problem would be to introduce
many smaller interfaces (e.g. CollectionWithoutModification, CollectionAdd,
CollectionRemove) grouping related methods, that are likely to be fully or
not at all implemented,that are then combined. Of course, I would advocate
compound types (Martin B├╝chi and Wolfgang Weck. Compound Types for Java.
Proceedings of OOPSLA'98. Pages 362-373. ACM Press, 1998 [End of own paper
ad :)]) or a similar mechanism to avoid cluttering the name space with all
the combinations required because of strict by-name type equivalence.

Yours,

Martin

====================================================================
Abo Akademi University          | mailto:Martin.Buechi@...
Department of Computer Science  | phone: +358 (0)2 215-4034
Lemminkaisenkatu 14a            | fax:   +358 (0)2 215-4732
20520  Turku                    | www:   http://www.abo.fi/~mbuechi/
FINLAND                         | time:  UTC +0300
--------------------------------------------------------------------
Make something idiot proof, and someone will build a better idiot.
====================================================================


Gmane