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

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)

Permalink | Reply | 0 comments |
headers
Andrei Voronkov | 4 May 1999 23:47
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)

Permalink | Reply | 0 comments |
headers
Fairouz Kamareddine | 5 May 1999 20:11
Picon
Picon

visiting fellowships:

		VISITING FELLOWSHIPS AT
	
	The ULTRA Research Centre  Of Logic and Computation
	in the Department of Computing and Electrical Engineering
	at Heriot-Watt University, in Edinburgh, Scotland

	http://www.cee.hw.ac.uk/ultra/institute.html

The ULTRA Research Centre Of Logic and Computation will host leaders
and young researchers in any field of Logic and Computation.  We are
offering various postdoctoral and visiting positions ranging between
THREE MONTHS and A YEAR.  We are interested in those researchers who
can contribute to our currently running projects (see 
http://www.cee.hw.ac.uk/ultra/) and in particular to the following two:

1. Efficient Programming in Classical Logic: Professor Fairouz 
   Kamareddine and Dr. Francois Monin.
2. On Type Theory and Term Rewriting for Expressive and Efficient
   Programming Languages: Professor Fairouz Kamareddine and 
   Dr. Joe Wells

In addition to the above projects, two new postdoctoral researchers 
are joining us this september to work on the following projects:

3. The theory and practice of  Explicit rewriting.
4. On the automation of rewrite systems

We are looking for active, energetic and committed people who will
contribute to projects 1,2,3 and 4 above and to our other ultra projects.
The visiting positions are available immediately.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Matthew Hennessy | 6 May 1999 12:30
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
(Continue reading)

Permalink | Reply | 0 comments |
headers
J.G.Smaus | 6 May 1999 12:52
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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Anuj Dawar | 6 May 1999 16:09
Picon
Picon
Favicon

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

Permalink | Reply | 0 comments |
headers
Joelle Despeyroux | 11 May 1999 16:16
Picon
Picon
Favicon

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

Permalink | Reply | 0 comments |
headers
Ruy de Queiroz | 13 May 1999 14:58
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)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 14 May 1999 21:24
Favicon

Recursive types in polymorphic lambda calculus

There is a fairly standard encoding of recursive types
into polymorphic lambda calculus, given by

	rec X.F[X]  =  all X.(F[X] -> X) -> X

where F[X] is a type in which the type variable X appears only
covariantly.  Recall that every covariant type corresponds to a
covariant functor, so for every h:X->Y we have F[h]:F[X]->F[Y].
If we abbreviate T = rec X.F[X], then the key functions on this
type are given by the polymorphic lambda terms:

	fold : all X.(F[X] -> X) -> T -> X
	fold = Lam X.lam k:F[X]->X.lam t:T.t{X}(k)

	in   : F[T] -> T
	in   = lam u:F[T].Lam X.lam k:F[X]->X.k(F[fold{X}(k)](u))

	out  : T -> F[T]
	out  = fold{F[T]}(F[in])

Questions: Who first had this insight?  Where is a good place to find
this spelled out in the literature?  Please send results to me, and I
will summarize them for the list.  Cheers, -- P
Permalink | Reply | 0 comments |
headers
Martin Buechi | 16 May 1999 13:02
Picon
Favicon

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

Permalink | Reply | 0 comments |

Gmane