[ToC] ==================\============================ AMAST Links 03 01 _____________________ \ / _____________________ Contributions are / \ AMAST Links / \ 21 March 1996 welcome! e-mail to ( / \ ) e-mailed to: amast@cs.utwente.nl \ / Vol. 03 Issue 01 \ / 822 subscribers ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ An index to all issues of the AMAST newsletter is available on the WWW: URL: http://www.cs.utwente.nl/data/amast/links/AL-Index.html A general index to AMAST information on the WWW server in Twente is at: URL: http://www.cs.utwente.nl/data/amast/Index.html The hypertext version of this issue is available at: URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/AL0301-ToC.html _________________ 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"at, M"unchen, Germany, July 1-5, 1996 *Update* of information in [AL0208C1]. The _AMAST'96 Preliminary Program_ is available at URL: http://www.cs.utwente.nl/data/amast/amast96/PrelProg.txt o The registration forms will be sent soon. o A WWW page containing information about the conference is reachable at URL: http://www.pst.informatik.uni-muenchen.de/amast96 o e-mail: amast96-info@informatik.uni-muenchen.de [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301M2.txt [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: o On the _workshop_, at URL: http://fdt.cnuce.cnr.it:8080/Home/fm-ercim/workshop.html o On the _working group_, at URL: http://fdt.cnuce.cnr.it:8080/Home/fm-ercim/WgDescription.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301M4.txt 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: 0. A _reminder_ (*Note:* last-minute contribution to this AL issue); 1. The programme of ESSLLI'96, given for each of the six areas above; 2. The ESSLLI'96 Student Session; 3. Local information: ESSLLI'96 site, accommodation, social events. Further information can be found at the _ESSLLI'96 Website_, at URL: http://ufal.ms.mff.cuni.cz [M5] ================================================ AMAST Links 03 01 Logical Foundations of Mathematics, Computer Sci. & Physics, GOEDEL'96 Kurt G"odel's Legacy Brno (birthplace of Kurt G"odel), Czech Republic, August 25-29, 1996 *Update* of information in [AL0207CN]. The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301M5.txt The conference announcement gives new information about the following items, among others: o Sponsors o Invited Speakers o Contact Addresses o Registration Form _Up-to-date information_ is maintained on the WWW, at the URL: http://www.fi.muni.cz/~zlatuska/goedel96.html 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 , 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301M6.txt 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 at URL: http://lu.eas.asu.edu/islip96.html [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_ at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301M7.txt _Final program, registration forms and local information_ on how to reach Cesena are available per WWW at URL: http://www.radio.alma.unibo.it/coordination96/index.html *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 at URL: http://www-theory.dcs.st-and.ac.uk/elp96.html 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"oping, Sweden, 22-26 April 1996 *Update* of information in [AL0206C5]. *Call for Participation* o European Symposium on Programming (ESOP'96) : 22--24 April o Colloquium on Trees in Algebra and Programming (CAAP'96) : 22--24 April o International Conference on Compiler Construction (CC'96) : 24--26 April 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_ at URL: http://www.ida.liu.se/activities/conferences/CAAP-CC-ESOP96/ [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MA.txt 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 at URL: http://www.cs.monash.edu.au/~jono/ISIS/ISIS.shtml [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, at URL: http://www.unict.it/lipari/home.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MC.ps Final program, registration forms and local information on how to reach Passau are available per WWW under URL: http://www.uni-passau.de/fmi/lehrstuehle/steffen/cfp/ *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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MD.txt [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301ME.txt 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: o Peter Freyd (Penn), o Mel Fitting (CUNY), o Matthew Hennessy (Sussex), o Gerard Huet (Inria), o Andre Scedrov (Penn) and o Jeannette Wing (CMU). 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_, at URL: http://www.math.tulane.edu/mfps12.html 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_, at the URL: http://www.math.tulane.edu/regform.html (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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MF.txt This and further information is available from the _ICALP'96 www-server_ at URL: http://www.uni-paderborn.de/~icalp96/ [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MG.txt 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MH.txt 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 at URL: http://www.etl.go.jp:8080/People/yoshiki/ALGI-e.html _Information for the third meeting_ is also available, at URL: http://nicosia.is.s.u-tokyo.ac.jp/~akama/algi3.html 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_ at URL: http://abelard.flet.mita.keio.ac.jp/person/linear96/Linear96.html _Listing of hotels_ at URL: http://abelard.flet.mita.keio.ac.jp/person/linear96/hotel.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MI.txt 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301MJ.txt A prettier version is available on the _FACS web site_ at URL: http://facs.lut.ac.uk/ 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* o C.A.R. Hoare (Oxford University, UK) o R.A. Back (Abo Akademi University, Finland) o B. Moszkowski (University of Newcastle, UK) o C.C. Zhou (University of United Nations, Macau) *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 at the URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C1.tex 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_ at the URL: http://www.di.unipi.it/~ugo/CONCUR96.html [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 at the URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C2.txt An _online version of the call_ can be found on the WWW at URL: http://www.abo.fi/~jharriso/cfp.html 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: o Category A: Full research paper; o Category B: Informal progress report. 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* o Deadline for category A submissions: 15 March 1996 o Deadline for category B submissions: 14 April 1996 o Notification of acceptance: 30 April 1996 o Camera-ready copy for category A due (provisional): 14 June 1996 [C3] ================================================ AMAST Links 03 01 Formal Methods in Computer-Aided Design FMCAD'96 - Call for Papers The full version of this announcement is available at the URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C3.txt 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_ at URL: http://www.csl.sri.com/FMCAD96 *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 at the URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C4.txt 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 at URL: http://www.csl.sri.com/RWLW96 [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C5.txt 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 at URL: http://pikas.inf.tu-dresden.de/ki96/ki96.html For any further questions don't hesitate to contact: Steffen H"olldobler, 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C6.txt 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 at URL: http://WWW.CE.UniPR.IT/hicss/eccs 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_ at URL: http://www.cba.hawaii.edu/hicss *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 (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C7.? 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 (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C8.? 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 : http://www.loria.fr/~retore/LACL.html 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301C9.txt 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: o Full original research papers and industrial usage reports, 5 copies, up to 16 pages, 12 point, single spaced,including an informative abstract as well as names and affiliations of all authors, and a list of keywords. o A cover letter naming a contact author (including postal and E-mail address) and indicating the preferred category (research paper or industrial usage report) in which the paper should be considered, is required. The cover letter should also state that the paper has not been presented in any language at another conference nor is it currently being considered by another conference or by a journal; furthermore it should state that, in case of acceptance, one of the authors will attend FORTE/PSTV'96 and present the paper. o Proposals for tool demonstrations and poster displays. o Proposals for tutorials and advanced technology seminars. 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_, at URL: http://www.informatik.uni-kl.de/aggotz/forte.pstv96 [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301CA.txt 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 : http://www.sc.ehu.es/scrwwwil/lc-96.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301CB.txt 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 at URL: http://www.usc.edu/dept/ceng/prasanna/home.html Additional information regarding _places of interest in India_ at URL: http://hulk.bu.edu/misc/india/ Additional information regarding _places of interest in Kerala_ at URL: http://www.cs.cmu.edu/afs/cs/user/vipin/www/kerala.html And _also_ at URL: http://www.granada.com/kerala/map/ [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301CC.txt 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: o Pedagogical Approaches o Empirical Studies o Cognitive Models of Logical Reasoning o Exemplary Course Material o Innovative Approaches o Courseware for Teaching Logic 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 at URL: http://www.research.att.com/lics/floc/ Info about the _Special Year_ at URL: http://dimacs.rutgers.edu/ [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 at URL: http://www.iicm.tu-graz.ac.at/jucs 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 at URL: http://sirio.cineca.it/murst-diu/ Included on the server are: o text of the ads published on the GU (Official Gazet), o positions available (e.g. 68+49 in CS, 174 in math. disciplines) o sample application (for italian and foreigners) 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301J2.txt 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 o Formal specification techniques for concurrent distributed systems. o Object-Oriented Software Engineering. o Visual spec techniques, in particular Message Sequence Charts. o CASE tools. o Specification of real-time requirements. 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 at URL: http://swen.uwaterloo.ca/~sleue/postdoc.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301J3.txt 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 at URL: http://www.dur.ac.uk/~dcs0zl/sir.html 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: o a degree or PhD in Computer Science or a related topic o a good knowledge of Unix, C++, object-oriented design and analysis o a strong interest in problem-solving software o significant work experience in software development (>= 2 years) o good communication skills in at least two of English, Dutch, French The following skills are also desired: o experience in constraint-based reasoning or related AI techniques o knowledge of ILOG SOLVER and ILOG VIEWS C++ class libraries o experience in scheduling systems and combinatorial problems o knowlegde of RDBMS 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 : http://www.cs.brandeis.edu/~mairson [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301J6.txt 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 : http://www.dcs.qmw.ac.uk/ [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 : http://www.dcs.qmw.ac.uk/ [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301JA.txt 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: o BS, MS or Ph.D degree in EE, CE, CS, CEE or CSEE. o Experience in one of the following areas: VLSI, Firmware, board design or system simulation. o Solid understanding of computer architecture. o Minimum 3 years experience in formal verification. o Strong communication and teamwork skills. o Must be flexible and willing to work in areas other than FM. In addition to the above requirements, previous experience in some of the following areas is preferred: o Integrated circuit design, verification, tools and methodologies. o VLSI testing, characterization, diagnostics. o CPU board design. o RISC Assembly language programming, C programming. o Behavioural modeling. o Industrial use of Formal Methods. 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: o Real-Time Scheduling (theory and practical applications) o Real-Time Networking o Execution Time Analysis o Methods for Real-Time System Software Development o Distributed Real-Time Systems o Real-Time System Analysis and Verification Additional information is available at URL: http://www.docs.uu.se/docs/hrts/visres96.html 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 via URL: http://www.cs.brown.edu:80/people/mph/HS96.html 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 via URL: ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html [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 from URL: http://www.dcs.ed.ac.uk/home/mf 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 via URL: http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W0.html [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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301T1.txt 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 at URL: http://www.inria.fr/croap/ctcoq/ctcoq-eng.html 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, at URL: http://www.cs.utwente.nl/data/amast/workshops/AMAST-RTW96-Prog.txt also in _LaTeX form_ at URL: http://www.cs.utwente.nl/data/amast/workshops/AMAST-RTW96-Prog.tex 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 at URL: http://www.cs.utwente.nl/data/amast/workshops/AMAST-RTW96-Proc.txt [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 at URL: http://www.disi.unige.it/faculty/cerioli/www/flirtshome.html 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 at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/full/AC0301S3.txt 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 at URL: http://www.vut.edu.au/~visual96 [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 at URL: http://lal.cs.byu.edu/people/black/black.html [A1] ================================================ AMAST Links 03 01 New items in AMAST repository at CS Faculty of University of Twente := http://www.cs.utwente.nl/data/amast/ := 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: o ... o 3rd AMAST Workshop on Real-Time Systems, ARTS'96 (Proceedings Information, Final Program) 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: o last digest of messages distributed on the list o 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 [M2] Wiebe van der Hoek [M3] Diego Latella [M4] Geert-Jan M. Kruijff [M4] Marco W. de Vries [M5] Dagmar Harmancova [M6] Mehmet Orgun [M7] Roberto Gorrieri [M7] Mauro Gaspari [M7] Nadia Busi [M8] Peter Schr"oder-Heister [M9] Helene Kirchner [MA] Jonathan Oliver [MB] Alfredo Ferro [MC] Tiziana Margaria [MD] Al Roth [ME] Michael W. Mislove [MF] Rolf Wanka [MG] Rom Langerak [MH] Akama Youji [MI] Frans Snijders [MJ] John Cooke [C1] Ugo Montanari [C2] Jim Grundy [C3] Mandayam Srivas [C4] Burgess [C5] Steffen H"olldobler [C6] Alberto Broggi [C7] Andrew Pitts [C8] Christian Retore [C9] FORTE-PSTV'96 [CA] Jesus M. Larrazabal [CB] D. Jayasimha [CC] Barbara Quigley [CD] Egon Boerger [J1] Eugenio Moggi [J2] Stefan Leue [J3] Zhaohui Luo [J4] Ph. Vincke [J5] Harry Mairson [J6] Gill Carter [J7] Carla Benjamin [J8] Chang-Shyh Peng [J9] Chang-Shyh Peng (see [J8]) [JA] Albert Camilleri [JB] Hans Hansson [L1] Maurice Herlihy [L2] Robert A.G. Seely [L3] Marcelo Fiore [L4] Tobias Nipkow [L5] Patrice Godefroid [T1] Gerard Huet [P1] Sandeep Kumar Shukla [S1] Dan Ionescu [S2] Maura Cerioli [S3] Zheng Zhi Jie [S4] Paul E. Black This issue of AMAST Links is available in four forms: o a collection of hypertext files, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/AL0301-ToC.html for the ToC-page, where links give access to individual pages; o a single hypertext file, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v03/i01/AL0301.html o a collection of plain-text files, one per page, each separately available (+) (see below) o a single plain-text file available by e-mail as well as (+) within the AMAST directory of the Twente WWW server, at URL http://www.cs.utwente.nl/data/amast/links/v03/i01/AL0301.txt where `' is either `-ToC' (for the ToC-page),or the 2-character page identifier (for one-page files), or empty (whole-issue file). *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_ at URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/links/v03/i01/ [end] =============================================== AMAST Links 03 01