[ToC] _________________________ AMAST Links 03 01

Contributions are welcome! _ _ _ _ _ _ _ _ _ _ _ _ _ _ date: 21 March 1996
e-mail to: amast@cs.utwente.nl ________________________ e-mailed to: 822 subscribers


Table of Contents

Meetings
[M1] AMAST'96, Preliminary Program (upd. [AL0208C1])
[M2] TARK VI, Call for Registration (upd. [AL0207C4])
[M3] Formal Methods for Industrial Critical Systems, Sat. W. at FME'96
[M4] 8th Eur. Summer School in Logic, Language & Information, ESSLLI'96
[M5] GOEDEL'96, Registration (upd. [AL0207CN])
[M6] 9th Int'l Symp. on Languages for Intensional Programming, ISLIP'96
[M7] COORDINATION'96, Call for Participation (upd. [AL0207CL])
[M8] ELP'96, Call for Participation (upd. [AL0206CA])
[M9] CAAP'96 ESOP'96 CC'96, Programme & Registration (upd. [AL0206C5])
[MA] Int'l Conf Information, Statistics & Induction in Science, ISIS'96
[MB] 8th Int'l Lipari School WWW page (upd. [AL0208M2])
[MC] Joint Int'l W's TACAS'96 & AIN'96, Final Program (upd. [AL0207CB])
[MD] PAAM'96, Preliminary Program & Registration (upd. [AL0208C2])
[ME] MFPS'96, Information Update & Registration (upd. [AL0208CC])
[MF] ICALP'96, Call for Participation and Program (upd. [AL0206C8])
[MG] 3rd Dutch Specification Day, Final Program
[MH] 3rd Seminar on Algebra, Logic, and Geometry in Informatics, ALGI-3
[MI] SMC/AE Symposium on Informatics
[MJ] 7th BCS FACS Refinement Workshop, Programme (upd. [AL0207CH])
CfPs
[C1] CONCUR'96, TCS Special Issue (upd. [AL0208C6])
[C2] 9th Int'l Conf. Theorem Proving in Higher Order Logics, TPHOLs'96
[C3] Int'l Conf. on Formal Methods in Computer-Aided Design, FMCAD'96
[C4] 1st Int'l Workshop on Rewriting Logic & its Applications, RWLW'96
[C5] 20th German Annual Conference on Artificial Intelligence, KI-96
[C6] Engineering Complex Computer Systems, Minitrack at 30th HICSS
[C7] 3rd Int'l Conf. on Typed Lambda Calculi & Applications, TLCA'97
[C8] Int'l Conf. Logical Aspects of Computational Linguistics, LACL'96
[C9] IFIP TC6/WG6.1 Joint Int'l Conf. FORTE/PSTV'96 (upd. [AL0208C5])
[CA] Logic Colloquium '96 (European Summer Meeting of the ASL), LC'96
[CB] 3rd Int'l Conf. on High Performance Computing, HiPC'96
[CC] DIMACS Symp. on Teaching Logic and Reasoning in an Illogical World
[CD] JUCS Special Issue on Evolving Algebras
Jobs
[J1] Associate Professor Positions at Italian Universities
[J2] Post-Doc Position Softw. Engineering, E&CE Dep't, U Waterloo, CND
[J3] Research Fellowship Type Theory & Appl., CS Dep't, U Durham, UK
[J4] Software Engineers wanted, SMG, Universite' Libre de Bruxelles, B
[J5] Postdoctoral Research on Logic in CS, Brandeis U, Waltham, MA, USA
[J6] M.Sc. Studentships Logic & Found. Progr., DCS, QMWC, U London, UK
[J7] Ph.D. Studentships Knowl. Repr. & Reason., DCS, QMWC, U London, UK
[J8] Faculty Position Informat. Sys., ISTD, Creighton U, Omaha, NE, USA
[J9] Executive Director Position, IITM, Creighton U, Omaha, NE, USA
[JA] Formal Verification Jobs, Hewlett-Packard GSL, Roseville, CA, USA
[JB] Visiting Research Position in Real-Time Systems, DoCS U Uppsala, S
Literature
[L1] Tech.Rep.: The Topological Structure of Asynchronous Computability
[L2] Paper: Categories for computation in context and unified logic: I
[L3] Preprint: Enrichment and Representation Theorems for Domains
[L4] Paper: Formal Verification of Algorithm W: The Monomorphic Case
[L5] Book: Partial-Order Methods for Verification of Concurrent Systems
Tools
[T1] Coq Proof Assistant, Version 5.10.15
Problems
[P1] Question: Decision algorithm for 2-nested Simulation Relation
Services
[S1] Proc. 3rd AMAST W. on Real-Time Systems, ARTS'96 (upd. [AL0208M1])
[S2] FLIRTS WWW page moved (upd. [AL0208S3])
[S3] VISUAL'96 WWW page, 1st Int'l Conf. on Visual Information Systems
[S4] New e-mail list on Software Verification
Archive
[A1] New items in the AMAST information repository in Twente
[A2] This issue

[M1] _________________________ AMAST Links 03 01

5th Int'l Conf. Algebraic Methodology and Software Technology, AMAST'96

Ludwig-Maximilians-Universität, München, Germany, July 1-5, 1996

Update of information in [AL0208C1] .
The AMAST'96 Preliminary Program is available.

[M2] _________________________ AMAST Links 03 01

Theoretical Aspects of Rationality and Knowledge, TARK VI

De Zeeuwse Stromen, The Netherlands, March 17 - 20 1996

Update of information in [AL0207C4] .

The TARK VI Call for Registration is available.

[M3] _________________________ AMAST Links 03 01

Formal Methods for Industrial Critical Systems

Oxford, England, March 19th, 1996
(Satellite Workshop at FME'96)

The first workshop of the ERCIM Working Group on Formal Methods for Industrial Critical Systems will be held in Oxford on March 19th, 1996 as a satellite meeting of the FME'96 Symposium.

Further information is available:


[M4] _________________________ AMAST Links 03 01

8th European Summer School in Logic, Language & Information, ESSLLI'96

Prague, Czech Republic, August 12 -- 23, 1996

The full version of this announcement is available.

Alike the other ESSLLI summerschools, the main focus will be the intersection of the areas between logic, linguistics, and computation, particularly where it concerns the modelling of human linguistic and cognitive abilities. As such, the programme includes courses, workshops and symposia covering a variety of topics within six areas of interest: Logic, Language, Computation, Logic & Computation, Computation & Language, and Language & Logic.

Courses are cast at both introductory and advanced levels. Introductory courses are designed to familiarize students with new fields and do not presuppose any background knowledge, while advanced courses are designed to allow participants to acquire more specialized expertise in areas they are already familiar with. Workshops are chaired by an expert in the field and will provide an opportunity for PhD students and other young researchers to present their work and gain informed feedback and useful contacts. Symposia will typically consist of a series of presentations on a timely topic by people active in the relevant areas. Both workshops and symposia are intended to encourage collaboration and cross-fertilization of ideas by stimulating in-depth discussion of issues which are in the forefront of current research in the field. Besides courses, workshops and symposia, there will also be evening lecturers, in which highly actual topics in research in Logic, Language and Information will be addressed.

A novelty at ESSLLI'96 is the student session. Students are encouraged to submit short papers describing work in progress.

More detailed information. See full version of announcement, for:

  1. A reminder (Note: last-minute contribution to this AL issue);
  2. The programme of ESSLLI'96, given for each of the six areas above;
  3. The ESSLLI'96 Student Session;
  4. Local information: ESSLLI'96 site, accommodation, social events.

Further information can be found at the ESSLLI'96 Website .


[M5] _________________________ AMAST Links 03 01

Logical Foundations of Mathematics, Computer Sci. & Physics, GOEDEL'96

Kurt Gödel's Legacy
Brno (birthplace of Kurt Gödel), Czech Republic, August 25-29, 1996

Update of information in [AL0207CN] .
The full version of this announcement is available.

The conference announcement gives new information about the following items, among others:

Up-to-date information is maintained on the WWW.

A limited number participants from economically severely handicapped countried can be supported by the organizers by allowing registration for student fee. Send your application for financial assistance electronically to <zlatuska@muni.cz>, or, if electronic connection cannot be used, to:

Dr Jiri Zlatuska
GOEDEL'96
Faculty of Informatice
Masaryk University
Botanicka 68a
CZ-602 00 Brno
Czech Republic

[M6] _________________________ AMAST Links 03 01

9th Int'l Symposium on Languages for Intensional Programming, ISLIP'96

Arizona State University, Tempe, Arizona, USA, May 13-15, 1996

The full version of this announcement is available.

There's a growing interest in computational models and/or programming languages and systems based on intensional logics such as temporal logic, interval logic, modal and intuitionistic logics. In fact, a whole new programming model called intensional programming has been created with applications in a wide range of areas including parallel programming, dataflow computation, temporal reasoning, scientific computation, real-time programming, temporal databases, spreadsheets, attribute grammars, and hardware synthesis.

This symposium aims at bringing together researchers working in all aspects of this area, and to promote intensive discussions and foster collaboration among researchers.

At the Symposium, the research will be presented and also critiqued, and the resulting modified, final papers will appear in a book entitled Intensional Programming II, published by World Scientific Press. (ISLIP 95 resulted in the book Intensional Programming I.)

Details about registration and accommodation will be provided later.

Symposium Chair

Edward A. Ashcroft / ISLIP'96
Department of Computer Science & Eng, Arizona State University
Tempe, Arizona 85283, U.S.A.
Phone: +1 602 965-7544, Fax: +1 602 965-2751
E-mail: ed.ashcroft@asu.edu

Latest information about the Symposium will be made available via the WWW page .


[M7] _________________________ AMAST Links 03 01

First Int'l Conf. on Coordination Models and Languages, COORDINATION'96

Cesena, Italy, April 15-17, 1996

Update of information in [AL0207CL] .
Preliminary Programme and Call for Participation .

Final program, registration forms and local information on how to reach Cesena are available per WWW .

Extended deadline for early registration: March 20th, 1996.

New! The tutorial "A cup of Java", by a person from
Sun Microsystems, has been added to the program.

Demos: the provisional program for demos will soon be available; a few extra slots for demos have been made available. To announce new demos, please send an e-mail to the local organizer Mauro Gaspari (gaspari@cs.unibo.it). Deadline: March 20th.


[M8] _________________________ AMAST Links 03 01

5th International Workshop on Extensions of Logic Programming, ELP'96

Leipzig (Germany), March 28-30, 1996

Update of information in [AL0206CA] .
Call for Participation

The registration fee is 200 DM for non-students and 100 DM for students, payable in cash upon arrival. It includes the proceedings volume (Springer LNAI), which will be available at the beginning of the conference.

Further information concerning the scientific program, travel and accomodation, as well as the registration form can be obtained through the WWW . or by e-mail from:

elp96@informatik.uni-leipzig.de

Roy Dyckhoff, Heinrich Herre, Peter Schroeder-Heister


[M9] _________________________ AMAST Links 03 01

CAAP'96, CC'96, ESOP'96

Linköping, Sweden, 22-26 April 1996

Update of information in [AL0206C5] .

Call for Participation

In cooperation with IFIP

Note: Early registration deadline - March 15

A word-wide-web page containing information about the conferences (Programme, System Demonstrations, Satellite meetings, Accomodation and Registration) is reachable .


[MA] _________________________ AMAST Links 03 01

Int'l Conf. on Information, Statistics & Induction in Science, ISIS'96

Melbourne, Australia, 20-23 August 1996

The full version of this announcement is available.

This conference will explore the use of computational modelling to understand and emulate inductive processes in science. The problems involved in building and using such computer models reflect methodological and foundational concerns common to a variety of academic disciplines, especially statistics, artificial intelligence (AI) and the philosophy of science. This conference aims to bring together researchers from these and related fields to present new computational techniques for supporting or analysing scientific inference and to engage in collegial debate over the merits and difficulties underlying the various approaches to automating inductive and statistical inference. See the full version of this announcement for a list of subject areas of particular interest.

Invited Speakers:

Henry Kyburg, Jr. (University of Rochester, NY)
Marvin Minsky (MIT)
J. Ross Quinlan (Sydney University)
Jorma J. Rissanen (IBM Almaden Research, San Jose, California)
Ray Solomonoff (Oxbridge Research, Mass)

Inquiries to:

isis96@cs.monash.edu.au
David Dowe: dld@cs.monash.edu.au
Kevin Korb: korb@cs.monash.edu.au or
Jonathan Oliver: jono@cs.monash.edu.au

Registration. A registration form will be available at the WWW site quoted below or by mail from the conference chair. Student registration will be available at a discount (but prices have not yet been fixed). Relevant dates are:

Early registration (at a discount): 3 June, 1996
Final registration: 1 July, 1996

More Information is available on the WWW .


[MB] _________________________ AMAST Links 03 01

8th Int'l School for Computer Science Researchers - "Computer Graphics"

Lipari Island, Italy, June 30 - July 13, 1996

Update of information in [AL0208M2] .

Up-to-date information about the Lipari summer school is maintained
on the WWW .

[MC] _________________________ AMAST Links 03 01

TACAS'96 & AIN'96

Tools & Algorithms for the Construction & Analysis of Systems, TACAS'96
2nd Int'l Workshop, Passau (Germany), March 27 - 29, 1996
together with the adjoint
Int'l Workshop on Advanced Intelligent Networks, AIN'96
Passau (Germany), March 25 - 26, 1996

Update of information in [AL0207CB] .
The Final Programs (Postscript) of both meetings are found.

Final program, registration forms and local information on how to reach Passau are available per WWW .

Note: a few extra slots for demos have been made available. Please contact the Local Organizer (tiziana@fmi.uni-passau.de).


[MD] _________________________ AMAST Links 03 01

Practical Appl. of Intelligent Agents & Multi-Agent Technology, PAAM'96

London, UK, Monday 22nd April - Tuesday 23rd April 1996

Update of information in [AL0208C2] .
The Preliminary Program & Registration Form are available.

[ME] _________________________ AMAST Links 03 01

Mathematical Foundations of Programming Semantics, MFPS'96

Boulder, Colorado, USA, June 3-5, 1996

Update of information in [AL0208CC] .
The full version of this announcement is available.

This is the latest update about MFPS 12, the Twelfth Workshop on the Mathematical Foundations of Programming Semantics. The invited speakers for MFPS 12 are:

In addition, there will be one special session during the meeting. This is a workshop year for MFPS, which means that the remainder of the program will be made up of talks by participants. The slots for these talks will be allotted on a first-come, first-served basis.

As with past MFPS Workshops, the Proceedings of the meeting will consist of journal-length papers submitted by participants after the meeting, and dealing with topics relevant to MFPS. These papers will be published as a special issue of Theoretical Computer Science; as such the papers will be refereed to the usual high standards of TCS. More details about this aspect will be provided at the meeting.

Updated information about the meeting can be obtained by accessing the MFPS 12 Home Page .

Those who do not have access to the World Wide Web can obtain updates by sending email to mfps@math.tulane.edu .

Those who are interested in registering for the meeting should complete the registration form included in the full version of this announcement. The form includes an entry to indicate your interest in giving a talk. Registration also can be done on line . (If you have a forms-capable browser.)


[MF] _________________________ AMAST Links 03 01

23rd Int'l Colloquium on Automata, Languages, and Programming, ICALP'96

Paderborn, Germany, July 8th - 12th, 1996

Update of information in [AL0206C8] .
The ICALP'96 Call for Participation & Program is available.

This and further information is available from the ICALP'96 www-server .


[MG] _________________________ AMAST Links 03 01

Third Dutch Specification Day

University of Twente, Enschede, NL, 21 March 1996

The full version of this announcement is available.

The theme of these Days is formal specification in computer science. Both formal techniques and their application in practice are addressed.

The program features four presentations by invited speakers. Material relevant to the presentations will be handed out.

The program (you find a few abstracts at the end of the full version of this announcement):

10.00 - 10.30:
Welcome, coffee
10.30 - 11.30:
Leslie Lamport (DEC Research): Specifying Systems: Some Impious Platitudes
11.30 - 12.30:
Muffy Thomas (University of Glasgow): Formal Specification and Analysis in Safety-Critical Systems
12.30 - 13.45:
Lunch
13.45 - 15.45:
Jean-Raymond Abrial (Independent consultant and researcher): Formal construction of the architecture of a software system, a case study with B.
15.45 - 16.15:
tea/coffee break
16.15 - 17.00:
Klaas Wijbrans (CMG): The BOS project: practical experiences with formal specification.

[MH] _________________________ AMAST Links 03 01

Third Seminar on Algebra, Logic, and Geometry in Informatics, ALGI-3

Keio University, Mita, Tokyo, Japan, April 3-5, 1996

The full version of this announcement is available.

The ALGI (Algebra, Logic, and Geometry in Informatics) seminar is a series of informal peripatetic seminars in Japan (hopefully extending to other areas of Eastern Asia / Oceania) on the interaction between informatics and mathematics.

Information about ALGI seminars can be found.

Information for the third meeting is also available.

The third ALGI meeting will be held as one of the post-conference workshops of Linear Logic 96 (held at Keio University, organized by Prof. Mitsu Okada). The scope of ALGI includes Linear Logic, but is not restricted to it.

We expect offers of talks about informal, half-baked works, as well as completed ones. Participants should fill in the registration form which is given in the full version of this announcement, and send it to

akama@is.s.u-tokyo.ac.jp
The details of the meeting will be announced later in the same place. Some details are in the full version of this announcement. Furthermore: Program/registration/hotel information for Linear Logic 96 . Listing of hotels .

[MI] _________________________ AMAST Links 03 01

Stichting Mathematisch Centrum / Academia Europaea Symp. on Informatics

CWI, Amsterdam, NL, 11 April, 1996
Trippenhuis, Amsterdam, NL, 12 April, 1996

The full version of this announcement is available.

The SMC/AE Symposium on Informatics is organized on the occasion of the 50th anniversary of the Stichting Mathematisch Centrum. The invited speakers are all members of the section on Informatics of the Academia Europaea, which will have a meeting in Amsterdam on April 12th.

The first day of the symposium will be held at the CWI and will highlight developments in fundamental informatics.

The second day will be held at the Trippenhuis (Kloveniersburgwal 29, Amsterdam, home to the Royal Netherlands Academy of Arts and Sciences), and will focus on the importance of informatics research for contemporary society.

Participation is free for everyone interested, though preregistration is required.

The program of the symposium, the registration form, and further information can be found in the full version of this announcement.


[MJ] _________________________ AMAST Links 03 01

BCS FACS Group -- The Seventh Refinement Workshop

Theory and Practice of System Design
University of Bath, England, 3--5 July 1996

Update of information in [AL0207CH]
The Workshop Programme is available.

A prettier version is available on the FACS web site .

The 7th BCS FACS Refinement Workshop will create a forum that discusses developing trends and the the state-of-art in the area of systematic designs. The use of formal techniques in computing systems is increasing rapidly, and providing well-recognized contributions to this field. They have beneficial applications throughout the engineering process, from the capture of requirements through specification, coding and compilation, right down to the hardware which embeds the system into its environment.

The workshop is designed to bring together researchers and practitioners from all areas of system design, and will aim to tackle some of the above issues. It will be a working conference with particular emphasis on participation through discussion.

Invited Speakers

Further information may be obtained from Joan Arnold at:

Email joan@comlab.ox.ac.uk
Tel: +44 (0) 1865 283521, Fax: +44 (0) 1865 273839

Postal Address:
Joan Arnold
Oxford University Computing Laboratory
Wolfson Building, Parks Road, Oxford OX1 3QD, UK


[C1] _________________________ AMAST Links 03 01

Seventh International Conference on Concurrency Theory, CONCUR'96

Pisa, Italy, August 26-29, 1996

Update of the information in [AL0208C6]

The full version of this announcement is available.

The CONCUR conferences aim to bring together researchers, developers and students in order to advance the concurrency theory and promote its applications. This year the proceedings will be published in the Springer LNCS series and it is the intention to dedicate an issue of TCS to CONCUR'96. The topics of interest are shown in the full version of this announcement at the URL given above.

Submissions

Authors are invited to send extended abstracts (in English, up to 15 pages in 12 point) to the PC chairman. Simultaneous submissions to other conferences or journals is not allowed. Electronic submissions are encouraged, in the form of uuencoded compressed PostScript files, sent to concur'96@di.unipi.it. A printed copy should be forwarded by express or courier mail. Otherwise 5 copies of the paper should be sent by express or courier mail to the PC. In both cases, a separate text-only message should be sent to concur'96@di.unipi.it, with a single postal and e-mail address for communication, complete title, author(s), affiliation(s) and 200 word abstract. Prospective authors should read the full version of this announcement at URL given above.

Program Chair:

Ugo Montanari, CONCUR'96, Dipartimento di Informatica,
University of Pisa, Corso, Italia, 40 I-56100 Pisa, Italy

Important Dates

Deadline for submissions: March 4, 1996
Notification of acceptance: May 6, 1996
Camera-ready version due: June 10, 1996

Further Information please send requests and submissions to:

concur'96@di.unipi.it or concur96@di.unipi.it
or view the CONCUR'96 page .

[C2] _________________________ AMAST Links 03 01

9th Int'l Conf. on Theorem Proving in Higher Order Logics, TPHOLs'96

The full version of this Call for Papers is available.

An online version of the call can be found on the WWW.

The 1996 International Conference on Theorem Proving in Higher Order Logics will be the ninth conference in a series dating back to 1988. The Conference will be held on 27-30 August 1996 (Tuesday to Friday) in Turku, in south-west Finland.

Topics. The programme committee welcome submissions on all aspects of theorem proving, particularly those relating to higher order logics or to proof systems based on secure mechanizations of logic. This includes, but is not limited to, the following areas: advances in theorem proving technology; proof automation and decision procedures; applications of mechanized theorem proving; development and extension of higher order logics; comparisons between various approaches to theorem proving; exploitation of external tools within theorem provers; incorporation of theorem provers into larger systems; novel industrial applications of theorem provers.

Submissions are invited in the following categories:

Prospective authors should read the detailed submissions information in the full version of this announcement. Email submissions may be sent to the organizing committee at orgcom@abo.fi. PostScript format is preferred. Papers may also be physically sent to:

Joachim von Wright, Department of Computer Science,
Abo Akademi University, Lemminkaisenkatu 14A,
FIN-20520, Turku, FINLAND
In this case, please include five (5) copies of each paper.

Important Dates


[C3] _________________________ AMAST Links 03 01

Formal Methods in Computer-Aided Design FMCAD'96 - Call for Papers

The full version of this announcement is available.

Formal Methods in Computer-Aided Design '96 is a forum for presenting state-of-the-art tools and techniques based on formal methods for computer-aided design of hardware. The conference location provides excellent opportunities for researchers interact with engineers from Silicon Valley semiconductor and CAD companies. The goal is to cover relevant formal aspects of work in computer-aided system design including verification, synthesis and testing. A special focus of FMCAD'96 will be on the integration of complementary techniques and tools. It is intended to publish the proceedings in time for distribution at the conference in the Springer LNCS series.

Papers: 15 page, 11-point limit with abstract, containing original research in sufficient detail to assess its merits and relevance. Simultaneous submission to other conferences or journals and submission of previously published material are not allowed.

Tutorials: 4 page abstract, 15 page, 11-point for final. We encourage presentations of tools on a suitable set of completely worked out examples.

Submission: in electronically self-contained Postscript to: fmcad96@csl.sri.com. Email submission is strongly encouraged for speeding up the reviewing process. Otherwise, send 7 hard-copies to:

Papers Mandayam Srivas, Re: FMCAD'96, SRI International (EL-262),
333 Ravenswood Ave., Menlo Park, CA 94025, USA.
Email: srivas@csl.sri.com
Tutorials Albert Camilleris, RE: FMCAD'96, Hewlett-Packard Company
M/S 5596, 8000 Foothills Boulevard, Roseville CA 95747-5596, USA.
Email: ac@hprpcd.rose.hp.com

Further Information requests can be directed to vijay@lsil.com or can be found on the WWW site .

Important Dates:

Submission deadline (firm): April 15, 1996
Notification of acceptance: June 17, 1996
Proceedings version of accepted papers due: July 15, 1996

[C4] _________________________ AMAST Links 03 01

First Int'l Workshop on Rewriting Logic and its Applications, RWLW'96

Asilomar Conference Center, Pacific Grove, CA, USA, September 3-6, 1996

The full version of this Call for Papers is available.

Rewriting Logic is a natural semantic framework for concurrency and parallel programming, and for the specification of systems and languages. It has also good properties as a logical framework for representing logics. A growing number of research efforts exploring the application of rewriting logic in all these directions are being carried out worldwide, and several languages based on rewriting logic are being designed and implemented. The Goal of this workshop is to bring together researchers in rewriting logic, from all over the world, to present recent work and discuss future research directions. In addition to time devoted to the presentation of papers, the program will include tutorial and invited presentations, and panel discussions on specific research topics. Papers will be accepted on topics including, but not limited to, the following: foundations, models, and extensions of rewriting logic (RWL); uses of rewriting logic as a logical framework; applications to the specification of languages and systems; applications to object-oriented specification and programming; applications to concurrency and parallel programming; programming languages based on rewriting logic.

Paper Submission The papers will be evaluated by the program committee on the basis of a 2000 word abstract submitted electronically (in postcript format) to the program chair (meseguer@csl.sri.com). The Proceedings will be available at the workshop and will also be made available by ftp. In addition, publication of a book after the workshop collecting papers of the highest technical and/or tutorial significance and that best represent the current state of the art, is being planned.

Important Dates

May 1, 1996: Abstracts due to program chair
June 1, 1996: Registration period begins
June 15, 1996: Notification of acceptance
July 15, 1996: Camera ready copies of full papers due

Further Information. See WWW .


[C5] _________________________ AMAST Links 03 01

20th German Annual Conference on Artificial Intelligence, KI-96

Dresden, Germany, September, 17-19, 1996

The full version of this announcement is available.

The 20th German Annual Conference on Artificial Intelligence, KI-96, will be held at the conference center Dre.Punct and the Technical University at Dresden, Germany. It consists of a scientific and an application track.

The application track comprises several forums and an industrial exhibition. The scientific track consists of invited as well as refereed talks, workshops, posters and system demonstrations. The official languages are German and English.

Topics. We invite you to submit papers, posters as well as system demonstrations on all aspects of artificial intelligence like, for example: knowledge representation, machine learning, and knowledge based systems; reasoning, deduction, inference, and inference systems; diagnosis, classification, planning, and expert systems; cognition and cognitive systems; vision and visual information processing systems; language and natural language processing systems; neural networks and connectionist systems; agents and multi agent systems; humans and robot systems; AI-systems and their sociological implications.

Beside these topics we are particularly interested in contributions covering all aspects concerning the representation of knowledge, from representations within nervous systems to representations within artificial systems.

Important Dates

April, 6th, 1996: submission deadline
May, 5th, 1996: notification of acceptance
June, 6th, 1996: camera ready copies due

Further Information concerning KI-96, including an extended call for papers and information for authors, can be found on the WWW . For any further questions don't hesitate to contact:

Steffen Hölldobler, KI, Informatik, TU Dresden, D-01062 Dresden
ki96@inf.tu-dresden.de

[C6] _________________________ AMAST Links 03 01

Engineering Complex Computer Systems

Maui, Hawaii, January 7-10, 1997
Minitrack @ 30th Annual Hawaii Int'l Conf. on System Sciences, HICSS-30

The Call for Papers for the ECSS minitrack is available.

Papers are invited for the Minitrack on Engineering Complex Computer Systems as part of the Advanced Technology track at the 30th HICSS.

Topics. Papers are solicited on all major aspects of ECCS including specifying, designing, prototyping, building, testing, operating, maintaining, and evolving of complex computer systems. See the Call for Papers quoted above for an extensive list of topics.

Submissions. Papers should be submitted to:

Alberto Broggi, HICSS'97 ECCS Coordinator
Dipartimento di Ingegneria dell'Informazione
Universita` di Parma, Viale delle Scienze, I-43100 Parma, Italy
See the Call for Papers for detailed submission instructions.

Conference Proceedings are published and distributed by IEEE CS.

Further Information about the ECCS Minitrack is available and kept up-to-date on the WWW .

If you wish to receive automatic updates about this event, please send Email to: broggi@CE.UniPR.IT, indicating "ECCS" as subject.

More information on the HICSS-30 Advanced Technology Track: contact

Ralph H. Sprague, Jr.; E-mail: sprague@hawaii.edu
Voice: (808) 956-7082; Fax: (808) 956-9889

See the Call for Papers for information on the other HICSS-30 tracks, or visit the HICSS page .

Important Dates

March 15, 1996:
Abstracts submitted to track coordinators for guidance and indication of appropriate content: authors unfamiliar with HICSS or those who wish additional guidance are encouraged to contact any coordinator to discuss potential papers.
June 1, 1996:
Full papers submitted to (mini)track coordinator.
August 31, 1996:
Notification of accepted papers mailed to authors.
October 1, 1996:
Accepted manuscripts, camera-ready, sent to minitrack coordinator; one author from each paper must register by this time.
November 15, 1996:
All other registrations must be received.

[C7] _________________________ AMAST Links 03 01

3rd Int'l Conf. on Typed Lambda Calculi & Applications, TLCA'97

Nancy, France, 2 -- 4 April 1997

The full version of this announcement is available in two
forms: plain-text and LaTeX respectively.

TLCA'97 will be the third in the TLCA series of conferences, which aims at providing a forum for the presentation and discussion of recent research in areas related to the following

Topics: Type systems for lambda calculi. Proof theory of type systems. Semantics of type systems. Typed lambda calculi. Proof verification via type systems. Type systems of programming languages. Typed term rewriting systems.

The programme of TLCA'97 will consist of about 30 selected presentations in plenary sessions.

Submission. Original contributions for TLCA should be sent to

Roger Hindley, Mathematics Department, University of Wales Swansea
Swansea SA2 8PP, U.K.; e-mail: j.r.hindley@swansea.ac.uk
fax: (+)-44-1792-295843

Electronic submission is preferred (Postscript files only); hard copy (6 copies) is acceptable, at the cost of some delay in communication.

See the full version of this Call for Papers for further submission requirements. A short abstract should be sent as an e-mail with the paper; it should use only standard ASCII characters.

Relevant dates Deadline for submissions : August 30, 1996; Notification of acceptance by : November 11, 1996;

Definitive versions of papers due:
December 6, 1996.

Proceedings. The accepted papers will be published as a volume of the Springer Verlag LNCS, that will be distributed at the conference.

More Information about the conference arrangements will become available later from the Organizing Committee Chairman and Secretary:

P. de Groote, P. Lescanne, INRIA Lorraine,
615 rue du Jardin Botanique, B.P. 101
F-54602 Villers-les-Nancy Cedex, FRANCE
e-mail: Philippe.de.Groote@loria.fr

[C8] _________________________ AMAST Links 03 01

Logical Aspects of Computational Linguistics

Nancy, 23-25 september 1996

The full version of the preliminary call for papers is available in
two forms: plain-text and LaTeX respectively.

There has been a growing interest in the use of logic in natural language processing, both for syntactical and semantical models. Some recent examples include logical deduction as a basis for parsing / generation, the use of non-commutative linear logic as a syntactical model, the relation between categorial grammars, CFG and TAG, natural language interfaces for automatic theorem proving, unification for anaphora resolution, and linear logic semantics for LFG.

This workshop is aimed at bringing together linguists, logicians, philosophers and computer scientists in order to present the latest results in these areas and to discuss the different approaches. See the full version of this announcement for a nonexclusive list of topics

Submissions: Authors are invited to submit before May 31 a 4-page abstract of a paper which has not been submitted elsewhere. The favoured format is electronic submission of a LaTeX, PostScript, dvi or ascii file. Email submissions should be made to retore@loria.fr . Authors can also use surface mail or Fax:

LACL c/o Christian Retore, INRIA-Lorraine & CRIN-C.N.R.S., B.P. 101
615, rue du jardin botanique, 54602 Villers les Nancy cedex, France
Fax: +33 83 27 83 19
After the full papers are refereed, we intend to publish them as a special issue of a journal, or as a volume in some series of lecture notes (this will be made precise in a later announcement).

Schedule: 31 May : 4-page abstract due 14 July : notification of acceptance 23 September : final paper due at the conference

Further information

WWW
contact:
retore@loria.fr, tel: +83 59 20 17

[C9] _________________________ AMAST Links 03 01

IFIP TC6/WG6.1 Joint International Conference FORTE/PSTV'96

Formal Description Technique for
Distributed Systems and Communication Protocols, and
Protocol Specification, Testing, and Verification
Kaiserslautern, Germany, 8-11 October 1996

The FORTE/PSTV'96 2nd Call for Papers is available.

FORTE/PSTV'96 will address Formal Description Techniques (FDTs) applicable to Communication Protocols and Distributed Systems (such as Estelle, Lotos, SDL, ASN.1, TTCN, Z, Automata, Process Algebras, Logics). The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of FDTs, and will provide an excellent orientation for newcomers. Solicited are:

All submissions should be sent to:

Jan Bredereke, University of Kaiserslautern, P.O. Box 3049,
D-67653 Kaiserslautern, Germany, Tel.: +49 631 205-3426
(Reinhard Gotzhein), -3287 (Jan Bredereke), -2640 (Fax),
E-mail: forte.pstv96@informatik.uni-kl.de

Submissions due April 19, 1996

To obtain additional information (Postscript copy of the Call for Papers, keyword list, etc.), you may also browse our WWW pages .


[CA] _________________________ AMAST Links 03 01

Logic Colloquium - 96, LC'96

European Summer Meeting of the Association for Symbolic Logic
Donostia - San Sebastian, Spain, July 9-15, 1996

The Second Announcement is available.

LC'96 is organized by the Institute for Logic, Cognition, Language & Information (ILCLI) and the Dept. of Logic and Philosophy of Science of the University of the Basque Country.

Main topics are: Model Theory, Proof Theory, Recursion and Complexity, Models of Arithmetic, Logic for Artificial Intelligence, Formal Semantics of Natural Language, Philosophy of Contemporary Logic.

Contributed Papers are invited from all areas of Logic. Authors wishing to submit a paper should send two hardcopies of an abstract not more than one page long (about 300 words) written in English to Prof. J.M. Larrazabal (address below), by April 15th, 1996.

Authors of accepted papers are expected to present them at the Colloquium. Abstracts from ASL members will be published as part of the meeting report in The Bulletin of Symbolic Logic.

The registration fee is 28,000 ptas. (35,000 ptas. after 15th April.) (14,000 ptas. for students and accompanying persons; 18,000 ptas. after 15th April.). This fee may be paid from abroad by an international check made out to ILCLI and sent to Prof. J.M. Larrazabal (address below); by way of a bank transfer to ILCLI

account n. 2101038103-10121481,
CAJA GIPUZKOA-DONOSTIA KUTXA,
Garibai 13, 20004 SAN SEBASTIAN, Spain
(please send a copy of your transfer to Prof. J.M. Larrazabal);
or by VISA, EUROCARD or MASTERCARD Credit Cards filling in the authorization form.

Further information may be obtained by writing to

Prof. Jesus M. Larrazabal
LC'96, ILCLI, Univ. of the Basque Country
Apdo. 220. 20080 DONOSTIA - SAN SEBASTIAN, Spain
Tel.: 34 43 320940, Fax: 34 43 293677, E.mail: ilcli@sf.ehu.es
WWW

[CB] _________________________ AMAST Links 03 01

3rd International Conference on High Performance Computing, HiPC'96

Trivandrum, India, December 19-22, 1996

The full version of this announcement is available.

The meeting will emphasize design and analysis of high performance computing systems, and their scientific, engineering, and commercial applications. In addition to technical sessions of contributed paper presentations, the conference will offer invited presentations, tutorials, vendor presentations, and exhibits.

Proposals are solicited for tutorials to be held at the meeting. Interested individuals should submit a proposal by June 3, 1996 to V.K. Prasanna (prasanna@ganges.usc.edu). See the full version of this announcement for details about the proposal.

Companies and R & D laboratories are encouraged to present their exhibits at the meeting. For details, companies are encouraged to contact the Exhibits Co-Chairs by August 31, 1996; contact address information is given in the full version of this announcement.

Authors are invited to submit original unpublished manuscripts that demonstrate current research in all areas of high performance computing including design and analysis of parallel and distributed systems and their applications in scientific, engineering, and commercial areas.

To submit a paper, send a summary of your work (not to exceed ten double spaced pages) to the Program Chair. Electronic submissions should be sent to hipc96@cis.ufl.edu . Hard copy (five copies) and fax (one copy) submissions should be sent to the program committee chair at the address/fax number given below. In addition to the summary, please include a cover page listing your postal address, e-mail address, telephone and fax numbers, and the name and address of the person who will present the work, if accepted.

Updated meeting information can be retrieved from the WWW.

Additional information regarding places of interest in India .

Additional information regarding places of interest in Kerala .

And also .


[CC] _________________________ AMAST Links 03 01

DIMACS Symposium on Teaching Logic and Reasoning in an Illogical World

Rutgers University, 25--26 July 1996

The full version of this announcement is available.

Logic and logical thinking are central to all disciplines and are critical in the mathematical and computer sciences. This symposium will explore the teaching of introductory logic and logical thinking, with a primary focus on the college level and a secondary focus on the high school level. The symposium will be interdisciplinary, emphasizing and contrasting approaches used in mathematics, computer science, natural sciences, and engineering.

The symposium seeks a sharing of ideas, rather than consensus, on how to teach logic, so that all participants gain an appreciation for the fundamental issues and ultimately are better able to motivate the importance of logic and to convey the foundations of logical reasoning to students. Topics of interest include, but are not limited to:

Submit an extended abstract (maximum of 4 pages) by 1 April 1996. Submissions in postscript form are preferred; email them to lmc@cs.cornell.edu. Mail paper submissions to: David Gries, Computer Science, Upson Hall, Cornell University, Ithaca, NY 14853 USA. Notification of acceptance: 1 May. Camera ready and electronic paper versions due: 1 July. Accepted papers will be published in a locally available proceedings and on the World Wide Web.

For further information, contact Peter Henderson, Department of Computer Science, SUNY Stony Brook, Stony Brook, N.Y. 11794-4400 USA. (516) 632-8463, pbh@cs.sunysb.edu.

The symposium will be held prior to the Federated Logic Conference (FLoC) -- for further information, see the FLoC home page .

Info about the Special Year .


[CD] _________________________ AMAST Links 03 01

Journal of Universal Computer Science, Special Issue: Evolving Algebras

Articles are solicited for a Special Issue of JUCS on Evolving Algebras. JUCS is Springer's new electronic journal available world-wide through the internet.

Further information on JUCS, including the format, is available . Or by sending an empty email to JUCS@iicm.tu-graz.ac.at with the following subject: info,format

The volume is going to appear in the Spring of 1997. Following the well established JUCS policy, there will be both an electronic (www accessible) edition of the special issue and a paper edition appearing at the end of the year.

The issue is open to advanced and innovative applications as well as theoretical achievements. Research contributions with cross-disciplinary or research-to-practice content are particularly welcome, including industrial applications, challenging case studies and reports on mature implementations. The area of the submitted paper may belong to any field of computer science or engineering.

Papers must be submitted in 5 hard copies to arrive not later than Dec 1, 1996 at the following address:

Egon Boerger
Dipartimento di Informatica
Universita di Pisa
Corso Italia 40
I - 56 125 PISA/ Italy

The cover page must contain an abstract and the full electronic and ordinary mail address of the corresponding author. An electronic copy in ps-format should be available and be sent in case of specific request.

Each submission will be refereed; the referee reports should be ready at the beginning of February, 1997. In case a paper is accepted under the condition of a revision, there will be a second round of refereeing. The final version, in JUCS format, is due on April 17, 1997 in JUCS format.

For further information contact: boerger@di.unipi.it


[J1] _________________________ AMAST Links 03 01

Associate Professor Positions at Italian Universities

A competition for associate professor positions has been advertised by MURST (Italian Ministery for University and Research). The deadline for application is the 30th April 1996.

Full details are available in italian from the MURST server.

Included on the server are:

Latest information: because of corrections to the official ads, also published in the Official Gazet, the deadline is going to shift to June 1996.


[J2] _________________________ AMAST Links 03 01

Post-Doc Position in Software Engineering

The full version of this announcement is available.

Applications are invited for a one-year definite term Post-Doc position at the Department of Electrical and Computer Engineering of the University of Waterloo. The research of the candidate to fill the position should address the general area of graphical and visual specification methods in the context of object-oriented analysis and design methods for concurrent real-time systems. Candidates should have research experience and/or interest in most of the following areas

An aptitude for programming and knowledge of C++ and/or Smalltalk are desirable. The research will be carried out in close cooperation with a leading Canadian software tool development company (ObjecTime).

To be considered for the position, candidates must have a PhD (or expect to receive one by the start date) in Computer Engineering, Computer Science or a closely related field, and a previous research record of high quality. The start date is flexible but preferably before July 1, 1996. Depending on the availability of funds, the position may be renewable.

Interested candidates should send a cover letter, their C.V. plus names and postal as well as e-mail addresses of at least 2 references as soon as possible, preferably by e-mail, to:

Stefan Leue
Department of Electrical & Computer Engineering
University of Waterloo, Waterloo, Ontario N2L 3G1, Canada
e-mail: sleue@swen.uwaterloo.ca
tel.: +1 519 885 1211 or +1 519 888 4567, extension 5313
fax.: +1 519 746 3077

This advertisement also appears on the WWW page .


[J3] _________________________ AMAST Links 03 01

Research Fellowship in Type Theory and its Appl to Theorem Proving

Department of Computer Science, University of Durham

The full version of this announcement is available.

Applications are invited for a post-doctoral research fellowship funded under the UK EPSRC research project "Subtyping, inheritance and reuse: developing expressive type theory for formal analysis".

The area of work is computer-assisted formal reasoning based on type theory. The project is to develop expressive type theories with subtyping and inheritance mechanisms to support structuring and reuse of formal theories and proofs. The theoretical research results will be incorporated into proof development systems such as Lego and used in application case studies.

The research fellowship is for a period of three years and available from May 1996. The appointment will be on the AR1A scale (starting salary from 15,986 to 18,294 pounds per annum, according to experience). Candidates would normally be expected to have a PhD in computer science or mathematics, or equivalent experience. Experience or background in areas such as constructive type theory, type systems for programming languages, formal proof development, or implementation of theorem provers, is considered to be desirable, though not necessary.

Further details of the research project and related information can be found from the WWW page .

Applications should include a curriculum vitae and names of two referees with their addresses (and email addresses if available). Please send applications or enquiries to

Dr Zhaohui Luo
Dept of Computer Science
The Science Laboratories
South Road, Durham DH1 3LE, U.K.
email: Zhaohui.Luo@durham.ac.uk
tel: +44-(0)191-3743657
fax: +44-(0)191-3742560

[J4] _________________________ AMAST Links 03 01

Software Engineers wanted

C++ / constraint programming / OO / Unix / Brussels

The Service de Mathematiques de la Gestion (SMG) of the Universite Libre de Bruxelles (ULB) is currently looking for software engineers.

The SMG is a department of the Universite Libre de Bruxelles (ULB) devoted to research in Operations Research and Decision Aid Systems. On April 1, 1996, it will start an applied research project in the field of long term human resources scheduling in collaboration with two private companies. This project will involve constraint-based reasoning techniques, object-orientation and advanced GUI design. We are currently looking for flexible software specialists who can perform activities ranging from research, analysis, design and implementation to support and training. These positions offer the opportunity to gather experience with innovative technologies and to apply it to practical problems in the industry.

The applicants will have:

The following skills are also desired:

If you wish to join our team, send your resume. Please, enclose detailed information about your education, work experience, language fluency, expected remuneration, etc. and send to:

Professor Ph. Vincke
Service de Mathematiques de la Gestion
Universite Libre de Bruxelles
Tel. 32 2 650.58.89 / 58.85
Fax. 32 2 650.59.70
e-mail:
pvincke@ulb.ac.be

[J5] _________________________ AMAST Links 03 01

Postdoctoral Research Associate: Logic in Computer Science

There is a position beginning in September 1996 and possibly earlier, for a postdoctoral research associate with an interest in logic in computer science at Brandeis University.

The successful applicant will be a researcher with interests in programming language theory, including lambda calculus, optimal evaluation, linear logic, games semantics, type theory, constructive mathematics, continuations, and functional programming. Some programming aptitude and an interest in algorithmics would be a good thing.

Given that broad outline and general focus, the person would obviously have an open agenda to pursue whatever research topics he or she found interesting.

The term of this appointment would be for one year, with an extension for a following year contingent upon funding.

Candidates should contact Prof. Mairson by email, and include a vita with the email addresses of at least two references.

Harry Mairson
Associate Professor
Computer Science Department
Brandeis University
Waltham, Massachusetts 02254
email: mairson@cs.brandeis.edu
WWW

[J6] _________________________ AMAST Links 03 01

M.Sc. in Logic and Foundations of Programming

Queen Mary and Westfield College University of London

The full version of this announcement is available.

Applications are invited for places on this newly designed M.Sc. programme (part of the Dept's. Advanced Methods in Computer Science M.Sc.) which aims to allow mathematically able students to acquire a thorough grounding in the logical foundations of computer science and the theory and practice of programming.

Candidates should have, or expect to obtain, a good first degree either in mathematics or in a subject having substantial mathematical content, together with a basic acquaintance with computing. Good graduates in computer science or philosophy will also be considered, provided they have adequate mathematical aptitude.

A small number of EPSRC studentships will be available for suitably qualified eligible candidates.

The programme will be taught by members of the College, including: Prof. Richard Bornat; Dr. Peter Burton; Dr. Keith Clarke; Dr. Peter O'Hearn; Prof. Wilfrid Hodges; Prof. Peter Landin; Dr. David Pym; Prof. Edmund Robinson; Mr. Jon Rowson; Dr. Victoria Stavridou; Dr. Paul Taylor.

More information from

Ms. Gill Carter
Department of Computer Science
Queen Mary and Westfield College
University of London
Mile End Road
London E1 4NS, U.K.
Tel: +44 (0)171 975 5555, Fax : +44 (0)181 980 6533
Email: gill@dcs.qmw.ac.uk
WWW

[J7] _________________________ AMAST Links 03 01

Ph.D. Studentships in Knowledge Representation and Reasoning

Department of Computer Science, Queen Mary and Westfield College

Applications are invited from students wishing to pursue research leading to a Ph.D. in the area of Knowledge Representation & Reasoning.

Suitable Ph.D. topics include: nonmonotonic logics (particular logics, general frameworks, properties of nonmonotonic consequence relations, model-based implementation), commonsense causal reasoning (using formalisms such as the Situation Calculus, the Event Calculus, and nonmonotonic temporal logics), and reasoning about the mental states of agents (using non- monotonic and modal logics to represent beliefs, desires, intentions, obligations, persistence, commitment and rationality).

Candidates should have a good first degree in an appropriate subject, such as Computer Science or Mathematics. Good graduates in Philosopy will also be considered, provided they have an appropriate background in formal logic. Normally, candidates are required to have an appropriate master's degree, although exceptions are possible.

Suitably qualified eligible candidates will be nominated for EPSRC, departmental or college awards. Graduate Teaching Studentships may also be available.

Further information can be obtained from:

Ms. Carla Benjamin
Department of Computer Science
Queen Mary and Westfield College
University of London
Mile End Road
London E1 4NS, U.K.
Tel: 0171 975 5225, Fax: 0181 980 6533
Email: carla@dcs.qmw.ac.uk
WWW

[J8] _________________________ AMAST Links 03 01

Assistant Professor in Information Systems

Creighton University invites applications for a tenure-track, assistant professor position in the Information Systems and Technology Department, College of Business Administration, beginning August, 1996. A doctoral degree in the field of Information Systems and expertise in telecommunications and systems integration is required. Demonstrated excellence in teaching and a potential for quality research are expected. Applicants should provide a resume and a list of three references to Dr. John Gleason, Search Committee, College of Business Administration, Creighton University, Omaha, NE 68178. E-mail: jgleas@creighton.edu. Phone (402) 280-2624, fax (402) 280-2172.

Evaluation of applications will begin March 1 and will continue until the position is filled. An Affirmative Action, Equal Opportunity employer. Women and minorities are encouraged to apply.


[J9] _________________________ AMAST Links 03 01

Executive Director

Creighton University Institute for Information Technology & Management

Creighton University Institute for Information Technology and Management has been newly founded to deliver technology and management development needs of the regional business community. The Institute will be a leading source of engineering education, offered through NTU (National Technical University), and technology skills and management development programs. Principal near-term objectives are aggressive market penetration in technology and management training, and start up and roll out of major new initiatives customized to corporate needs.

This is a challenging, high-energy position involving commitment to prompt, high-quality service. The ideal candidate will be a dynamic, nationally recognized individual with a track record of leading the design and implementation of technology-based solutions in business organizations.

Key elements of this position include an insightful understanding of existing and emerging information technologies, entrepreneurship, strong interpersonal communication skills, relationships management, marketing, project management, and consulting.

An attractive competitive base compensation, incentive plan, and benefits package consistent with the candidate will be negotiated.

Please forward, in confidence, a resume and cover letter to:

Dr. Vasant Raval, Acting Director
The Creighton University Institute for IT and Management
College of Business Administration
Creighton University
2500 California Plaza
Omaha, NE 68178
Fax: (402) 280-2172 Phone: (402) 280-2342
E-mail: vraval@creighton.edu
Creighton University is an Equal Opportunity Employer

[JA] _________________________ AMAST Links 03 01

Formal Verification job openings

General Systems Lab - Hewlett-Packard Company, Roseville, California

The full version of this announcement is available.

The General Systems Laboratory of Hewlett-Packard is again hiring verification engineers with skills and interests in Formal Verification. Successful applicants will join a small-but-growing team whose charter is to apply Formal Methods to a variety of computer system design problems. This is an opportunity to develop formal techniques which will have genuine impact on the computer industry.

Requirements:

In addition to the above requirements, previous experience in some of the following areas is preferred:

For immediate consideration, email your resume to:

fvjobs@rosemail.rose.hp.com

Hewlett-Packard is an equal employment opportunity employer dedicated to affirmative action and workforce diversity.


[JB] _________________________ AMAST Links 03 01

Visiting Researcher in Real-time Systems

University of Uppsala, Sweden

The position is intended for two years. We seek applicants with a PhD, a research record and interest in one or several of the following areas:

Additional information is available .

Interested? Please send CV and state your interests and requirements by e-mail, fax or physical mail to Hans Hansson.

Hans Hansson E-mail: hansh@docs.uu.se
Dept. of Computer Systems (DoCS)
P.O. Box 325
S-751 05 Uppsala
Sweden
tel@DoCS +46 18 183155, switchb. +46 18 182500
tel@home +46 18 429974, fax@DoCS +46 18 550225
mobile +46 70 7527785

[L1] _________________________ AMAST Links 03 01

The Topological Structure of Asynchronous Computability

by Maurice Herlihy and Nir Shavit
Brown University Computer Science Dept. Technical Report CS96-03

The abstract and links to a postscript version of this paper are available .

This is the long-awaited technical report version of the STOC 93 and 94 papers on the application of algebraic topology to distributed computing, now with proofs.


[L2] _________________________ AMAST Links 03 01

Categories for computation in context and unified logic: I

by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely

This paper introduces the notion of contextual categories. These provide a categorical semantics for the modelling of computation in context, based on the idea of separating logical sequents into two zones, one representing the context over which the computation is occurring, the other the computation itself. The separation into zones is achieved via a bifunctor equipped with a tensorial strength. We show that a category with such a functor can be viewed as having an action on itself. With this interpretation, we obtain a fibration in which the base category consists of contexts, and the reindexing functors are used to change the context.

We further observe that this structure also provides a framework for developing categorical semantics for Girard's Unified Logic, a key feature of which is to separate logical sequents into two zones, one in which formulas behave classically and one in which they behave linearly. This separation is analogous to the context/computation separation above, and is handled by our semantics in a similar fashion. Furthermore, our approach allows an analysis of the exponential structure of linear logic using a tensorially strong action as the primitive notion. We demonstrate that from such a structure one can recover a model of the linear storage operator.

Finally, we introduce a sequent calculus for the fragment of Unified Logic modeled by contextual categories. We show cut elimination for this fragment, and we introduce a simple notion of proof circuit, which provides a description of free contextual categories.

The paper is available .


[L3] _________________________ AMAST Links 03 01

Enrichment and Representation Theorems

for Categories of Domains and Continuous Functions
by Marcelo P. Fiore, Dep't of Computer Science, LFCS, U. of Edinburgh

Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. We prove an enrichment theorem showing that every axiomatic domain-theoretic category can be endowed with an intensional notion of approximation, the path relation, with respect to which the category Cpo-enriches. Subsequently, we provide a representation theorem of the form: every small domain-theoretic category (with a lifting monad) has a full and faithful representation in a domain-theoretic category of cpos and continuous functions (with a lifting monad) in a suitable intuitionistic set theory.

Our analysis suggests more liberal notions of domains. In particular we present a category where the path order is not omega-complete, but in which the constructions of domain theory (as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are possible.

This preprint is available in the files rep.dvi and rep.ps.


[L4] _________________________ AMAST Links 03 01

Formal Verification of Algorithm W: The Monomorphic Case

Dieter Nazareth and Tobias Nipkow

A formal verification of the soundness and completeness of Milner's type inference algorithm W for simply typed lambda-terms is presented. Particular attention is paid to the notorious issue of "new" variables. The proofs are carried out in Isabelle/HOL, the HOL instantiation of the generic theorem prover Isabelle.

The paper documents HOL's subtheory MiniML and is available .


[L5] _________________________ AMAST Links 03 01

Partial-Order Methods for the Verification of Concurrent Systems

An Approach to the State-Explosion Problem
Patrice Godefroid

This PhD thesis is now available in revised form as volume 1032 of Lecture Notes in Computer Science, Springer-Verlag, January 1996, ISBN 3-540-60761-7 (foreword by Pierre Wolper).


[T1] _________________________ AMAST Links 03 01

Coq Proof Assistant, Version 5.10.15

The full version of this announcement is available.

We are glad to announce the release of version 5.10.15 of the Coq Proof Assistant for the Calculus of Inductive Constructions. This release includes various changes in the code and libraries, which are described more precisely below. The documentation has also been updated.

Coq V5.10.15 comes in two flavors: the regular Coq, and a new, fully up-to-date and compatible distribution of Ct-Coq (i.e. Coq with a sophisticated graphical user-interface).

The www page is available .

As usual, you might send problems, bug reports, remarks about the installation to coq@pauillac.inria.fr and more general questions about the coq system to the mailing list coq-club@pauillac.inria.fr. Questions specific to the Ct-Coq interface should be addressed to ctcoq-request@sophia.inria.fr.

Enjoy!


[P1] _________________________ AMAST Links 03 01

Problem: Deciding 2-nested simulation between processes

Does anyone know of an algorithm for deciding 2-nested simulation relation (defined by Groote and Vaandrager) between finite state processes?

Sandeep Shukla has an algorithm that has time complexity quadratic in the size of the transition relations of the transition systems. He would appreciate it if someone could point to any other algorithm for solving this problem.

Sandeep needs to refer to this in a survey he is writing now.

Please email replies to sandeep@cs.albany.edu


[S1] _________________________ AMAST Links 03 01

Proceedings of the Third AMAST Workshop on Real-Time Systems

Salt Lake City, Utah, USA; March 6-8, 1996

Update of information in [AL0208M1] .

Proceedings are available for the Third AMAST Workshop on Real-Time Systems -- the program was made available last week, also in LaTeX form .

For information about the Proceedings, please contact:

Prof. Dan Ionescu
Room A513, Colonel By Hall
770 King Edward Avenue
Department of Electrical Engineering
University of Ottawa
Ottawa, Ontario, CANADA K1N 6N5
Tel: (613)-562-5800 x 6209, or 6236
Fax: (613)-562-5175
e-mail: ionescu@trix.genie.uottawa.ca
or: dan@gemini.genie.uottawa.ca
or: ionescu@elg.uottawa.ca

This announcement is also available on the WWW .


[S2] _________________________ AMAST Links 03 01

FLIRTS WWW page moved

Update of [AL0208S3]

Due to some rearrangement in our file system, the flirts pages are now reachable (hopefully) again on WWW .

Please let me know if you have problems accessing it (or the local pages linked to it).

Please send comments, suggestions and complaints directly to me, thanks,

Maura (cerioli@disi.unige.it).


[S3] _________________________ AMAST Links 03 01

VISUAL'96 WWW page, 1st Int'l Conf. on Visual Information Systems

Update of information in [AL0208M1]
The full version of this announcement is available.

With the widespread use of multimedia information, there is a pressing requirement to efficiently manage, store, manipulate and retrieve images and pictorial data in a wide spectrum of applications. As many organisations currently maintain large collections of images, the need for flexible visual information management is already critical. Future information systems in commercial and scientific applications will have a high visual content, and it is necessary to integrate the visual and image components into the architecture of organisational information systems. Such visual components will tend to permeate all information systems and in time will not be regarded as a distinct element, but will form an essential part of any information system, working alongside and in harmony with structured information processing components.

The conference focused attention on the management of visual information. Over 50 papers have been presented by authors from Australia, Austria, China, Finland, France, Germany, Hong Kong, India, Italy, Japan, New Zealand, the Netherlands, Singapore, UK and USA.

For more information see VISUAL'96 WWW page .


[S4] _________________________ AMAST Links 03 01

New e-mail list on Software Verification

This is to announce a new software verification e-mail list.
I and a number of people I have met are interested in formal verification of software, but I have not found any newsgroups or e-mail lists devoted exclusively to it. To help, I created a mailing list where people can discuss issues related to proving programs. To join the list, send e-mail to majordomo@lal.cs.byu.edu. The subject doesn't matter. The body must contain the line
subscribe softverf
You should get an automatic response within about an hour.
Soon I will create some World Wide Web pages with references and
resources related to software verification.
Paul E. Black 's home page can be visited.

[A1] _________________________ AMAST Links 03 01

New items in AMAST repository at CS Faculty of University of Twente

<location> := http://www.cs.utwente.nl/data/amast/
<location> := ftp://ftp.cs.utwente.nl/pub/doc/amast/
Date: 21/03/1996
Contents: Index.html, README, amast96/, workshops/, info/, links/,
sigala/, amast95/, amast93/, amast91/
amast96/:
AMAST'96 Conference: Preliminary Program, ...
Contents:
PrelProg.txt, ...
workshops/:
AMAST Workshops: Contents : ...
AMAST-RTW96-Proc.txt AMAST-RTW96-Prog.txt, AMAST-RTW96-Prog.tex
info/ :
records of communication onto the AMAST mailing list
Contents:
..., ady03/, caad/, ...
ady03/ :
digests of messages sent onto the AMAST mailing list in 1996; two digests are available:
  • last digest of messages distributed on the list
  • cumulative annual digest for the current year
Contents:
ADY03N02 [01/03/1996--10/03/1996]
CAADY03 [01/01/1996--10/03/1996]
caad/ :
cumulative annual digests of messages sent onto the AMAST mailing list during previous years:
Contents:
...
CAADY02 [01/01/1995--31/12/1995]
links/ :
AMAST newsletter
Contents:
AL-Index.html, v03/, ...
Note :
The file AL-Index.html provides WWW users with links to individual issues of the AMAST newsletter (...)
v03/ :
third volume of AMAST Links (1996)
Contents:
i01/
i01/ :
AMAST Links Vol. 03, Issue 01 [21/03/1996]
full/

[A2] _________________________ AMAST Links 03 01

This issue

was edited by Giuseppe Scollo, Michael Johnson, Edmund Kazmierczak, Giancarlo Ruffo and Elena Trichina, thanks to contributions by:
[M1] Bernhard Reus <reus@informatik.uni-muenchen.de>
[M2] Wiebe van der Hoek <wiebe@cs.ruu.nl>
[M3] Diego Latella <d.latella@cnuce.cnr.it>
[M4] Geert-Jan M. Kruijff <gj@ufal.ms.mff.cuni.cz>
[M4] Marco W. de Vries <marco@fwi.uva.nl>
[M5] Dagmar Harmancova <dasa@uivt.cas.cz>
[M6] Mehmet Orgun <mehmet@macadam.mpce.mq.edu.au>
[M7] Roberto Gorrieri <gorrieri@cs.unibo.it>
[M7] Mauro Gaspari <gaspari@cs.unibo.it>
[M7] Nadia Busi <busi@cs.unibo.it>
[M8] Peter Schröder-Heister <psh@hume.Informatik.Uni-Tuebingen.De>
[M9] Helene Kirchner <Helene.Kirchner@loria.fr>
[MA] Jonathan Oliver <jono@cs.monash.edu.au>
[MB] Alfredo Ferro <ferro@dipmat.unict.it>
[MC] Tiziana Margaria <tiziana@fmi.uni-passau.de>
[MD] Al Roth <alroth@pap.com>
[ME] Michael W. Mislove <mwm@math.tulane.edu>
[MF] Rolf Wanka <wanka@uni-paderborn.de>
[MG] Rom Langerak <langerak@cs.utwente.nl>
[MH] Akama Youji <akama@is.s.u-tokyo.ac.jp>
[MI] Frans Snijders <Frans.Snijders@cwi.nl>
[MJ] John Cooke <D.J.Cooke@lut.ac.uk>
[C1] Ugo Montanari <ugo@DI.Unipi.IT>
[C2] Jim Grundy <jim.grundy@abo.fi>
[C3] Mandayam Srivas <srivas@csl.sri.com>
[C4] Burgess <burgess@csl.sri.com>
[C5] Steffen Hölldobler <sh@inf.tu-dresden.de>
[C6] Alberto Broggi <broggi@CE.UniPR.IT>
[C7] Andrew Pitts <Andrew.Pitts@cl.cam.ac.uk>
[C8] Christian Retore <Christian.Retore@loria.fr>
[C9] FORTE-PSTV'96 <forte@informatik.uni-kl.de>
[CA] Jesus M. Larrazabal <ilcli@sf.ehu.es>
[CB] D. Jayasimha <jayasim@cis.ohio-state.edu>
[CC] Barbara Quigley <bquigley@dimacs.rutgers.edu>
[CD] Egon Boerger <Egon.Boerger@zfe.siemens.de>
[J1] Eugenio Moggi <moggi@disi.unige.it>
[J2] Stefan Leue <sleue@swen.uwaterloo.ca>
[J3] Zhaohui Luo <Zhaohui.Luo@durham.ac.uk>
[J4] Ph. Vincke <pvincke@ulb.ac.be>
[J5] Harry Mairson <mairson@cs.brandeis.edu>
[J6] Gill Carter <gill@dcs.qmw.ac.uk>
[J7] Carla Benjamin <carla@dcs.qmw.ac.uk>
[J8] Chang-Shyh Peng <cspeng@creighton.edu>
[J9] Chang-Shyh Peng (see [J8])
[JA] Albert Camilleri <ac@gslxsrv1.rose.hp.com>
[JB] Hans Hansson <hansh@Mizar.DoCS.UU.SE>
[L1] Maurice Herlihy <mph@cs.brown.edu>
[L2] Robert A.G. Seely <rags@triples.Math.McGill.CA>
[L3] Marcelo Fiore <mf@dcs.ed.ac.uk>
[L4] Tobias Nipkow <nipkow@sunbroy14.informatik.tu-muenchen.de>
[L5] Patrice Godefroid <god@graceland.ih.att.com>
[T1] Gerard Huet <Gerard.Huet@inria.fr>
[P1] Sandeep Kumar Shukla <sandeep@cs.albany.edu>
[S1] Dan Ionescu <ionescu@elg.uottawa.ca>
[S2] Maura Cerioli <cerioli@disi.unige.it>
[S3] Zheng Zhi Jie <zheng@matilda.vut.edu.au>
[S4] Paul E. Black <black@leopard.cs.byu.edu>

This issue of AMAST Links is available in four forms:

Note: This issue will also be available, in all of its four forms, by anonymous ftp from the AMAST repository at the University of Twente. File names will be the same as above, but under the ftp directory .