headers
Teodor Knapik | 1 Oct 1997 15:17
Picon

vacant position

Tenured professorship in computer science is available
at the University of Reunion Island starting from September,
1, 1998. The person holding the position is intended to
enrich 30 staff members of IREMIA, the local research
laboratory composed of both computer scientist and
mathematicians. The laboratory is well equipped with Sparc
workstations and Mac computers.

The research interests of the applicant should be related
to one of the following items

      - formal verifications using model checking
          and theorem proving,
      - logic programming, constraint solving,
        concurrent constraint logic programming,
      - machine learning (both symbolic and numerical),
      - multi-agent systems.

Besides a PhD, one of the formal requirements is the French
diploma "Habilitation a diriger les recherches". However,
equivalent foreign diplomas (as e.g. German Habilitationsschrift)
are accepted. Moreover, candidates from countries where an
equivalent diploma does not exist are encouraged to apply,
provided that they justify a substantial experience in research,
teaching and research supervision.

Another requirement is the ability to teach in French at both
undergraduate and graduate levels.

The salary depends on experience but it is at least 276000 FRF
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 2 Oct 1997 19:10
Picon

Research Position at Stanford


STANFORD UNIVERSITY
Department of Computer Science
Research Associate

Research Group in the Computer Science Department seeks qualified
applicants for a Research Associate position.  The objective of the
project is to develop methods for ensuring semantic consistency
between parts of software systems. In particular, it will be necessary
to protect systems against errors resulting from faulty modules, or
errors introduced as a result of transmitting code across an insecure
network. One approach to this problem is to transmit a program together
with a proof that certain errors will not occur. Another approach is
to augment a system with on-line test modules that monitor the behavior
of potentially faulty components. Expertise in any of the following
topics may prove useful: formal methods, automated logical tools,
model checking, cryptography, protocol analysis, probabilistic methods,
type systems, linear logic, Java compiler, virtual machine, and Java
security. Duties include independent research, working with graduate
students and other members of the research project, including
collaborators at other institutions, and attending research meetings.
Applicants must have Ph.D. in Computer Science or relevant discipline.
Previous implementation experience will be a plus. Salary will depend on
the candidate's qualifications. Send resume and at least three references to
Professor John Mitchell, Department of Computer Science,  Gates Bldg. 4b,
Stanford University, Stanford, CA 94305-9030; mitchell@...
(e-mail preferred).

--------------
(Addendum: since lots of ad are being posted with specific salary
(Continue reading)

Permalink | Reply | 0 comments |
headers
Uffe Henrik Engberg | 3 Oct 1997 03:04
Picon
Favicon

Research Positions at BRICS Research Centre and Int. PhD School


		 BRICS, Basic Research in Computer Science

		   Universities of  Aarhus  and Aalborg

Research Positions at BRICS Research Centre and International PhD School

There are  several research positions  at BRICS  starting  next year, 1998.
Applications by researchers are welcome in theoretical computer science and
related areas, especially, but not exclusively, within the following areas:

      - Semantics of Computation,
      - Logic,
      - Algorithms and Data Structures,
      - Complexity Theory,
      - Data Security,
      - Programming Languages,
      - Distributed Computing,
      - Verification.

Openings,  while likely to  start as postdoctoral  positions, generally for
1-2 years, have the possibility of extension to longer-term positions.

BRICS, Basic Research in Computer Science, is funded by the Danish National
Research Foundation and consists of the BRICS Research Centre and the BRICS
International PhD School.
The Research Centre (Director Glynn Winskel) is a joint venture between the
theoretical-computer-science  groups at   the  universities of  Aarhus  and
Aalborg, Denmark.
The PhD  School (Director Mogens Nielsen)  is based in the Computer Science
(Continue reading)

Permalink | Reply | 0 comments |
headers
H. de Swart | 3 Oct 1997 15:53
Picon
Picon

second call for papers and tutorials Tableaux'98


Second CALL for PAPERS and TUTORIALS                     

                     International Conference

                            TABLEAUX'98

               Analytic Tableaux and Related Methods

      Conference Centre Boschoord, Oisterwijk (near Tilburg),
                          the Netherlands

                          May 5 - 8, 1998

                            ==========

This conference is a continuation of international workshops/conferences 
on Theorem Proving with Analytic Tableaux and Related Methods held in 
Lautenbach near Karlsruhe (1992), Marseille (1993), Abingdon near 
Oxford (1994), St. Goar near Koblenz (1995), Terrasini near Palermo (1996) 
and Pont-a-Mousson near Nancy (1997).

This conference has the scientific and financial support of the Department 
of Philosophy of Tilburg University (the Netherlands), and is 
sponsored by:
- SUN Microsystems Nederland B.V.,
- Compulog,
- the Dutch Graduate School in Logic.

                            ==========
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vladimir Alexiev | 4 Oct 1997 01:57
Picon
Picon

Re: about current state of the art of LL in AI...

[For new readers that may wonder why this showed up in their
mailboxes... note that the LINEAR mailing list is mirrored to
TYPES. --BCP]

> To: Vladimir Alexiev <vladimir@...>
> From: jpalacio@...
> could you tell me aboput the current state of the art relating Linear Logic
> in Artificial Intelligence? I want to keep this line of research as much as
> possible.

This question is probably better addressed to the linear mailing list, so I am
forwarding it there. Here are the things that come to my mind. Probably you
already know about some of them. You can find bibliographic references at
http://pecan.srv.cs.cmu.edu/afs/cs/user/iliano/www/linearbib/ 
or http://www.cs.cmu.edu/%7Eiliano/linearbib/linearbib.html. In my opinion,
there is still very little done in this area, and there's potential for much
more. 

- Deductive planning (Masseron+Tollu+Vauzielles; Holdoebler and others at
  Darmstadt).
- Hierarchies with exceptions (Fouquere+Vauzielles).
- Database updates based on the previous work (Vauzeilles+?).
- Explanations (abduction) (Arima).
- NLP (Hodas+Miller), categorial grammars (Morill).
- Connection between LL and Fuzzy logic (Barr
  http://theory.doc.ic.ac.uk/tfm/papers/BarrM/fuzzy.models.ps.Z;  Cardoso+
  Valette+Pradin-Chezalviel; Kreinovich+Nguyen)
- There's a lot of work on LL LP, which isn't necessarily related to AI, but
  it provides programming languages with potential applications to AI that are
  more sophisticated than Prolog. Some of these languages are (no doubt I am
(Continue reading)

Permalink | Reply | 0 comments |
headers
Patrick Lincoln | 6 Oct 1997 19:41
Picon

Re: about current state of the art of LL in AI...


Here are some more responses: 

pdl.

----------

From: Vijay Saraswat <vj@...>
Date: Sat, 4 Oct 1997 06:20:16 -0400 (EDT)
To: vladimir@...
CC: jpalacio@..., linear <at> CS.Stanford.EDU
In-reply-to: message from Vladimir Alexiev on Fri, 3 Oct 1997 16:57:51 -0700
Subject: Re: about current state of the art of LL in AI...

Let me add the work that Dalrymple, Lamping and I have been doing
(with various collaborators) on using Linear cc as the vehicle
for assembling meanings of natural language utterances, in a
context where the parsing is done using Kaplan and Bresnan's LFG
(Lexical Functional Grammars).

  http://www.parc.xerox.com/istl/groups/nltt/semantics

This approach  is being pursued by several other authors now, and
a book (edited collection of papers) is being worked on. 

----------

Date: Mon, 6 Oct 1997 11:36:10 +0200
From: Serena.Cerrito@... (Serena Cerrito)
To: jpalacio@..., vladimir <at> cs.ualberta.ca
(Continue reading)

Permalink | Reply | 0 comments |
headers
Thom Fruehwirth | 7 Oct 1997 11:09
Picon

Research Position in Computational Logic Available

Research Position in Computational Logic Available
(EC Training and Mobility of Researchers, Framework 4)

As part of our commitment to highly competitive research and
development in constraint reasoning and programming, applications are
invited for research positions at post-doctorate and also
post-graduate level in the field of Computational Logic at the
department of Computer Science, with an emphasis on (concurrent)
constraint (logic) programming, program analysis, synthesis and
transformation of constraint programs or agent based computing
utilizing constraint reasoning.

Researchers would be funded by the European Community under Marie
Curie Fellowships provided by the Training and Mobility of Researchers
(TMR) scheme of the Framework 4 programme for a maximum of 36 months
(post-grad) or 24 months (post-doc). Applicants must be nationals of
the European Union (except Germany), or an associated state (Iceland,
Israel, Lichtenstein, Norway, Switzerland), normally not older than
35.

More information about TMR Activity 3 Marie Curie Research Training
Grants you find at http://www.cordis.lu/tmr/src/grants1.htm which has
the following links:
 Frequently Asked Questions http://www.cordis.lu/tmr/src/quest&an.htm
 Information Package ftp://ftp.cordis.lu/pub/tmr/docs/rtg_971.doc
 Application Form ftp://ftp.cordis.lu/pub/tmr/docs/rtg_971.doc
 Evaluation Guide ftp://ftp.cordis.lu/pub/tmr/docs/tmr-eval.doc

More information on our activities in constraint reasoning and
programming you find at
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gerard Boudol | 7 Oct 1997 15:49
Picon
Picon
Favicon

Paper announcement: types and concurrency

This is to announce the availability of the paper

   "Typing the use of resources in a concurrent calculus",

to be published in the Proceedings of ASIAN'97, the Asian Computing
Science Conference, Kathmandu, Nepal, December 9-11, 1997 (LNCS to
appear), at the URL

   http://www.inria.fr/meije/personnel/Gerard.Boudol.html

Here is the abstract:

We introduce a new type system for the blue calculus -- a variant of
the pi-calculus that directly contains the lambda-calculus. Our
notion of type is built upon a combination of Curry-Church simple
types and Hennessy-Milner logic with recursion. We interpret a
modality as the type of a process offering a resource of some type on
a given name. In the typing system this is used in a kind of logical
cut rule, ensuring that a message to the name will meet a
corresponding offer. We show that our calculus is type safe, that is,
types are preserved along the computations.
Permalink | Reply | 0 comments |
headers
Patrick Lincoln | 9 Oct 1997 20:06
Picon

Re: about current state of the art of LL in AI...


Here are two more responses: 

pdl.

----------

From: lecomte@...
Posted-Date: Tue, 7 Oct 1997 08:05:15 +0000
Comments: Authenticated sender is <lecomte@...>
To: linear@...
Date: Tue, 7 Oct 1997 08:05:15 +0000
Subject: LL and AI
Priority: normal
X-Mailer: Pegasus Mail for Windows (v2.32a)

Concerning linguistic (and NLP) applications,
you must also add works by :

J. Lambek,
M. Moortgat,
M. Abrusci,
C. Casadio,
A. Lecomte and C. Retore
...

see all the proceedings of the Roma workshop
(every year since 1993)

----------
(Continue reading)

Permalink | Reply | 0 comments |
headers
Nevin Heintze | 10 Oct 1997 05:08
Favicon

call for papers

                           Call for Papers

            Workshop on Formal Methods and Security Protocols

                       Thursday, 25 June, 1998
                        Indianapolis, Indiana
                         (following LICS'98)  

  Computer security protocols are notoriously difficult to get right.
  Surprisingly simple problems with some well known protocols have been found
  years after the original protocol was published and extensively analyzed.  

  Our workshop goal is to bring together the formal methods and security
  communities.  Security is a current hot topic in the formal methods
  community, and we hope that this workshop can help focus these energies.

  Topics of interest include descriptive techniques (specification languages,
  models, logics) and analysis techniques (model checking, theorem proving,
  and their combination), as applied to protocols for authentication, fair
  exchange, electronic commerce, and electronic auctions.  However, this list
  is not exclusive.  We particularly want to hear about new approaches, new
  problems, new security properties, and new protocol bugs. Reports on work
  in progress are welcome.   

  The program of the workshop will include a keynote address by Roger
  Needham, a number of technical sessions (with talks of about 15-20 minutes
  duration), and a panel discussion.  The overall program will aim to
  address questions such as: What are the opportunities in security for more
  formal reasoning and analysis?  Where should formal methodists be
  spending their talent, time, and energy?  What are the more pressing
(Continue reading)

Permalink | Reply | 0 comments |

Gmane