Comments are welcome!
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _
date : 7 November 1994
e-mail to: amast@cs.utwente.nl
________________________
e-mailed to : 325 subscribers
The full version of this preliminary announcement is available.
The Workshop on Logic, Domains, and Programming Languages is aimed at computer scientists and mathematicians alike, who share an active interest in the mathematical foundations of computer science. The scope of the workshop encompasses all aspects of Programming Language Semantics ranging from purely theoretical topics to concrete applications and implementations of semantic methods. Possible workshop topics are, for example, Lambda Calculi and Functional Programming, Domain Theory, Denotational and Algebraic Semantics, Type Theories, Linear Logic, Process Algebras, and Concurrency.
Invited Speakers:
Also 25-40 slots for 25 minute presentations of ongoing work are available. If you are interested in signing up for a slot, please send a title and an abstract of your intended presentation to ldpl95mathematik.th-darmstadt.de by January 15, 1995.
Slots will be filled on a ``first come, first served'' basis. Each request will be answered by February 15, 1995, the latest. We are investigating the possibility of publishing workshop proceedings.
There will be no workshop fee; participants will only be asked for a contribution to cover expenses for coffee breaks, reception, etc.
You are invited to pre-register for this workshop. In that case, or if you need further information, please send all correspondence to
Dr Michael Huth, Workshop on Logic, Domains, & Programming Languages AG 1, Fachbereich Mathematik, Technische Hochschule Darmstadt 64289 Darmstadt, Germany. E-mail: ldpl95mathematik.th-darmstadt.de
Talks will be held in the Max Palevsky Cinema on the first floor. Lunch and the break will be held in the third floor theater and will be provided for all participants. Dinner will cost approx. $10 per person.
If you wish to attend please send email to Lance Fortnow:
fortnowcs.uchicago.eduPlease tell us if you will be attending lunch and/or dinner and if you have any food restrictions. Let us know by Friday, November 18th so we can plan the meals accordingly.
Program:
For more information:
The full version of this announcement is available.
This spring school focuses on how-to-write-functional-programs. The spring school aims to bring computer scientists up-to-date with the latest advanced functional programming techniques. It is assumed that the attendees have some basic knowledge of functional programming, i.e., on the level of Bird and Wadler's `Introduction to functional programming'. An ample amount of time will be spent on exercises. The number of students will be strictly limited, in order to allow an intensive interaction between students and lecturers.
List of Topics includes:
Speakers John Hughes (Göteborg), John Launchbury (OGI), Mark Jones (Nottingham), Phil Wadler (Glasgow), Jeroen Fokker (Utrecht), Lennart Augustsson (Göteborg), Dick Kieburtz (OGI), Magnus Carlsson (Göteborg), Erik Meijer (Utrecht), Thomas Hallgren (Göteborg).
Applications The number of attendees is limited, so it's important to return the application form (see full version of this announcement) as soon as possible. Deadline for applications is April 1, 1995. Further information is available via email at baastad@cs.chalmers.se or on WWW.
Fees The board and accomodation fee is 4500 SEK. The participation fee is 1000 SEK for PhD students (a letter of recommendation is required), 3000 SEK for academia, and 5000 SEK for others.
Scholarships There is a limited number of scholarships available for people who cannot obtain support from other sources. A request for full or partial support should be enclosed with the application.
The full version of this announcement is available.
The full version of this announcement includes:
Please register (conference, hotel, excursion) by November 25. Also, send a hardcopy to Marganit Charish including the conference registration fee.
We ask that you send a check or money order only for the conference registration. Hotels will be paid directly and the excursion fees can be paid at the registration desk.
Direct all correspondence to Marganit Charish, Secretary of ISTCS, by e-mail, phone, fax, or air mail (not 1st class mail!!!)
Marganit Charish, Secretary of ISTCS'95 Department of Computer Science, School of Mathematical Sciences Tel Aviv University, Tel Aviv, Israel phone: +972-3-6408040, fax: +972-3-6409357 e-mail: marga@math.tau.ac.il
The full version of this announcement is available.
The aim behind both conferences is to stimulate the exchange of ideas and information among computer scientists, especially those working in academic and research institutions in Australia and New Zealand. The proceedings of both conferences will be published as issues of the Australian Computer Science Communications.
ACSC is the premier Australasian conference for the presentation of Computer Science research - the first edition was held in 1978. Invited speakers are:
ADC is the region's most important forum for the dissemination of results in database systems theory and practice. Invited speakers are:
Workshop An Australasian Computer Architecture Workshop will be held at Flinders University at the same time as ADC'95.
Further Information relating to location, travel, accommodation, Provisional Programme, Registration, Organizers, Sponsors, etc., is available in the full version of this announcement as mentioned above.
The LaTeX full version of this Call for Papers is available.
This workshop is the ninth in a series of international meetings, the last three having been in Dagstuhl (Germany, 1992), Boston (USA, 1993) and Val d'Ajol (France, 1994). As its predecessors, UNIF'95 is meant to be an opportunity to meet old and new colleagues, to present recent work, and to discuss new ideas and trends related to unification.
The dates for UNIF95 have been chosen to facilitate combined trips to the RTA'95 conference starting on Wednesday April 5 in Kaiserslautern.
This year's workshop is organized by Robert Nieuwenhuis and Albert Rubio. The following is a (non-exclusive) list of possible topics:
It is expected that there will be no registration fees but because of the size of the facilities, places at the workshop will be limited to about 50 people. The final list of talks and participants will be selected by Claude Kirchner and Robert Nieuwenhuis.
If you intend to participate in the workshop, please apply to roberto@lsi.upc.es, indicating: (i) full name and address, (ii) whether you intend to give a talk, and (iii) preference for single or double room. Please apply now, or at least before January 15, 1995. (early applications will have a higher priority). Abstracts will be due by March 1, 1995.
If you have any questions, email roberto@lsi.upc.es.
The full version of this Call for Papers is available.
MFCS is the 20th annual symposium in the series organized alternately in the Czech Republic, Poland, and Slovak Republic, respectively. Papers presenting original research on theoretical aspects of computer science are sought.
Principal topics of interest include (but are not limited to): algorithms and data structures, automata and formal languages, complexity and computability, computational geometry, cryptography, data bases and knowledge-based systems, declarative programming, formal specifications and program development, models of computation, parallel and distributed computing, semantics and logics of programs, theoretical issues in artificial intelligence, VLSI systems.
Invited Speakers:
S. Arnborg (Stockholm), V. Geffert (Kosice), G. Gottlob (Vienna),
J. Hartmanis - key note address (Cornell), R. Karp (Berkeley),
D. Lehmann (Jerusalem), D. Perrin (Paris), A.A. Razborov (Moscow),
J. van Leeuwen (Utrecht), P. Vitanyi (Amsterdam).
Instructions for Authors:
Authors are invited to submit 6 copies of a draft paper (no e-mail submissions accepted) and an abstract of up to 20 lines (preferably by e-mail), in English, to be received by January 9, 1995 by
Jiri Wiedermann, MFCS'95, Institute of Computer Science
Academy of Sciences of the Czech Republic
Pod vodarenskou vezi 2, 182 07 Prague, Czech Republic
tel: +42 2 6605 3520, fax: +42 2 8585 789, email: wieder@uivt.cas.cz
Papers should start with a succinct statement of the problem, the results achieved, their significance and a comparison with previous work. The length, including cover page and bibliography, should not exceed 10 pages (roughly 4500 words total). If available, an e-mail address and the fax number for the contact author should be included.
Dates: Subm: 9 Jan 1995; Notif: 3 Apr 1995; Final: 15 May 1995.
Local enquiries: actionm@cuni.cz (Milena Zeithamlova)
The sixth of the biennial conferences on Category Theory and Computer Science is to be held in Cambridge in 1995, in conjunction with the third Cambridge Summer Meeting in Category Theory.
The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory, algebra, geometry and logic. Whilst the emphasis is on applications of category theory, it is recognised that the area is highly interdisciplinary and the organising committee welcomes submissions in related areas.
Topics central to the conference include:
Submissions purely on category theory are also acceptable as long as the applicability to computing is evident.
Previous meetings have been held in Guildford (Surrey), Edinburgh, Manchester, Paris and Amsterdam.
Proceedings: it is anticipated that will be published by Springer in the LNCS series.
Dates: Subm: 1 Feb 1995; Notif: 14 Apr 1995; Final: 1 Jun 1995.
Submissions: send 5 hard copies of a draft paper (max 20 pages) to
Dr. David Pitt, Department of Mathematical and Computing Sciences
University of Surrey, Guildford, Surrey, GU2 5XH, United Kingdom
Local Arrangements:
Dr. Peter Johnstone
Department of Pure Mathematics and Mathematical Statistics
16 Mill Lane, Cambridge, CB2 1SB, United Kingdom
Registration forms will be available nearer to the date.
Organising and programme committee:
S. Abramsky, P.-L. Curien, P. Dybjer, P. Johnstone, G. Longo,
G. Mints, J. Mitchell, E. Moggi, D. Pitt, A. Pitts, A. Poigne,
D. Rydeheard, F-J. de Vries, E. Wagner.
The conference aims at providing a forum for the presentation and discussion of recent research in the following areas:
The program of TLCA will consist of about 30 selected presentations in plenary sessions.
Programme Committee: H. Barendregt, M. Dezani (Chair), J-Y. Girard, R. Hindley, F. Honsell, J. W. Klop, G. Longo, A. Meyer, G. Plotkin, P. Scott, J. Smith, J. Tiuryn.
Submissions: Original contributions are solicited for TLCA; they should be sent to the conference secretariat. Electronic submission (PostScript only) is preferred; hard copy (6 copies required) will also be accepted. Papers should be clearly written and allow the program committee to assess the merits of the work. References and comparisons with related work should be included. Papers should not exceed 15 standard pages and should be accompanied by a one-page abstract.
Proceedings: It is intended to publish the accepted papers as a volume of the Springer Verlag Lecture Notes in Computer Science series.
Organizing Committee: G. Cleland, P. Gardner, M. Lekuse, G. Plotkin (University of Edinburgh).
Dates: Subm: 8 Sep 1994; Notif: 12 Nov 1994; Final: 15 Dec 1995.
TLCA Secretariat
Professor M. Dezani
Universita di Torino, Dip. di Informatica,
Corso Svizzera, 185, 10149 Torino, Italy
Tel: 39-11-7429232, Fax: 39-11-751603, Email: dezani@di.unito.it
Lambda-Calculus Network Meeting
Participants of TLCA are welcome to attend a Lambda-Calculus Network Meeting to be held immediately before the conference.
The Formal Aspects of Computing Special Interest Group's annual Christmas meeting has concurrency as its theme this year.
Keynote speakers include
Proposals are invited for further contributions to the meeting. In a departure from recent practice, contributions in the form of papers, tutorials and workshops will all be welcomed.
For the purposes of initial selection, proposals should be a page or two in length, and should be sent to either member of the organising committee (see below). Please feel free to contact an organiser to discuss a possible proposal.
Proposals should reach the organisers by 30th November 1994, but do submit earlier if possible.
The organisers are particularly keen to receive proposals for contributions of a general nature, such as those that review recent developments in an aspect of concurrency in a form suitable for a wide audience.
Tim Denvir
Translimina Ltd.
37 Orpington Road, Winchmore Hill, London N21 3PD
Tel.: +44 81 882 5853, Fax: +44 81 882 3118
e-mail: timdenvir@cix.compulink.co.uk
Richard Mitchell
Department of Computing, University of Brighton
Lewes Road, Brighton BN2 4GJ, UK
Tel.: +44 273 642458, office 273 642451, Uni. switchboard 273 600900
Fax: +44 273 642405, e-mail: Richard.Mitchell@brighton.ac.uk
The full version of this Call for papers is available.
Advances in networking have allowed computer systems across the world to be interconnected. Despite this, heterogeneity in interaction models prevents interworking between systems. Open Distributed Processing (ODP) is an emerging technology which attempts to solve the software interaction problem by proposing a common framework for distributed systems. ODP systems are those that support heterogeneous distributed processing both within and between autonomous organisations.
One of the aims of ICODP'95 is to bring together representatives from both academia and industry to discuss the Conference theme Achieving Open Distributed Systems - Experiences with Distributed Environments.
Areas In addition to papers addressing the Conference theme, papers are sought in all areas pertinent to ODP, including but not limited to: Distributed Applications (for Telecommunications, Government, etc), Distributed Architectures, Trading and Type Management, Distributed Environments, Computer Supported Co-operative Work, Enterprise Issues, Resource Discovery, Modeling and Specification, Security, Transactions, Management.
Information for Authors Contributions are expected either as papers (max 12 pages) or as position statements (max 4 pages). The purpose of position statements is to provide a seed for debate and discussion. See full version of this Call for submission information, addresses, etc.
Dates: Subm: Oct 14 (papers), Nov 25 (position statements), 1994;
Notif: Dec 9, 1994; Final: Jan 20, 1995.
Related Events
A TINA (Telecommunications Information Networking Architecture) Conference will be held in Melbourne, in the week prior to ICODP'95. This is aimed at initiating and consolidating a sound worldwide base for the technological advances needed to bring telecommunications and computing together into an overall information networking architecture. Enquiries on TINA'95 should be sent to Steve Leask, Telstra Australia:
Email: s.leask@trl.oz.au, Phone: +61 3 2536238, Fax: +61 3 2536362.
The full version of this Call for Papers is available.
CSCW is a multidisciplinary area where behavioral, computer, educational, engineering, management, organisational and social scientists, engineers and users meet in order to improve the understanding of and exchange experience of cooperative work and supporting computer and communication technology in different settings.
Topics include, but are not limited to
Submissions We invite submissions of original work: papers, videos and demonstrations, panel, workshop and tutorial proposals. Submissions must be in English and, for each category, must follow the specific requirements stated in the full version of this Call (see above).
Dates: Subm: Feb 1, 1995; Notif: Mar 24, 1995; Final: Apr 21, 1995.
Program Committee chairman: Hans Marmolin, KTH, Stockholm
Proceedings chairman: Kjeld Schmidt, Risoe, Denmark
Panels chairman: Lennart E Fahlen, SICS, Stockholm
Demos/videos chairman: Konrad Tollmar, KTH, Stockholm
Tutorials chairman: Kai-Mikael Jaeae-Aro, KTH, Stockholm
Workshops chairman: Paal Soergaard, Norwegian Comput. Center, Oslo
General information on ECSCW'95 via WWW will appear.
General questions: by email to ecscw95@kth.se, fax to +46-8-102477, phone to JoAnn Gerdin, conference secretariat, +46-8-7906280.
Text and LaTeX full version of this Call for Papers available.
This symposium is intended to provide a forum for researchers working in theoretical computer science and discrete mathematics. Papers presenting original research on theoretical aspects of computer science and on combinatorics are sought.
Topics: Typical, but not exclusive, topics of interest include
Abstract Submission: Authors are requested to send 6 copies (in English, possibly double-sided) of a max 10-page extended abstract to:
Ming Li -- COCOON'95, Department of Computer Science
University of Waterloo, Waterloo, Ont. N2L 3G1, Canada
More precise requirements are given in the full version of this Call.
Dates: Subm: Mar 14, 1995; Notif: Apr 28, 1995; Final: May 30, 1995
Proceedings: published by Springer in the LNCS series, available at the conference. Each accepted paper should be presented by an author.
Program Committee Co-Chairs:
Conference Co-Chairs:
The full version of this Call for Papers is available.
The Computing Center of the Siberian Division of the Russian Academy of Sciences and the Electrical Engineering University are organizing the Third International Conference on Parallel Computing Technologies (PaCT-95), which will be held in St.-Petersburg, September 12-15, 1995. Aim of PaCT-95 is to give an overview of new developments, applications and trends in parallel computing technologies. We sincerely hope this conference will help to deepen our understanding of parallel computing technologies by providing a forum for an exchange of views between scientists and specialists from many countries over the world.
Main topics:
Call for papers: Original papers are invited for the Conference. An extended abstract (ca. 5-7 pages) should be submitted to the conference address (see below). Electronic copies in plain ASCII, LaTeX format, or postscript are preferable. Alternatively, submissions may be sent by ordinary mail (four copies). Detailed submission information, including additional information required of authors, pre-registration forms, and submission addresses, is in the full version of this Call (see above).
Technical details: The extended abstract should be in plain ASCII, or standard LaTeX (`article' style) and can be submitted via email.
Dates: Subm: Feb 1, 1995; Notif: Mar 15, 1995; Final: May 20, 1995.
Proceedings: will be distributed at the Conference.
Conference Addresses:
V.E.Malyshkin, E-mail: malysh@comcen.nsk.su, pact-95@comcen.nsk.su
Fax: 007-3832-324-259, 007-3832-357-942; Tel: (3832)-350-994
The full version of this 2nd Call for Papers is available.
Design, development and operation of computing and communication systems ought to be accompanied by assessments of their quantitative non-functional properties. Quantitative properties include system performance, reliability, performability. Assessing quantitative properties involves system modelling, wherever possible supported by system measurement. In view of the variety and technical complexity of existing paradigms, model analysis techniques and measurement options, quantitative system assessment will only become standard practice if supported by widely applicable techniques and easily usable tools.
Topics: the conference will focus on
Dates: (all submissions to the Programme Chair, please)
Programme Chair: Heinz Beilner, Universität Dortmund F. Informatik
email: beilner@ls4.informatik.uni-dortmund.de
Organiz. Chair: Martin Paterok, IBM Deutschland I., ENC Heidelberg
email: paterok@vnet.ibm.com
The LaTeX version of this Call for Papers is available.
This workshop follows the three previous editions of BMW held at the University of Bordeaux in October 1992, at the University of Quebec in Montreal in both June 1993 and May 1994. This year, the theme is more focused than previously: verification tools at work on `real' examples.
Our aim is to explore scope, efficiency and limitations of available tools. To achieve this, we invite researchers to present significant experiments in using tools for the verification of large systems.
We expect these experiments to be shown at least partially during software demonstration sessions.
One-hour lectures are scheduled: 4 invited lectures and 12 communications selected by the Program Committee. The presentations will be followed by discussion and common work sessions.
Program Committee: A. Arnold, S. Brlek, M. Ferguson, N. Halbwachs, O. Roux, J. Thistle.
Invited Speakers: J.P. Elloy, J.F. Groote, K. McMillan, J. Sifakis.
Organizing Committee: P. Felix, A. Griffault (LaBRI, Bordeaux).
Submissions: =<10-page papers on practical experiments; guidelines:
Alain Griffault, LaBRI, Universite Bordeaux I
351, cours de la Liberation, F-33405 Talence Cedex, France
Phone: +33-56.84.69.15, Fax: +33-56.84.84.12
e-mail: Alain.Griffault@labri.u-bordeaux.fr
Dates: Subm: Feb 15, 1995; Notif: Mar 31, 1995; Final: May 15, 1995
Registration: The registration fee is 400 FF (Students: 100 FF).
Local arrangements, more information: contact organizing committee.
Job Title PhD Fellow
Enquiries contact mike@macadam.mpce.mq.edu.au urgently.
Closing date for receipt of applications has passed, but
truly exceptional students may still apply before November 14.
The Microsoft Institute of Advanced Software Technology, based in North Ryde, Sydney, is offering four PhD fellowships commencing in the 1995 academic year. The Institute is affiliated with Macquarie University, and was established by Microsoft as part of the Partnership for Development Program with the Australian Government. Successful applicants will work within the Microsoft Institute's two research units: Distributed Computing and Natural Language Processing. Each unit is headed by an experienced academic researcher: Dr John Potter and Dr Robert Dale respectively.
The Institute's Fellowship scheme commenced in 1992, and has attracted outstanding students. Of the eight current fellows, five are University Medallists and all attained First Class Honours.
Eligibility Candidates must either be an Australian citizen, or hold Permanent Resident status in Australia; and have successfully completed a Bachelor's degree with Honours, or alternately have proceeded to a Master's degree by research, at an Australian tertiary institution.
Terms and Conditions The fellowship provides a A$20,000 per annum supplement to the Australian Postgraduate Award; applicants must simultaneously apply, via the Microsoft Institute, for an APA with Macquarie University. The award is normally tenable for a period of three years, with the expectation that the student will submit a doctoral dissertation at the end of this period. There are no commercial obligations: Institute Fellows are not judged on the commercial relevance of their work to Microsoft, but purely on the quality of their research.
Job Titles
Lecturer / Senior Lecturer, School of Computer Science & Engineering
Enquiries
may be directed to Professors Hiller, Compton, Hellestrand or Wainwright,
Phone +612 385 5518.
Closing date for receipt of applications is 25th November 1994.
Applications are invited for appointment to the positions of Lecturer and Senior Lecturer in the Department of Computer Science & Engineering at the University of New South Wales in Sydney, Australia.
Up to three positions are available (quote reference 514) with a preference for candidates with a background in software engineering, parallel and distributed systems, algorithms, or real time computing. However, outstanding applicants in any area of computer science are welcome.
A fourth position (quote reference 515) is available for a person who has a background in telecommunications and networking.
Successful candidates will be expected to teach undergraduate and graduate subjects within the School, and to make an effective contribution to the School's research activities. Appointees must be able to supervise students up to the PhD level.
Applicants must have a relevant PhD (or equivalent) along with teaching and research experience.
The positions are available for a fixed term of 5 years.
Intending applicants should contact
The Recruiting Officerfor a copy of the advertisement and selection criteria.
Human Resources
The University of NSW
Sydney 2052
Applications are invited for the new Chair in Theoretical Computer Science which has been established for the strategic purpose of strengthening the School's research and teaching standing in the fundamentals of computer science. The School wishes to attract an internationally recognised academic who can provide leadership, ideally in support of its theoretical research strengths in:
The person appointed would be expected to play a leading role in the Centre of Theoretical Computer Science which brings together researchers from the Departments of Pure Mathematics and Philosophy.
Informal enquiries to
Professor Peter Dew (dew@scs.leeds.ac.uk, Tel 0532 335432)
or to
Professor Simon French (sf@scs.leeds.ac.uk, Tel. 0532 335433)
Further particulars may be obtained from
(Mrs) S.M.D. Wheelerquoting reference 48/112.
Personnel Director, Office of the Registrar
The University of Leeds, Leeds LS2 9JT, UK
Tel. 0532 335775(direct line); Fax 0532 335779,
Closing date for applications: 5 December 1994.
The Advanced Telecommunications Institute (ATI) in Stevens Institute of Technology has been funded by Federal Government and Industry with an aim to establish a nationally preeminent telecommunications institute for applied research.
The role of ATI is to initiate and provide telecommunications technology through applied research, development and technology transfer. In addition, ATI integrates state-of-the-art research into engineering education. To achieve this mission ATI invites resumes for Post Doctoral Fellows from people with a proven track record of research in:
Please send your resumes to:
Dr. Dhadesugoor R. Vaman
Director, Advanced Telecommunications Institute
Stevens Institute of Technology
Hoboken, NJ 07030, USA, Fax 201-216-5057
The Department of Electrical Engineering and Computer Science (EECS) at Stevens Institute of Technology invites applications for tenure-track faculty positions at the assistant and associate professor levels. Applicants should have a Ph.D. in Electrical Engineering, Computer Engineering or Computer Science and should show evidence of exceptional research and teaching promise.
The EECS Department is currently seeking applicants in software engineering, database management, operating systems, artificial intelligence, computer graphics, image and signal processing, and wireless communications. Applicants are also sought in telecommunications: high speed multimedia networking (ATM and broadband ISDN), network management and multimedia applications.
Stevens Institute of Technology, founded in 1870, is located in Hoboken, New Jersey on the west Bank of the Hudson river directly across from Manhattan, NY. Stevens has recently established an Advanced Telecommunications Institute (ATI), a national center for applied research in telecommunications. The EECS Department offers Bachelor's (programs are accredited by ABET and CSAB), Master's, Engineer's and Ph.D. degrees in electrical engineering, computer engineering and computer science.
Applications
Send your vita, with the names of four references, to:
Prof. A. SatyanarayanaAddress e-mail inquiries to
Chairman, Faculty Search Committee
Department of Electrical Engineering and Computer Science
Stevens Institute of Technology
Castle Point on the Hudson, Hoboken, NJ 07030
eecs@stevens-tech.edu
Stevens is an Affirmative Action/Equal Opportunity employer.
The full version of this announcement is available.
The following positions are available immediately:
Applications are invited for positions within the Software Research Lab (SRL) at the new NASA Independent Software Verification and Validation Facility in Fairmont, West Virginia. The lab is operated by West Virginia University through a cooperative research agreement with the National Aeronautics and Space Administration's Headquarters Office of Safety and Mission Assurance (OSMA - Code Q).
Researchers are needed in the following areas of software engineering: metrics, safety & criticality, process, V&V, testing, OT&E, requirements engineering, and formal methods. Applicants are expected to hold the Ph.D. degree in computer science or a closely related field with some experience in one or more of these areas.
Please send a cover letter, vita, reprints of recent publications, and direct three letters of recommendation to:
Dr. John R. Callahan, NASA IV&V Facility
100 University Drive, Fairmont, WV 26554
Phone: 304-367-8235, Fax: 304-367-8211
Applicants can also send/direct their information via email (in ASCII or PostScript format) to:
callahan@cs.wvu.edu
Additional information about the IV&V Facility, the SRL, and these positions is available after Sept. 16, 1994 via the SRL WWW server (IP address: 129.164.10.21).
West Virginia University is an equal opportunity/affirmative action employer. The positions are subject to University approval.
The full version of this announcement is available.
DIMACS, the Center for Discrete Mathematics and Theoretical Computer Science, is soliciting applications for university-industry postdoc and senior research fellowships in computer-aided verification as part of its 1995-6 Special Year on Logic and Algorithms.
One of the topics on which this special year is focused is computer-aided verification, which studies algorithms and structures for verifying properties of hardware and software. It draws upon techniques from graph theory, combinatorics, automata theory, complexity theory, Boolean functions and algebras, logic, Ramsey theory and linear programming.
The university-industry postdoctoral program is an NSF-sponsored program that provides opportunities for recent doctoral recipients in the mathematical sciences to broaden their knowledge, experience, and perspectives by exposing them to industrial environments and for industry to interact with talented researchers who are beginning their careers.
The university-industry senior research program is an NSF-sponsored program whose goal is to increase participation of mid-career and senior mathematical scientists in an industrial research setting and to expose mid-career and senior industrial mathematical scientists to academic research. The program provides research fellowships, both university-to-industry and industry-to-university.
Conditioned on funds approval, we expect DIMACS-industry postdoctoral positions, industrial positions for academic mathematical scientists, and DIMACS positions for industrial mathematical scientists. Interested mathematical scientists are encouraged to apply. Details on application procedures, eligibility, terms and conditions, application checklist, and further information, are in the full version of this announcement.
The full version of this announcement is available.
The Department of Computer Science of The Hong Kong University of Science and Technology plans to hire at least two new faculty members for its Theory & Algorithms group in the coming year. The interests of the group's four current members include distributed algorithms, randomization, computational geometry, data structures, mathematical analysis of algorithms and combinatorics. We welcome applications from researchers in these or any other areas of theory.
The official notice that appeared in the CACM is included in the full version of this announcement.
If you have any further questions concerning theory at HKUST please feel free to contact me at
golin@cs.ust.hkDr. M. J. Golin, Dept of Computer Science, HKUST
The full version of this announcement is available.
The Department of Computer Science at Dartmouth College invites applications for two positions in computer science. The first position is at the level of Associate or Full Professor. Candidates for this position should have a substantial record of research in a major area of experimental computer science and systems. The second position is also tenure-track, but both level of appointment and area of research are open. However, preference will be given to a junior appointment.
The Department of Computer Science currently includes nine regular faculty members, and will have eleven regular members after these appointments. Several faculty members in the Thayer School of Engineering and the Department of Mathematics have research interests related to computer science and participate in the Computer Science Ph.D. program. Research interests in the department include algorithms, multimedia, graphics, visualization techniques, computational geometry, asynchronous concurrent systems, parallel algorithms, parallel file and disk systems, operating systems, design automation, VLSI, robotics, electronic libraries, combinatorial optimization, image processing, and signal processing.
Persons interested should submit a curriculum vitae and a list of at least four references, at least one of whom can comment on teaching. Review of the applications will begin immediately and will continue until the search is complete. Please send applications materials and general inquiries to Phyllis Bellmore, Computer Science Recruiting, Department of Computer Science, Dartmouth College, 6211 Sudikoff Laboratory, Hanover, NH 03755-3510. Specific questions can be referred to Scot Drysdale, Chair, at the same address (scot@cs.dartmouth.edu).
More information on Dartmouth's Computer Science Department is available over WWW .
Dartmouth is an equal opportunity/Affirmative Action employer and encourages applications from women and members of minority groups.
The Department of Computer Science and Engineering anticipates having several openings and is interested in attracting outstanding junior and senior candidates in the following areas: computer architecture, databases, security/cryptography, and theory. Salary and rank will be commensurate with qualifications, in conformance with University of California policies. A Ph.D. in computer science or related area is required. We are most interested in hiring at the Professor or Associate Professor level, but will consider strong applications at the junior level.
Applications received by March 1, 1995 will be given full consideration, but later applications will also be considered if unfilled positions remain. Please send a curriculum vitae (including a statement of teaching and research accomplishments), a statement of citizenship status, and the names of four references to:
Prof. Christos Papadimitriou, Chair, Faculty Recruiting Committee
Mail Code --- 0114, Department of Computer Science and Engineering
University of California, San Diego, La Jolla, CA 92093--0114, USA
UCSD is an Equal Opportunity/Affirmative Action Employer; women and minority applicants are encouraged to apply.
In this thesis I discuss a method for the correct development of programs for parallel or distributed computer systems. The idea is to develop the system stepwise, starting from a sequential or layered initial design that reflects the logical structure of the system. In a number of steps the initial design is refined to meet the actual architecture of the system under consideration. The top-level structure however is still sequential or layered. Then this layered system is transformed to a parallel or distributed system tailored to the physical structure of the system by means of the communication closed layers principle, originally introduced by Elrad and Francez, which states that under some side conditions layered and parallel systems are equivalent.
We use a new program composition operator, called layer composition. It's functional behavior is as if it were sequential composition, but it allows parallelism between independent components. This allows to formulate the communication closed layers principle as an algebraic law. The foundation of the method are hierarchical graphs, which are a hierarchically structured extension of partial order models. Hierarchical graphs are used both as a semantic model and to define our process language in. Hierarchical graphs allow to model shared memory algorithms, asynchronous and synchronous communication, atomicity, and real-time.
We apply the method of layered design to several examples, such as the Two-Phase Commit protocol for distributed databases, a distributed minimum-weight spanning tree algorithm, parts of caching algorithms, and algorithms computing distances in graphs. Also some small examples concerning real-time are discussed.
Copies of the thesis are available from the author on request: E-mail: janssenw@cs.utwente.nl
As programs are increasingly used in safety critical applications, program correctness is becoming more important; as size and complexity of programs increases, the traditional approach of testing is becoming inadequate. Proving the correctness of programs written in imperative languages is awkward; functional programming languages, however, offer more hope. Their logical structure is cleaner, and it is practical to reason about terminating functional programs in an internal logic.
This dissertation describes the development of a logical theory, TPT, for reasoning about the correctness of terminating functional programs, its implementation using the theorem prover Isabelle, and its use in proving formal correctness. The theory draws both from Martin-Löf's work in type theory and Manna & Waldinger's work in program synthesis. It is based on classical first-order logic, and it contains terms that represent classes of behaviourally equivalent programs, types denoting sets of terminating programs and well-founded orderings. Well-founded induction is used to reason about general recursion in a natural way and to separate conditions for termination from those for correctness.
The theory is implemented using the generic theorem prover Isabelle, which allows correctness proofs to be checked by machine and partially automated using tactics. In particular, tactics for type checking use the structure of programs to direct proofs. Type checking allows both the verification and derivation of programs, reducing specifications of correctness to sets of correctness conditions. These conditions can be proved in typed first-order logic, using techniques of reasoning by induction and rewriting, and then lifted up to TPT. Examples of program termination are asserted and proved, using simple types. Behavioural specifications are expressed using dependent types, and the correctness of programs asserted and then proved. As a non-trivial example, a unification algorithm is specified and proved correct by machine.
The work in this dissertation clearly shows how a classical theory can be used to reason about program correctness, how general recursion can be reasoned about, and how programs can direct correctness proofs.
Thesis now available by anonymous ftp from Cambridge.
This is the announcement of the new releases of GLD and GLA graphical tools for LOTOS. Precompiled versions for SunOS are available by using anonymous ftp.
GLD (GraphicaL Designer)
GLD is a tool aimed at graphical editing and design for LOTOS. It uses two different formalisms: G-LOTOS and DART (can be mixed). Using this tool the system is described as a set of modules or components and its interconnections using DART language. From this architectural design, the tool is able to obtain a LOTOS description mapping the DART design.
Main features of GLD tool are:
GLA (Graphical Animator)
GLA is a graphical animator of the behaviour of a full LOTOS specification, using graphical views from the DART specification to show:
Where to find GLD and GLA
By anonymous ftp get:
We are happy to announce the avaibility of AutographV3 (in alpha prerelease version). Volunteers are sought to try out this new system and turn in bug reports extensively.
Autograph is a graphical editor for networks of automata, in the context of automatic verification for process algebras.
The new version is written in C++, uses color and still runs under X11 on Sparc stations (with Sun OS4.x). It is interfaced with Fc2 format for (decorated) labelled transition systems, and (output only) for networks descriptions. This allows interface to verification tools, such as Auto (also developped in our team).
The new `atg' binary is available Z-compressed as well as gz-compressed by anonymous ftp.
Install instructions are contained in the README file extracted while untar'ed.
Enjoy!
Valerie Roy (vr@cma.cma.fr)
Robert de Simone (rs@cma.cma.fr)
The idea is that class Entity will never be instantiated (an abstract base class in C++ terminology), but is used to specify all properties common to User and Group. Now there are operations defined on these classes, eg
join: entity, group -> groupwhich are used to assign or delete entities (ie users or groups) to resp. from groups. There are other operations which operate on entities and I also need operations which operate on all entities (eg search for a user with a specific name). As far as I understand, ACT ONE does not support inheritance. If this is correct, could some of you give me a hint which formalism would be appropriate to specify (and maybe verify) my approach? I also need some constraints, eg for each group there may be a maximal number of members (members can be users or groups), and the operation join should only add an entity to the group if this number is not yet reached. Another example of constraint is as follows. Each group has a flag which can restrict membership to users (this way it would be possible to prohibit nested groups). Consequently, the operation join should fail, if this flag is set and it is tried to add a group to the group. As you can see, object orientation is important for my model. I would be really thankful for any hint or pointer to appropriate literature.
leave: entity, group -> group
You are invited to submit a discussion piece to Computing Surveys on topics arising from the recent Turing Award article by Juris Hartmanis in the October CACM. The overall topic of his article, `On Computational Complexity and the Nature of Computer Science', lends itself to both technical discussion of questions in theoretical computer science and broader discussion of policy issues relating to `Computing the Future'. I hope you will be able to participate so that we can start a meaningful discussion on the research directions and goals of computer science in the pages of Computing Surveys. Juris has agreed to comment on accepted discussion items. Potential topics for discussion, all of them related to questions raised in the paper, are listed in the full version of this invitation (see above).
Your discussion should be between 500 and 1000 words, and should be received no later than Dec 15th for inclusion in the March 1995 issue of Computing Surveys. Please send a message to my secretary `kha@cs.brown.edu' with a copy to me `pw@cs.brown.edu' to let me know if you can participate in this `Computing Surveys Symposium'.
Yours
Peter Wegner
Editor in Chief Computing Surveys (starting January 1995)
(This is an excerpt from the routine distribution for the categories mailing list, which is the file routine.dist in pub/categories at sun1.mta.ca and was last updated on Sept 15, 1994.)
Access to archives of categories postings and other useful pointers is available on the World Wide Web .
This page may also be reached by pointing to Mount Allison University in New Brunswick, Canada and then choosing `Academic Information', `Science', `Math and Computer Science' and `Research Information'.
The archives of postings on categories are held at the ftp site sun1.mta.ca in the directory pub/categories. This is a Unix system.
The postings are filed in yearly subdirectories called 90, 91 etc. Within those subdirectories there are monthly files, and an annual list of dates and subjects of postings.
In the pub/categories directory there is also a file called ftp.sites with information about ftp sites holding files of interest to subscribers. Please send information about WWW/ftp sites with holdings of interest to categories-request@mta.ca, or to me.
If you need detailed instructions on how to use ftp, ask anyone knowledgable about the Internet at your site, or write to me.
Bob Rosebrugh
Dep't of Mathematics and Computer Science
Mount Allison University
Sackville, N. B. E0A 3C0, Canada
Phone: +1-506-364-2538 InterNet: rrosebrugh@mta.ca
I would like to announce the availability of a world-wide web home page on logical frameworks .
This includes a (BibTeX) bibliography, pointers to implementations, addresses of researchers in the area, and a ``what's new'' page. Many papers are available via anonymous ftp; hypertext links to them are provided so they can be conviently previewed or retrieved by the click of a button.
Corrections, additions and other comments and suggestions are most welcome.
Important Disclaimer: In order to keep the task of compiling this material manageable I excluded general-purpose theorem proving systems designed for the formalization of classical or constructive mathematics, such as NQTHM, NuPrl, Coq, LEGO, and others. However, I included individual experiments carried out in these systems that are meta-logical in nature. I would like to provide cross references to home pages for such related systems and type theories where available.
Frank Pfenning
Department of Computer Science, Carnegie Mellon University
Pittsburgh, PA 15213-3891, U.S.A.
Telephone: +1 412 268-6343, FAX: +1 412 268-5576, InterNet: fp@cs.cmu.edu
<location> := ftp://ftp.cs.utwente.nl/pub/doc/amast/
<location> := http://www.cs.utwente.nl/data/amast/Index.html
Date: 24/10/1994
Contents :
Index.html
,
README
,
amast91/, amast93/, amast95/, info/,
links/, pstv95/, sigala/
The directory of each issue of AMAST Links may have a subdirectory full/, where more detailed information is stored, that is referred to in the corresponding newsletter. Only the presence, not the contents, of those subdirectories is documented here.
was edited by Giuseppe Scollo, Michael Johnson and Edmund Kazmierczak,
thanks to contributions by:
Michael Huth [M1],
Lance Fortnow [M2],
Erik Meijer [M3],
Amos Fiat [M4],
John Roddick [M5],
Robert Nieuwenhuis [M6],
Milena Zeithamlova [C1],
David Rydeheard [C2],
Philippa Gardner [C3],
John Cooke [C4],
Laszlo Kovacs [C5], [C6],
Ming Li [C7],
Victor Malyshkin [C8],
Falko Bause [C9],
Alain Griffault [CA],
Michael Johnson [J1], [J2],
Peter Dew [J3],
Klaus Sutner [J4], [J5],
Jack R. Callahan [J6],
Barbara Quigley [J7],
Mordecai J. Golin [J8],
Scot Drysdale [J9],
Ramamohan Paturi [JA],
Wil Janssen [L1],
Martin Coen [L2],
Jesus Sanchez Allende [T1],
Valerie Roy [T2],
Erik Wilde [P1],
Peter Wegner [V1],
Bob Rosebrugh [S1],
Frank Pfenning [S2].
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. The file names will be the same, but in another directory .