Contributions are welcome!
_ _ _ _ _ _ _ _ _ _ _ _ _ _
date: 25 October 1995
e-mail to: amast@cs.utwente.nl
________________________
e-mailed to: 779 subscribers
Dr. Valentin Antimirov died on May 31, 1995 after a severe disease. Valentin was an active member of the AMAST community. The enclosed obituary notice, which will appear in the Bulletin of the EATCS, throws more light on the personality of Valentin.
Our colleague and friend, Ukranian computer scientist Valentin Antimirov died on May 31 in Nancy (France) after a severe illness. He was only 34 years old and he was working virtually until his last day.
He was born on May 4, 1961 in Grozny (Russia). He studied in Moscow in one of the strongest of the Moscow Institutes - the Institute of Physics and Technics. After his graduation he lived and worked in Kiev (Ukraine). So, he was a son of this strange big country which ceased to exist in 1989, but which left so many evil traces in so many people's lives. He lived in Kiev already in 1986, the year of Chernobyl explosion which, who knows, might have been fateful to him.
In 1989, when two of the present authors visited the Glushkov Institute in Kiev, Valentin was heading a dynamic research group working on equational reasoning and algebraic specification. At that time, only few scientific connections existed between the West and the former Soviet Union, but our clear feeling was that Valentin's work deserved a much better recognition. The contrast between the high quality of research and poor working conditions was striking. The whole group of about ten people shared a single room and three East German PC's, on which they were developing very interesting and innovative software, implementing the newest ideas of algebraic specifications.
In March 1991 Valentin made a visit to Nancy which gave rise to a tighter collaboration with the Nancy group. He also established contact with Aarhus (Denmark) the same year, and held a post-doc position there for 12 months, during which he started what was to be his last passion: an intense study of the theory of regular expressions, reading everything there was to read on the subject, and finding novel techniques for implementing decision problems. In April 1993 he moved to Copenhagen to continue this work. In January 1994 he took a a position of visiting scientist in Nancy and began to work in France. Once one of us proposed that he should write a little survey on the complexity of various regular expression problems. He said that he liked the idea but he had rather to work on new results. He was in hurry. Despite the disease, he worked more and more. He gave a talk at STACS'95 (his picture at STACS'95 appeared in the last EATCS Bulletin). Those who participated at RTA'95 should remember him discussing, questioning, arguing. Finally, he had a paper accepted for the FCT conference in Dresden in August 1995 that he didn't have chance to present.
Valentin loved discussing. On various topics, scientific or not. Among scientific topics there was one to which he was especially partial throughout his career: algebraic specifications. He taught algebraic specifications to students of Kiev University. He was very devoted to this scientific idea and carried such an amount of conviction that other people easily got convinced too.
Those who knew Valentin beyond his scientific life will recall him and his wife Tatiana playing guitar and piano and singing. His repertoire was composed of Okudjava, Nikitin, and other such authors so familiar to the Soviet intelligentia. These songs belong to the so-called `amateur song' movement that started at the end of Khruschev's `thaw' and was pursued during almost 20 years of Brezhnev's era. This was a form of protest, escape, revelation, intellectual food for a whole generation.
He was struggling against his disease until his last days, despite the knowledge that there was no escape. Last time he came to work in the office was on May 18. That day he escaped from the hospital in order to send the final version of his FCT paper. After that he continued to work in the hospital on his powerbook. On May 31 he passed away.
Gregory Kucherov (Nancy)
Pierre Lescanne (Nancy)
Peter Mosses (Aarhus)
Alonzo Church, who was born on June 14, 1903 in Washington, D.C., died on Friday, August 11, 1995, in Hudson, Ohio at the age of 92.
The family has suggested that in lieu of flowers memorial contributions be made to the Association for Symbolic Logic (1409 West Green Street, Urbana, IL 61801, USA) and marked "For the Alonzo Church Fund".
Update of information in [AL0206M1] .
A preliminary AMiLP'95 Call for Participation is available.
The AMiLP'95 Call for Participation contains a preliminary programme, and further information about the workshop organization, costs, accommodation, travel, and registration.
Advance Registration
Due to the limited number of places available, advance registration is recommended. The advance registration deadline is:
Friday 1 December, 1995
A registration form is included in the Call for Participation. If you wish to register in advance, please compile that form and send it to:
AMiLP'95 Secretariat
University of Twente, Fac. Informatica, SETI
P.O. Box 217, NL-7500 AE Enschede, The Netherlands
phone: + 31 53 4893680, fax: + 31 53 4893503
e-mail: amilp95@cs.utwente.nl
Further Information
A WWW page for AMiLP'95 is under preparation, it will have the URL
http://www.cs.utwente.nl/data/amast/workshops/AMiLP95.html
Please address your inquiries to the AMiLP'95 Secretariat, preferably by e-mail, at the address given above.
Update of information in [AL0205C4] .
The Program and Registration Information is available on the WWW at the following sites:
The abstracts from the 1st SPIN Workshop are now available online, through Netscape or Mosaic. You can access it through the standard SPIN News page .
The abstracts are also available directly .
The abstracts page also contains some references to other papers that didn't make it in time for the workshop itself.
There is also a brief announcement of at least a somewhat firmer plan now to organize also the 2nd SPIN workshop, next year in New Jersey, adjacent to the CAV96 and LICS96 conferences.
If you would like to change one of the links to point to a local copy of a paper, or propose any other type of change (extra papers, other links), let us know!
J-Ch. Gregoire
Doron Peled
Gerard Holzmann
Once again this October the Category Theory Research Center (CTRC) has sponsored a weekend meeting at McGill University. This annual event brings together mathematicians interested in the categorical aspects of logic, computer science, combinatorics, universal algebra, homological algebra, topology, analysis, and theoretical physics.
If you are interested in more information, please consult the CTRC web page .
Update of information in [AL0203C7] .
The full version of Advance Program and Registration is available in
two forms: plain-text and LaTeX respectively.
Postscript versions of Advance Program and Registration are available on the Symposium WWW site.
Update of information in [AL0204C1] .
The List of Accepted Papers is available.
Update of information in [AL0203CB] .
The FOCS'95 Technical Program is available.
The main subject of the meeting is the intuitionistic type theory that Per Martin-Löf started developing in 1970. This is reflected in the festive title of the meeting, but the organizers also wanted some related developments to be taken into account at the meeting. The program displays the various points of view from which type theory has been approached, including logic and foundations of mathematics, computing science, philosophy and linguistics.
Two and a half days of talks were followed by a round table discussion on the background and possible future lines of development of type theory. A list of speakers and discussants follows.
Program committee: Giovanni Sambin, chair (University of Padua), Furio Honsell (University of Udine), Jan Smith (Chalmers University), Goran Sundholm (University of Leiden), Jan von Plato (University of Helsinki).
Invited speakers: Peter Aczel, Stefano Berardi, Rod Burstall, Thierry Coquand, Martin Hofmann, Petri Maenpaa, Lena Magnusson, Per Martin-Löf, Christine Paulin, Aarne Ranta, Anton Setzer, Goeran Sundholm, William Tait, Silvio Valentini, Dirk van Dalen.
Round table: N. G. de Bruijn, Robert L. Constable, Jean-Yves Girard
Update of information in [AL0203C8] .
The Programme of the Symposium is available.
A selection of papers from the conference will appear in a book in the Lecture Notes series published by CSLI.
The full version of this announcement is available.
The interplay between mathematics and computer science has traditionally centered around areas in logic, category theory and discrete mathematics. In recent years new connections between mathematics and computer science have emerged from such unexpected quarters as algebraic topology, differential geometry, dynamical systems and operator algebras. These new developments hold the promise of bringing new insights and powerful mathematical tools to bear on problems in computing. At the same time, such problems have opened new avenues of exploration for the mathematician.
This workshop is intended to bring together mathematicians and computer scientists for a series of tutorials and discussions on "New Connections". It is being timed to take advantage of parallel programmes in "Semantics of Computation" and "From Finite to Infinite Dimensional Dynamical Systems" at the Issac Newton Institute in the second half of 1995. The workshop is being jointly hosted by the two programmes and by Hewlett-Packard's Basic Research Institute in the Mathematical Sciences (BRIMS) in Bristol, England. Financial support is expected from BRIMS, the London Mathematical Society and the MATHFIT initiative of the Engineering and Physical Sciences Research Council.
If you are interested in giving a contributed talk at the workshop, please send a title, abstract and a list of 2-3 relevant references to the organiser, Jeremy Gunawardena at BRIMS (address in the full version of this announcement). A bibliography will be complied from this data and made available to all participants.
Discussions are underway with Cambridge University Press for publication of the proceedings.
A list of invited participants, pre-registration information and other details are in the full version of this announcement.
For further information about BRIMS try the WWW site.
Newton Institute WWW site : http://www.newton.cam.ac.uk/
Update of information in [AL0205C7] .
The List of Accepted Papers is available.
Update of information in [AL0206MI] .
The Final Program is available.
Update of information in [AL0201C7] .
The Preliminary Program is available.
Note: The 1995 Asia-Pacific Software Engineering Conference (APSEC'95) will be held immediately following ISAAC'95, in Brisbane, Queensland, 7-9 December, 1995. For further information please contact:
APSEC'95 Secretariat
PO Box 135 Aspley, QLD 4034 Australia
Facsimile: +61 7 3263 7020
- email:
- angie@acslink.net.au
- www
The full version of this information is available.
The meeting is dedicated to Peter Freyd in celebration of his 60th birthday. Peter of course will attend. The seminar welcomes talks using or addressing category theory or logic either explicitly or implicitly, in the study of any aspect of mathematics or science.
Proceedings will begin on Saturday at 9:30 am in Room 2511, the James Clerk Maxwell Building, the King's Buildings (the science campus of Edinburgh University), when we will finalise the timetable and start talks. A light lunch will be provided each day in the adjoining room, as well as coffee and biscuits.
We plan to publish a proceedings of the meeting as a special issue of the Journal of Pure and Applied Algebra, dedicated to Peter. Obviously, it is impractical for many scientists from outside western Europe to attend the meeting, so we will allow submissions to the proceedings by people who cannot attend but would like to participate.
Here is a current list of speakers and titles:
There is no registration fee. For more information relating to social events and accommodation, see the full version of this announcement.
The full version of the Call for Registration is available.
The workshop takes place as part of the Newton Institute programme on the Semantics of Computation. The general aims of the programme are twofold. First, to refine the current framework for the semantics of computation so that it is capable of dealing with the more subtle computational features present in the programming languages of today and tomorrow. Secondly, to provide a framework for interaction between such fundamental research and the issues confronted by language designers and software engineers. We particularly have in mind current developments such as object-based concurrent programming, and projects to develop the next generation of advanced programming languages, such as ML 2000. The range of technical and conceptual challenges involved in this work requires active collaboration and flow of information between overlapping communities of mathematicians, computer scientists and computer practitioners.
The aim of the Workshop is to bring together researchers pursuing various strands, to compare and contrast the different approaches, and take stock of current progress and future directions.
The following people have already agreed to speak at the Workshop:
Information relating to the Workshop Programme is included in the Call for Registration. The organizers invite offers of contributed talks; see the full version of this Call for details.
Update of information in [AL0201CE] .
The Final Programme & Call for Participation is available.
The organisation can be contacted at deon96@di.fc.ul.pt
WWW page on the workshop : http://www.di.fc.ul.pt/~llf/deon96.html
Update of information in [AL0206C2] .
Due to requests received from many potential authors and participants to the Third AMAST WRTS, the organizing Committee decided to extend the deadline for the submission which is now set for
November 10, 1995The organizing Committee urges all the potential participants to submit papers or to fill up the participation forms in order to be able to make the corresponding hotel arrangements. The participation forms are available in the Call for Papers .
Plain text and Postscript(tm) versions of the full Call for Papers are available . They may also be retrieved by anonymous FTP .
This conference is the eighth in a series dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on verification tools and the algorithms and techniques that are needed for their implementation. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series.
Topics: Modeling and specification formalisms; Algorithms and tools; Verification techniques; Applications and case studies; Verification in practice.
Submission Information: The conference will include contributed papers, project and tool presentations, and invited lectures. Submissions are invited in two categories:
Authors may submit a paper by mailing electronically a self contained Postscript(tm) version to the address cav96-submit@research.att.com
Important dates:
Submission deadline (firm): January 4, 1996
Notification of acceptance: March 11, 1996
Proceedings version of accepted papers due: April 17, 1996
The full version of this Call for Papers is available in two
forms: plain-text and LaTeX respectively.
The LICS Symposium aims to attract original papers of high quality on theoretical and practical topics in computer science that relate to logic in a broad sense, including algebraic, categorical and topological approaches.
Suggested, but not exclusive, topics of interest include: abstract data types, automated deduction, categorical models, concurrency, constraint programming, constructive mathematics, database theory, domain theory, finite model theory, hybrid systems, logics of knowledge, lambda and combinatory calculi, linear logic, logical aspects of computational complexity, logics in artificial intelligence, logic programming, modal and temporal logics, model checking, program logic and semantics, rewriting, logical aspects of symbolic computing, software specification, type systems, verification.
Paper submission: Send 12 copies of an extended abstract (not a full paper) to the program chair. Authors without access to copiers may submit a single copy. The first page of the extended abstract should include the title of the paper, names and affiliations of authors, a brief synopsis, and the contact author's name, address, phone number, fax number, and email address, if available.
Important Dates:
- Submission deadline:
- December 13, 1995 (firm)
- Notification :
- March 7, 1996
- Final papers due :
- May 7, 1996
A postscript version of the Call for Papers is available via
- LICS WWW page
- anonymous ftp
Update of information in [AL0206C6] .
The full version of this announcement is available.
The TARK conferences aims to bring together researchers from a variety of fields including: Artificial Intelligence, Cryptography, Distributed Computing, Economics, Game Theory, Linguistics, Philosophy and Psychology. This is to further understanding of interdisciplinary issues involving formal reasoning about rationality and knowledge. Topics of interest include, but aren't limited to: semantic models for knowledge and belief, bounded rationality, resource-bounded reasoning, commonsense epistemic reasoning, knowledge and action, applications of reasoning about knowledge and other mental states and belief revision. Previously a by-invitation-only conference, TARK is now open to all interested attendees.
Note that some of the dates and other details have changed from the previous announcement published in AL0206. Interested parties are advised to consult the full version of this announcement at the URL above.
The full version of this First Call for Papers is available in two
forms: plain-text and LaTeX respectively.
The conference is in honour of the 65th anniversary of Andrei Ershov (1931-1988) and his outstanding contributions towards advancing informatics. The aim of the Conference is to provide a forum for the presentation and discussion of advanced research directions in Computer Science. For a developing science, it is important to work out consolidating ideas, concepts and models. Movement in this direction is one of the goals of the Conference. Improving contacts and exchanging ideas between researchers from the East and West is another goal.
The conference includes topics in Theoretical computer science, Programming Methodology, Artificial Intelligence and New Information Technologies. A more detailed list of suggested topics is given in the full version of this announcement. To maintain an intensive conference atmosphere and enable in-depth discussions, the number of participants is limited to 100.
Submissions. All submissions must be in English and give sufficient detail to allow the Programme Committee to assess the merits of the work. Prospective authors should read the detailed submission information in the full version of this announcement.
Important Dates
Conference Chair
Alexandre Zamulin, Institute of Informatics Systems
6 Acad. Lavrentjev pr. 630090 Novosibirsk, Russia
Phone: +7-3832-396258. Fax: +7-3832-323494. Email: zam@iis.nsk.su
The full version of this Call for Papers is available in two
forms: plain-text and LaTeX respectively.
This Call for Papers will not be widely distributed by post. Please post it at your place of work and distribute it as widely as possible among interested researchers that you know. Notice the change of dates, including the early deadline. For additional information see the WWW page .
Scope and Format: Research contributions to the theory, design, specification or implementation of distributed systems are solicited. Topics of interest include, but are not limited to: Distributed algorithms and complexity, network protocols and architectures, multiprocessor algorithms and architectures, distributed operating systems, communication networks, concurrency control and synchronization, fault tolerance, specification, semantics and verification, and cryptography and security.
Submissions:
Prospective authors should read the detailed submission information in the full version of this announcement.
Important Dates:
To be considered by the committee, abstracts must be received by October 27, 1995, or sent by airmail and postmarked before October 20, 1995. This is a firm deadline. Acceptance or rejection notifications will be sent by December 20, 1995. Camera-ready versions of accepted papers and short abstracts will be due January 31, 1996.
Program Chair
Yoram Moses,Department of Applied Math and Computer Science,
Weizmann Institute of Science Rehovot, 76100, Israel.
Email: yoram@cs.weizmann.ac.il
The full version of this Call for Papers is available.
The workshop is intended to bring together scientists and engineers from a variety of fields, including communications and networks, operating systems, storage and retrieval, user interface development, distributed computing, multimedia and hypermedia information representation. The workshop will examine current and new approaches from different perspectives ranging from architecture to technology. A detailed list of topics is given in the full version of this announcement.
Further information is available .
Deadlines:
Contact person:
Herwart Pusch - GMD FOKUS
tel. + 49 30 25499 233
fax. + 49 30 25499 202
Email: idms@fokus.gmd.de
The LaTeX full version of this Call for Papers is available.
This conference is intended to provide a forum for researchers in theoretical computer science, combinatorics related to computing, and experimental analysis of algorithms. Typical, but not exclusive, topics of interest include: algorithms and data structures, complexity theory, computational algebra, biology, geometry, learning theory, number theory, cryptography, combinatorics related to algorithms and complexity, parallel and distributed computing, graph theory and communication networks and experimental analysis of algorithms.
Submissions this year will be conducted electronically. Authors should send a PostScript file containing an extended abstract to Prof. Jin-Yi Cai, COCOON'96 Program Co-Chair, at
cocoon96@cs.buffalo.eduPlease first send an e-mail to cocoon96@cs.buffalo.edu with the subject HELP. A detailed instruction on how to submit your paper will be sent to you. For those who have no access to e-mails, one can send 6 hard copies of an extended abstract to:
Prof. Jin-Yi Cai -- COCOON'96Prospective authors should read the more detailed submission information given in the full version of this announcement.
Dept. of Computer Science, State University of New York
Buffalo, NY 14260 USA
Important Dates
Further Information will be maintained in the COCOON'96 WWW page .
The full version of this announcement is available.
This is a call for contributed presentations for WOPA'96. The goal of the Workshop on Parallel Algorithms is to promote the exchange and dissemination of information among researchers in this field. The fourth Workshop on Parallel Algorithms is a constituent meeting of the Federated Computing Research Conference (FCRC). The constituent FCRC meetings will partially overlap in time to facilitate the interaction of the researchers from different fields of computer science and to expose them to a wider range of research problems and results. The full list of constituent meetings is given in the full version of this announcement at the URL above.
Submissions
Prospective contributors should read the detailed submission information in the full version of this announcement at the URL above.
Important Dates
Program Chair
Joseph F. JaJa, UMIACS, University of Maryland,For additional information, send e-mail to: wopa96@umiacs.umd.edu
A.V. Williams Bldg, Paint Branch Drive,
College Park, MD 20742, U.S.A.
Phone: +1 301-405-6722. Fax: +1 301-314-9658
The full version of this announcement is available in two
forms: plain-text and LaTeX respectively.
COLT'96 will be held in the town of Desenzano del Garda, Italy, from June 28 through to July 1 1996. We invite papers in areas that relate directly to the analysis of learning algorithms and the theory of machine learning, including neural networks, statistics, statistical physics, Bayesian/MDL estimation, reinforcement learning, inductive inference, knowledge discovery in databases, robotics, and pattern recognition. We encourage submission of papers describing experimental results that are supported by theoretical analysis.
Abstract Submission
Authors should submit fifteen copies (preferably two-sided) of an extended abstract to:
Michael Kearns - COLT '96Prospective authors should read the detailed submission information in the full version of this announcement at the URL above.
AT&T Bell Laboratories, Room 2A-423, 600 Mountain Avenue
Murray Hill, New Jersey 07974-0636,
Phone(for overnight mail): (908) 582-4017
Important Dates
Program Chairs
Avrim Blum (Carnegie Mellon University) and Michael Kearns (AT&T Bell Laboratories).
The full version of the Final Call for Papers is available.
The aim of the workshop is to bring together researchers and practitioners interested in the development and application of tools and algorithms for specification, verification, analysis and construction of distributed and embedded systems. The overall goal of the workshop is to compare the various methods and the degree to which they are supported by interacting or fully automatic tools. Theoretical papers without a clear link towards automation or tool construction as well as tool documentations and applications without conceptual message are inappropriate for TACAS and should be submitted somewhere else.
Besides scientific talks there will be refereed tool sessions, with two page abstracts in the conference proceedings, and standard tool demonstrations during the breaks. A detailed list of topics is available in the full version of this annuncement.
Submissions
Authors are invited to submit an extended abstract not exceeding 5000 words for regular papers and 1500 words for tools presentations to to the local organizer. Electronic submission is encouraged via email. Prospective authors should read the detailed submission information in the full version of this announcement.
Important Dates
Organization and Submissions
Tiziana Margaria <tiziana@fmi.uni-passau.de>
FMI, University of Passau, Innstr. 33, 94030 Passau, Germany
Tel: +49 851 509.3096. Fax: +49 851 509.3092.
Additional Information:
Further information and updates are available via WWW .
The full version of this Call is available.
The PAP series of conferences is the world's leading showcase for Prolog applications and systems. Now in its fourth year the conference continues to grow, and to demonstrate the benefits of this important technology, including increased productivity, reduced maintenance, and flexible solutions which can easily adapt to changing business needs. We invite you to submit papers or industrial reports describing applications in the areas of logic and constraint logic programming.
For more information about PAP'96 see the WWW .
The PACT conference and exhibition is the premier forum for constraint applications and systems. Now in its second year the conference builds on the success of PACT'95, and clearly demonstrates the benefits of constraints for solving real-world problems. PACT'96 will focus on the industrial exploitation of Constraint Programming, and explore the realisable benefits for business, and future trends for this important technology.
For more information about PACT'96 see the WWW .
Anyone interested in either of these conferences is advised to read the full version of this announcement which contains detailed submission information and important dates for both conferences.
The full version of this Call for Papers is available.
In 1996 IOPADS graduates from an informal workshop held in conjunction with IPPS to a symposium format to be co-located with many others at FCRC'96. The aim of IOPADS has always been to bring together researchers in all aspects of parallel I/O, which we broadly place into five categories: architecture, algorithms, applications, file and operating systems, and compilers and runtime systems. It is our opinion that the problems of parallel I/O are most effectively addressed by investigating all these areas rather than working in each area in isolation. Although I/O-related papers appear in many other conferences, the value of IOPADS is in gathering interested researchers from all these areas of computer science, encouraging interdisciplinary interaction, rather than working in isolation.
Submissions
Papers submitted to IOPADS must be unpublished and must not submitted for publication elsewhere. The manuscript should be at most 20 8.5x11 or A4 pages long (including figures, tables, references, but excluding the page withheld from reviewers), typeset with a 10-point font on 20-point spacing, i.e., double spaced. Electronic submission (of PostScript) is strongly encouraged (details available on the Web page below, or contact the Program Chair). For hard-copy submission, send 7 copies of the paper (preferably double-sided) to the Program Chair.
Important Dates
All submissions, electronic or hard copy, must arrive by 6pm Eastern Time on October 17, 1995. Decisions will be announced by December 22, 1995.
Program Chair
Alok Choudhary, ECE Dept., 121 Link Hall Syracuse University,
Syracuse, NY, 13244. Phone: (315) 443-4280.
Email: choudhar@cat.syr.edu
For updates and more information , refer to the WWW site.
The LaTeX full version of the Call for Papers is available.
The Twenty-Eighth ACM Symposium on Theory of Computing (STOC), sponsored by the ACM Special Interest Group on Algorithms and Computation Theory, will be held in Philadelphia, May 22--24, 1996. Papers presenting original research on theoretical aspects of computer science are sought.
Typical, but not exclusive, topics of interest include algorithms and data structures, complexity theory, computational algebra and geometry, computational biology, cryptography, databases, machine learning, algorithmic graph theory, applications of logic, parallel & distributed computation, probabilistic computations, computer architectures and robotics.
Submission. Authors are encouraged to submit extended abstracts and brief announcements electronically. A detailed description of the electronic submission process is available on the Internet at the STOC'96 WWW page .
You may also obtain instructions as an automatic reply to e-mail to stoc96@cs.rpi.edu with the subject heading HELP.
See the full version of this announcement for more details relating to abstract format, submission requirements, program committee, etc.
Important Dates
Best Student Paper Award: A prize of $500 will be given to the author(s) of the best student-authored paper (or split between more than one paper if there is a tie). A paper is eligible if all its authors are full-time students at the time of submission. This must be indicated in the submission cover letter.
FCRC'96: STOC'96 participates in the 1996 Federated Computing Research Conference, FCRC'96. Look for further information on FCRC'96 at ACM's homepage .
The full LaTeX version of this announcement is available .
Formal analysis techniques are currently being applied in the design, development and assessment phases of both hardware and software. Generally, such applications do not get widespread attention, and therefore, the impression can come into existence that formal techniques are not being applied, or are not applicable to contemporary industrial problems.
In order to remedy this impression, Science of Computer Programming will in cooperation with the COST 247 project devote a special issue to applications of formal analysis techniques. Typically, contributions explain the application of the techniques to obtain insight in the functioning of systems, and assess the industrial relevance of the application. This insight can, for instance, be obtained by using (finite) state exploration tools, theorem provers or checkers, simulators or test generators. The insight can also be obtained by applying verification theory, specifying (modal) properties or transformation rules. The application of methods and techniques that enable the use of analysis techniques also falls within the scope of this special issue. This special issue is not intended for the presentation of new theory.
The length of contributions should not exceed approximately 20 pages. Detailed information is given in the full version of this announcement. A postscript version is available upon request (jfg@phil.ruu.nl).
Important Dates Deadline for submission : November 1, 1995
The full version of the First Call for Papers is available.
The CADE conferences are the major forum for the presentation of new research in all aspects of automated deduction. Original research papers, descriptions of working reasoning systems, and problem sets that provide innovative, challenging tests for automated reasoning systems, are solicited.
CADE conferences cover all aspects of automated deduction: First vs. Higher Order Logics, Classical vs. Non-Classical Logics, Special vs. General Purpose Inference, Interactive vs. Automatic Systems.
Specific topics of interest include (but are not limited to): Resolution, Sequent Calculus, Decision Procedures, Unification, Rewrite Rules, Mathematical Induction, and any applications of automated deduction, including: Deductive Databases, Logic and Functional Programming, Commonsense Reasoning, Software and Hardware Development.
Papers on commercial or industrial applicationsCADE-13 will be held as part of the Federated Logic Conference FLoC'96. The Proceedings of CADE-13 will be published by Springer-Verlag in their Lecture Notes in Artificial Intelligence Series. Research papers should not exceed 15 (fifteen) proceedings pages. System descriptions and problem sets should not exceed 5 (five) proceedings pages. Springer style files should be used if possible. These can be obtained from the CADE-13 web site .
of automated deduction are especially encouraged.
Prospective authors should consult the full version of this Call, for detailed submission requirements and other information.
Important Dates
Submission deadline: 12 January, 1996
Notification of acceptance: 20 March, 1996
Camera-ready copy due: 26 April, 1996
Further calls will be made for tutorials, workshops and a theorem proving competition, and details of these will also be available at the CADE-13 web site.
The full LaTeX version of the Call for Papers is available.
Formal techniques constitute the foundation of a systematic design. 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 use of refinement techniques in computing systems is increasing rapidly, as it provides the theoretical foundations for the design of reliable systems.
The workshop is devoted to considering the problems and the solutions in computing system design. Particular emphasis will be given to examination of how well formal refinement techniques for design, analysis and verification serve in relating theory to practical development of real time systems.
Papers are invited which address theoretical or practical issues in development and/or application of formal system specification, design, refinement and implementation. The organisers are aiming for a balanced mixture of theoretical and practical material, drawn from fully refereed papers as well as invited presentations. Some particular themes that might be addressed by authors are listed in the full version of this announcement. Papers with clear industrial relevance are particularly encouraged.
The proceedings are likely to be published by Springer-Verlag as part of the BCS Workshop series. Details of the cost of the workshop and a provisional timetable will be distributed at beginning of March 1996.
Submission details and other information are in the full version of this Call. Depending on availability of suitably mature (and formally based) software engineering tools to support refinement, a tool demonstration may also be possible.
Dates For Authors
Submission of papers: 15th November 1995
Notification of acceptance: 15th January 1996
Camera-ready copy of papers: 15th April 1996
The Call for Papers is available.
Key Dates:
Expression of interest: 13th Nov. 1995
Panel proposal submission: 8th Jan. 1996
Paper submission: 8th Jan. 1996
Notification of acceptance: 8th Mar. 1996
Further information on the workshop is available on the WWW .
The Call for Papers is available.
Important Dates
Submission deadline: March 8, 1996
Acceptance notification: June 17, 1996
Preliminary Call for Papers and Participation available.
PAAM'96 WWW page : http://www.demon.co.uk/ar/PAAM96/index.html
Paper submission deadline: January 26th, 1996.
Update of information in [AL0206C3] .
The full version of this Call for Papers is available.
Aims
A new class of models, formalisms and mechanisms for describing concurrent and distributed computations has emerged over the last few years. Some significant representatives of this new class are models and languages based on (generative) communication via a shared data space: Gamma, Linda, Linear Objects, Polis and Tao are examples.
Coordination models and languages are being investigated by the ESPRIT Basic Research Project, COORDINATION, which is organising this event. The objective of this conference is to provide a forum for the rapidly growing community of researchers interested in this field.
Further Information
WWW pages are available for further information, at two sites:
Invited Speakers - provisional
Ugo Montanari (Pisa Univ.)
Mario Tokoro (Keio Univ. / Sony)
Peter Wegner (Brown Univ.)
Important Dates
Deadline for submissions: October 30, 1995
Notification of acceptance: December 15, 1995
Camera-ready version due: January 15, 1996
Proceedings
The proceedings will be published by Springer-Verlag in the Lecture Notes in Computer Science (LNCS) series.
The Call for Papers is available in two
forms: plain-text and LaTeX respectively.
WWW : http://www.usc.edu/dept/ceng/prasanna/meetings/ipps/ipps96/ippshome
Important Dates
Deadline for submissions: November 15, 1995
Notification of acceptance/rejection: December 31, 1995
Deadline for final text: January 31, 1995
Workshop: April 15, 1996
IPPS'96 : April 15--19, 1996
The Conference Announcement & Call for Papers is available.
On the occasion of the 90th anniversary of the birth of Kurt Gödel.
WWW : http://www.fi.muni.cz/~zlatuska/goedel96.html
Important dates
Submission d'line: January 14, 1996 (anniversary of Gödel's death)
Acceptance/rejection notices: March 21, 1996
Final versions of papers due: April 28, 1996 (Goedel's birthday)
The Call for Papers is available.
Important Dates
Submission deadline: 1 December 1995
Notification of acceptance: 1 February 1996
Camera ready copies: 1 March 1996
The full version of this announcement is available.
The Advanced Computing Research Center is one of the University of South Australia's nine newly-endowed research centers.
The Center is seeking to appoint a candidate to participate in the Distributed Object Recognition research project. This project is currently funded by a University Development Grant on a one year basis. Future funding is possible depending on progress. To participate in this project the following qualification is desirable:
Annual salary is A$34,602 to A$40,087 depending on experience.
For further details of this post please contact Dr Jane You
Tel.:+61 8 3023970, Fax: +61 8 3023381, Email: jane.you@unisa.edu.auApplications with curriculum vitae including the names of two referees should be forwarded to Professor G.J. Milne, Director, Advanced Computing Research Center, University of South Australia, The Levels, South Australia 5095, Australia.
Information about the School of Computer and Information Science can be found in WWW .
The full version of this announcement is available.
Bellcore's Security and Network Design Research Department consists of over 30 research scientists and developers working on various applied research projects in the areas of information security, distributed computing and network design. The researchers and developers are required in the following areas:
Candidates must have Ph.D. or equivalent in Electronic Engineering or Computer Science with an emphasis on networking, cryptology, cryptographic, protocols, and security for distributed systems.
Applications for these positions, including a vita and list of references, should be sent to the following address:
Hiring Committee
Security Research Department
Bellcore, Room 2M399
445 South Street, Morristown, NJ 07960
More information about the responsibilities and special qualification requirements is available in the full version of this announcement.
The full version of this announcement is available.
Reference Number: 54595
The Software Verification Research Centre is a Special Research Centre of the Australian Research Council. Its mission is to create improved methods and tools, of industrial significance, for developing verified software.
Research positions are available for the following projects (one position per project), starting from January 1996:
See the full version of this announcement for a description of the aims of each project and of the successful applicants' profiles.
General Information
For each position, the ideal candidate enjoys working in groups and is able to progress towards stated goals with minimal supervision. Unless stated otherwise, appointment will be for one year in the first instance.
For further information on any of these positions, phone (07)365 1003, fax (07)365 1533, or email: svrc@cs.uq.oz.au
Applications, quoting Reference Number 54595, should nominate three referees with their address, email address, fax and telephone numbers and be sent to: The Director, Software Verification Research Centre, Department of Computer Science, The University of Queensland, QLD 4072, or emailed to svrc@cs.uq.oz.au
The closing date for applications is Friday 17 November 1995. The level of appointment will be in accordance with qualifications and experience. Salary ranges: see the full version of this announcement.
Work flow on Intelligent Distributed database Environment (WIDE) is an ESPRIT project aiming at the development of a next generation work flow management system based on state-of-the-art database technology. The project is organized in five main work packages: transaction management, active rule processing, database integration, work flow methodology, and end user testing.
The main tasks in WIDE of the University of Twente are located in the extended transaction management and work flow methodology work packages. The extended transaction management work package aims at the specification and implementation of an advanced transaction management module that is to be integrated with the active rule processing module and the general database platform. The work flow methodology package aims at the specification of a work flow specification technique and workflow design methodology and tools.
From November 1st 1995, two research positions will be available in the WIDE project at the University of Twente, each position for 30 months period. Extension of the positions will be a possibility to allow further research leading to a Ph.D. thesis. One position will be mostly devoted to the extended transaction management work package, the other to a combination of the work flow methodology and extended transaction management work packages.
Candidates for the positions should hold a M.Sc. in computer science. Background in database management systems and/or work flow management is an advantage. Further information can be obtained from Paul Grefen, (tel.: 053-893705) or Peter Apers (tel.: 053-893690).
Dr.ir. P.W.P.J. Grefen <grefen@cs.utwente.nl>
Information Systems Division, Computer Science Department
University of Twente, P.O. Box 217, 7500AE Enschede, The Netherlands
Phone +31-53-893705; Secr +31-53-893690; Fax +31-53-339605
The Department of Mathematics, National University, Bogota, Colombia is looking for two full-time positions at the level of associate professor, in order to push forward its newly formed Ph.D. program in Mathematics.
Some of the areas of interest are Mathematical Logic and Category Theory. The most needed expertizes are categorical logic, non-classical logics and/or mathematical theory of computation.
Candidates are expected to have Ph.D., international publications, willingness to supervise Ph.D. thesis, strong commitment to research and some beginning interest in doing research/teaching in Spanish.
Annual salary is expected to be around $25.000 (USA). Nevertheless, the real acquisitive power of the salary goes beyond its face value. It should be noted that in Bogota, for example, a fair lease of a 3-bedroom apartment costs aproximately $600 (USA) monthly.
Candidates should send an e-mail to Fernando Zalamea, e-mail address:
fzalamea@bacata.usc.unal.edu.cowith a short resume of their curriculum vitae and a proposal of activities to be carried on in Colombia (advanced courses/seminars, plans about future research are encouraged).
Further instructions would then be sent to candidates who reply to this communication.
The Macquarie University Mathematics Department expects soon to advertise a permanent Chair in Mathematics. The current holder, the Number Theorist John Loxton, has become Deputy Vice-Chancellor at Macquarie. The other Chairs in the Department are held by Alf van der Poorten (Number Theory), Alan McIntosh (Functional Analysis & PDEs), and myself.
I would certainly like the vacant Chair to be filled by someone in a field closely allied with Category Theory. So I am looking for expressions of interest. Please contact me by email if you are interested or have suggestions.
Ross Street <street@macadam.mpce.mq.edu.au>
Center of Australian Category Theory
Mathematics Department, Macquarie University
New South Wales 2109, AUSTRALIA
Telephone: (61-2-)850-8921, Facsimile: (61-2-)850-8114
email: street@mpce.mq.edu.au
The Carnegie Mellon Department of Mathematics seeks to make two tenure track appointments at the Assistant Professor level, although applications at a more senior level will be considered. These positions will commence in the Fall of 1996.
One appointment will be made in Discrete Mathematics or Mathematical Programming and candidates who can support the Department's educational program in Algorithms, Combinatorics, and Optimization are strongly preferred.
The second appointment will be made in stochastic analysis and candidates for this position who can support the Department's educational programs in Mathematical Finance are strongly preferred.
Applicants should send a vita, list of publications, and a statement describing current and planned research.
Candidates should also arrange to have at least three letters of recommendation sent to:
Appointments Committee,
Department of Mathematics, Carnegie Mellon University,
Pittsburgh, PA 15213.
Carnegie Mellon University is an Affirmative Action/Equal Opportunity Employer.
The Department of Computer Science invites applications for an entry level, tenure track position in Computer Science. Candidates are required to have completed a Ph.D. degree in Computer Science by the date of appointment and must show exceptional potential in teaching and research. Tentative date of appointment is for Fall 1996.
Midwestern State University has approximately 6,000 students and offers both BS and MS degrees in Computer Science. The teaching load is 12 hours of undergraduate courses, or 3 hours graduate and 6 hours undergraduate and will include a variety of courses in the computer science curriculum.
Applicants should send a letter of application, vita, statement of teaching philosophy, statement of research interests, and names and addresses of 3 references to:
Dr. Ranette Halverson
Coordinator of Computer Science
Midwestern State University
3410 Taft Blvd.
Wichita Falls, TX 76308-2099
Application deadline is December 31, 1995. Applications from women and minority groups are especially encouraged.
For the project Integer Polyhedra and Binary Spaces, subsidized by the Netherlands Organization for Scientific Research, the research group Combinatorial Optimization & Algorithmic at the CWI in Amsterdam searches for an Onderzoeker in Opleiding. (This is one of the Dutch equivalents for PhD student.)
Her/his task will be to carry out research in the area of discrete mathematics and integer programming. The research aims at the analysis of combinatorial optimization problems with the aid of graphs and polyhedra.
The duration of the project will be maximal 4 year.
Information can be obtained from the project leaders:
A.M.H. Gerards, phone: +31-20-5924045; e-mail: bgerards@cwi.nl
A. Schrijver, phone: +31-20-5924087; e-mail: lex@cwi.nl
Applications with curriculum vitae and references should be sent to:
A.M.H. Gerards
CWI
Afd. BS
Postbus 94079
1090 GB Amsterdam
The full version of this information is available.
Applications are invited for a Lectureship in the Department of Computer Science which is available from 1 January 1996. Candidates should have a strong research orientation in Design and Analysis of Algorithms and be capable of teaching computational geometry.
The appointment will be made on an appropriate point of either the Lecturer A scale, currently from sterling 17,288 to 21,982 per annum, or Lecturer B scale, currently from sterling 22,811 to 28,564 per annum (inclusive of 2,134 London Allowance p.a.) depending on qualifications and experience. If you are interested please contact
Hillia Holland (Mrs),for an application form and further details. The closing date for the receipt of applications (including a list of publications and the names of two academic referees) is 20 October 1995. Please quote reference A2/CS/21/95.
School Personnel Officer,
School of Physical Sciences and Engineering,
King's College London,
Strand, London WC2R 2LS, United Kingdom
Tel. +44 (0)171 873 2427, e-mail H.Holland@kcl.ac.uk
Promoting excellence in teaching, learning & research, Equality of opportunity is College policy.
For further particulars see the full version of this announcement.
Information about the Department is available at the departmental web page .
For informal enquiries about the Algorithm Group, please contact Dr C.S. Iliopoulos, tel +44 (0)171 873 2588 or e-mail csi@dcs.kcl.ac.uk
In addition prospective applicants are welcome to have an informal exploratory discussion with the Head of the Department, Professor J.R. Ullmann, tel +44 (0)171 873 2588.
The Service de Mathematiques de la Gestion (SMG) of the Universite Libre de Bruxelles is currently looking for software engineers.
The SMG is a department of the Universite Libre de Bruxelles devoted to research in Operations Research and Decision Aid Systems. Around September 95, it will start an applied research project in the field of long term human resources scheduling in collaboration with two private companies. We are looking for flexible software specialists who can perform activities ranging from research, analysis, design and implementation to support and training.
The applicants will have:
A working experience in constraint-based reasoning or related AI techniques, knowledge of ILOG SOLVER and ILOG VIEWS C++ class libraries, experience in scheduling systems and combinatorial problems and knowledge of RDBMS are desirable.
If you wish to join our team, send your resume with enclosed detailed information about your education, work experience, language fluency, expected remuneration, etc.
Universite Libre de Bruxelles
Service de Mathematiques de la Gestion
c/o Pierre Jacques
CP 210/01
Boulevard du Triomphe
1050 Brussels, Belgium
Fax: +32 2 240 07 91, email : pjacques@ulb.ac.be
The full version of this announcement is available.
The Service de Mathematiques de la Gestion of the Universite Libre de Bruxelles is the operations research department of the free university of Brussels. The department is seeking researchers for the following projects:
Starting date is January 1st 1996. Please contact as soon as possible
Daniel De Wolf (for posts 1, 2 and 3)
Tel: (32 2) 6505628, Fax: (32 2) 6505970, e-mail: dewolf@ulb.ac.be
Peter Cowling (for posts 2 and 3)
Tel: (32 2) 6505022, Fax: (32 2) 6505970, e-mail: cowling@ulb.ac.be
Service de Mathematiques de la Gestion, CP 210/01
Universite Libre de Bruxelles
Boulevard du Triomphe, B-1050 Bruxelles, Belgium
The Department of Computing Science at the Chalmers University of Technology and Goteborg University announces two postdoctoral fellow positions.
The Department of Computing Science has about 30 staff members and about 25 PhD students. The department receives funding from ESPRIT, and from the Swedish Government agencies TFR and NUTEK. The major topics of research are programming logic and type theory, functional programming and concurrency, but research is also carried out in a number of other topics.
The postdoctoral positions are four year fellowships. The postdoctoral fellow will take part in research, supervision of research students and teaching. The position is intended for a younger researcher with a good research record, and the intention is that the fellowship holder obtains the experience necessary for becoming an associate professor during the four years. The postdoctoral fellow will spend about 75 per cent of time on research and about 25 per cent on teaching. Applicants must have a PhD and a good research record. The department tries to increase the number of female employees, and welcomes female applicants. Further details can be obtained from Christer Carlsson, Head of the Department. Tel: +46-31-772 1038. Email: carlsson@cs.chalmers.se
To apply, send us a CV in English, covering your research and your teaching experience, and any other relevant experience, and giving the names of referees. Send three packets, each containing a copy of your CV, and of the research papers and other documents you wish to include. The last date for the application to arrive is 16 October 1995. The application should be marked with "Ref. No. E333 2836/95" and be sent to The Registrar, G=F6teborgs University, Vasaparken, 411 24 Gothenburg, Sweden.
The following technical report is available .
We demonstrate that in the context of statically typed pure functional lambda calculi, exceptions are strictly more powerful than call/cc. More precisely, we prove that the simply typed lambda calculus extended with exceptions is strictly more powerful than Girard's F-omega (a superset of the simply typed lambda calculus) extended with call/cc and abort.
This result is established by showing that the first language is Turing equivalent while the second language permits only a subset of the recursive functions to be written. We show that the simply typed lambda calculus extended with exceptions is Turing equivalent by reducing the untyped lambda calculus to it by means of a novel method for simulating recursive types using exception-returning functions. The result concerning F-omega extended with call/cc is from a previous paper of the author and Robert Harper's.
Will appear in: Chris Hankin, Ian Mackie and Raja Nagarajan, eds., Proceedings of the Second Imperial College Department of Computing, Workshop on Theory and Formal Methods, Moller Center, Cambridge, UK, 11-14 September 1994, World Scientific Publishing Co., 1995.
We present models of full classical linear logic, whose Kleisli categories for the exponential comonad are cartesian closed categories of topological spaces and continuous functions. One of these categories is dcpos and Scott-continuous functions and another one its full subcategory given by the dcpos with bottom. They turn out to be proper subcategories of a cartesian closed category of topological spaces satisfying an ``anti-separation'' axiom which we think is new.
The paper is available .
These reports are available from burns@windfall.crl.McMaster.CA "For profit" companies are asked to pay $5 and $8 respectively (except for members of TRIO and CITR).
This report explores some ideas for formally specifying modules based on trace assertion method outlined in, for example, [Parnas and Wang 1989]. These ideas include:
These are lecture notes for a short course (five lectures) by Wilder and Tucker on tabular methods for system documentation that forms part of a second year undergraduate course on system development within the Department of Computer Science, University of Wales, Swansea, Wales. The topics covered are: tables in the real work; tables and the system design life cycle; four documentation problems (word processor, calculator, polyline and dialogue box); general tables, and tables of terms over algebras.
We are keen to receive comments, suggestions and information on the material in these notes.
Update of information in [AL0206L8] .
The full version of this information is available.
James Otto has made available an update and correction of his thesis Complexity Doctrines via a note .
The note
The full version of this announcement is available.
The content of the special issue on Declarative Knowledge of the Annals of Mathematics and Artificial Intelligence (Volume 14, No. 1, 1995 edited by Wlodek Zadrozny) is as follows
We describe a subtyping extension of the Pure Type System lambdaP (an abstract version of LF). This system is the simplest corner of the lambda-cube with type-dependency, yet forms the core of applied type-theories for which subtyping is a desirable extension, for example to give better economy of encodings in LF or to allow automatic adaptation of proofs in \lambdaPRED (the predicate calculus fragment of the Calculus of Constructions).
We establish some meta-theoretic results about the system, including subject reduction, minimal types and decidability.
The combination of subtyping and type-dependency is quite tricky to analyse, mainly because the typing and subtyping relations are mutually defined, which means that tested techniques of examining subtyping in isolation no longer apply. We prove our results using an algorithmic reformulation which breaks some circularity of the definitions, and separates beta-reduction on types and terms.
The paper is available by ftp from Edinburgh.
The papers appearing in the following list are now available via anonymous ftp (gzipped postscript).
The file INDEX in that directory contains short descriptions of the papers.
The bibliography is now available .
It is intended to keep the bibliography of the book
A. Björner, M. Las Vergnas, B. Sturmfels,up-to-date electronically. The current version includes the complete bibliography of the book and all corrections, additions and updates known to Ziegler. Any corrections, new papers concerned with oriented matroids, and other relevant updates that you tell him about will be entered asap. That is, this is a ``living document''.
N. White & G. M. Ziegler:
Oriented Matroids,
Encyclopedia of Mathematics, Vol. 46,
Cambridge University Press 1993, 516 pages.
The conference was held in Quebec City from August 10th to 13th. The proceedings are available .
The full version of this announcement is available.
1995; 512 pages, 172 illustrations.
ISBN 0-387-94459-1 Hardcover $59.95
Springer
This book presents temporal logic as a means of specifying properties of reactive systems and develops an extensive verification methodology for proving that a system meets its safety specification.
Readers are assumed to have some familiarity with programming and basic concurrency concepts as well as first-order logic. No previous exposure to temporal logic is assumed since it is covered in the first chapter.
An educational version of the Stanford Temporal Prover (STeP), a tool that supports the verification of reactive systems, is available for use with this book.
While being completely self-contained, the new volume is a sequel to the previous volume, devoted to the specification of reactive systems by temporal logic:
The Temporal Logic of Reactive and Concurrent Systems: Specification
Z. Manna, Stanford University, CA
A. Pnueli, Weizmann Institute of Science, Rehovot, Israel
1992; 427 pages, 96 illustrations
ISBN 0-387-97664-7 Hardcover $49.95
To order: 1-800-Springer, or e-mail orders@springer-ny.com, or check the web site at http://www.springer-ny.com
Update of [AL0205MK]
The full version of this announcement is available.
(Note: the ToC's in the full version are in LaTeX format.)
The proceedings of the colloquium held at Ottawa in May are now available. The proceedings of the second colloquium will be available next year. Volume 1 is edited by Paola Flocchini, Bernard Mans and Nicola Santoro. Volume 2 is edited by Evangelos Kranakis and Lefteris Kirousis.
The ultimate goal of the research in Distributed Computing is to understand the nature, the properties and the limits of computing in a system of autonomous communicating agents. To this end, it is crucial to identify those factors which are significant for the computability and the communication complexity of problems. A very important role is played by those factors which can be termed as structural Information; that is, a priori knowledge available to the entities about the structure of the system.
The identification, characterization, and analysis of Structural Information and of its impact on communication complexity is an important theoretical task which has immediate practical importance (e.g., to determine the tradeoff between the cost of making globally available and mantaining structural information and the reduction in the communication costs given by such an information).
The purpose of the Colloquia on Structural Information and Communication Complexity (SIROCCO) is to explicitly focus on the interaction between structural information and communication complexity. The Colloquia comprise of position papers (outlining open problems, research directions etc.), presentation of current research results, and group discussions.
A collection of 15 short biographies of great living computer scientists. The technical level ranges from standard biography (untechnical) to a verbal description of the fundamental ideas in an algorithm, architecture, language or AI technique.
For more information and excerpts, please see the WWW page .
Publisher: Copernicus, An Imprint of Springer-Verlag, New York, Inc.
175 Fifth Avenue
New York, New York 10010
ISBN: 0-387-97922-1 (August, 1995)
springer books 1-800- 777-4643 ($23)
What the Critics Say: ``... a fascinating collection of profiles and interviews...'' L.R. Shannon, "Of Digital History," The New York Times, Science Times section, Tuesday, August 29, 1995; ``... lucidly written, consistently interesting, full of beautiful insights, examples, and stories, and generally inspiring. Also, lots of fun.'' David Gelernter, Professor of Computer Science, Yale University, author of Mirror Worlds, and 1939: The Lost World of the Fair.
The full version of this announcement is available.
Hardcover, xii, 229 pp.; price: 74,- DM; ISBN 3-05-002791-6
This book examines the concepts of knowledge and belief and their formalization in systems of epistemic logic, concepts which are equally central to philosophy and artificial intelligence research (AI). The original contributions compiled in "Knowledge and Belief in Philosophy and Artificial Intelligence" give an excellent overview of the current state of research in a field which has now developed into one of the focal areas of knowledge representation.
Contents:
The book may be ordered from:
VCH Verlagsgesellschaft mbH
P.O. Box 10 11 61
D-69451 Weinheim
Germany
Fax: +49 (0)6201 606184
Phone: +49 (0)6201 606152
A paper about a mechanization of the wellfounded recursion theorem is available nipkow/slind/papers/wfrec.ps.Z
It uses a formally proven wellfounded recursion theorem as the basis upon which to build a function definition facility for Higher Order Logic. This approach offers flexibility in the choice of wellfounded relations used, the deferral of termination arguments, and automatic isolation of termination conditions. Building on this platform, we provide the ability to define recursive functions via pattern matching. The system is parameterized and has already been instantiated to quite different theorem provers (HOL and Isabelle).
Concurrent ML is an extension of Standard ML of New Jersey with concurrent features similar to those of process algebra. Reppy has given it an operational semantics based on reductions of configurations, using entire programs rather than program fragments. The existing semantics are not, therefore compositional, and do not support compositional reasoning (for example equational reasoning about program fragments).
We present a compositional operational semantics for a fragment of CML, based on higher-order process algebra, and use this to define weak bisimulation for CML. We give some small examples of proofs about CML expressions and show that our semantics corresponds to Reppy's up to weak first-order bisimulation.
Computer Science Technical Report 95:05, School of Cognitive and Computing Sciences, University of Sussex.
The report is available electronically.
All reports from the School are available.
We are pleased to announce that a new version of HyTech is now publicly available. HyTech is an automatic tool for the analysis of embedded systems. HyTech computes the condition under which a linear hybrid system satisfies a temporal requirement. Hybrid systems are specified as collections of automata with discrete and continuous components, and temporal requirements are verified by symbolic model checking. If the verification fails, HyTech generates a diagnostic error trace.
HyTech is available by anonymous ftp and on the WWW:
Tom Henzinger, Pei-Hsin Ho, and Howard Wong-Toi.
The full version of this announcement is available.
I have just released Otter 3.0.4. There are very few changes to the ordinary features, and there are no substantial performance improvements, so many users won't need to upgrade. To help you decide, I have included two things: (1) short document on the new features, and (2) my file "Changelog" of notes on bug fixes and other changes.
You can obtain OTTER by anonymous ftp .
You may get information on DOS and Macintosh versions .
Also, visit our WWW page on automated deduction at Argonne.
Bill McCune
I have just released MACE 1.2.0. MACE (formerly called ANL-DP) is a program that searches for small finite models of first-order statements. It can also test satisfiability of propositional statements. See the MACE page for an introduction.
To run this version of MACE, you need Otter 3.0.4, which parses the input and does some translation.
You can obtain MACE by anonymous ftp .
MACE is not available for DOS or Macintosh computers.
Bill McCune
I am a user of the computer algebra system AXIOM, which has a sophisticated type structure for math concepts and structures.
I would be pleased to know of other users, and would be glad to give further information to anyone interested. There is a preprint:
Domains of data and domains of terms in AXIOMwhich includes a batch of AXIOM code for free groupoids and categories on directed graphs.
by R Brown and W Dreckmann
Ronnie Brown
Prof R. Brown
School of Mathematics
Dean St
University of Wales
Bangor
Gwynedd LL57 1UT
UK
Tel: (direct) +44 1248 382474
(office) +44 1248 382475
Fax: +44 1248 355881
email: mas010@bangor.ac.uk
- wwweb for maths
We are releasing the mechanically checked proof scripts for the FM9001 microprocessor. The FM9001 is a general-purpose 32-bit microprocessor which has been implemented as a CMOS ASIC. The proof being released rigorously connects the expression of the FM9001 as a netlist with the characterization of the FM9001 at the machine-code programmer's level. (The FM9001 is the foundation of the `CLI Stack', which also includes several verified compilers and applications all running on the FM9001. Other parts of the `CLI Stack' are separately released.)
To obtain information about the FM9001 microprocessor and proof, please examine the WWW page .
To obtain the FM9001 system, use anonymous ftp . Then follow the instructions of this README.
Bishop C. Brock and Warren A. Hunt, Jr.
brock@cli.com, hunt@cli.com
*Update of information in [AL0205T1] .
A new update of Isabelle, Isabelle94-4 , is now on the Cambridge ftp site. It is also on the Munich site .
Here's a summary of changes from Isabelle94-3.
Space requirements are much reduced, thanks to changes to the parser and classical reasoner.
Theory files (.thy) no longer require \...\ escapes to break lines.
You can search the theorem database. See the section "Retrieving theorems" on page 8 of the (updated) Reference Manual.
There are new examples, especially Grabczewski's monumental case study involving the Axiom of Choice.
The previous version of HOL is now called Old_HOL. It will disappear altogether in Isabelle-95!
The new version of HOL (previously called CHOL) uses a curried syntax for functions.
Application looks like f a b instead of f(a,b). Mutually recursive inductive definitions finally work in HOL.
In ZF, pattern-matching on tuples is now available in all abstractions. It translates to the operator "split". (Previously this was only available in HOL.)
Larry Paulson
Tobias Nipkow
The full version of this announcement is available.
The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems, using the clause normal form of 1st order logic. The TPTP supplies the ATP community with:
The tools are available on the WWW or by anonymous ftp, with either of the following URLs:
If you would like to register as a TPTP user, and be kept informed of such developments, please email one of us. Our addresses are:
Geoff Sutcliffe : geoff@cs.jcu.edu.au (FAX: +61-77-814029)
Christian Suttner : suttner@informatik.tu-muenchen.de (FAX: +49-89-526502)
The full version of this summary is available .
An open collaborative effort has been initiated: to design a
Common Framework for Algebraic Specification.
The rationale behind this initiative is that the lack of such a framework greatly hinders the dissemination and application of research results. In particular, the proliferation of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread support throughout the research community is urgently needed.
The initiative has been started by COMPASS (ESPRIT Basic Research WG 6112), in cooperation with IFIP WG 14.3 (Foundations of Systems Specification), but participation is already not confined to members of those groups. Some 25 leading researchers in algebraic specification have already agreed to participate, others are being invited to join.
The current aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The collective experience and expertise of the participants provides a unique opportunity to achieve this aim within a short time-span. The common framework will provide a family of languages at different levels:
A schedule of the immediate sub-goals is in the full version of this summary. Sub-groups of the participants are focussing on particular issues. Coordination of the collaborative effort is by means of moderated mailing lists, WWW databases, sub-group meetings, and plenary meetings (held adjacent to major conferences, to minimize travel).
Further details about the common framework initiative, including information about how to participate, are available on WWW .
I have finally made a web page for my database of automated reasoning systems and tools (and added many new entries).
If you find errors or missing links please let me know. I am still gathering data and making new entries (a never ending process it seems.)
Enjoy
Carolyn Talcott's home page can be visited.
The full version of this information is available.
**Announcing the Xy-pic version 3.1 Diagram Typesetting Package.** This is to announce a Release of my Diagram Typesetting Package: Xy-pic 3.1
This is a maintenance release where many little problems of the major release of Xy-pic 3.0 (from July) have been solved. Xy-pic is a package for typesetting a variety of graphs and diagrams with TeX. Xy-pic works with most formats (including LaTeX, AMS-LaTeX, AMS-TeX, and plain TeX), in particular Xy-pic is provided as a LaTeX2e supported package (following the CTAN LaTeX2e bundle standard).
**Availability.** Xy-pic can be retrieved through the World Wide Web Xy-pic home page .
Check the README file for the exact details.
The full version of this announcement is available.
Since Kris has just announced a new version of XY-pic, allow me to offer up my own diagram package for users of dvips.
The macros in kuvio.tex use PostScript embedded in \special control sequences to rotate arrows from the horizontal.
For anyone who's interested, the following files can be found.
See the full version of this announcement for a summary of the main features of the macros in kuvio.tex and of the contents of the files listed above.
The full version of this information is available.
The international WG7 mailing list distributes mail regarding the work of Working Group 7 of the Joint Technical Committee 1 of ISO and ITU-T (CCITT). Typically, the following areas are covered by postings:
The ODP mailing list is still operating and is a subset of the WG7 list.
Material for the new WG7 list can be published on the ftp site containing the RM-ODP documents and other related documents. You can retrieve the README and INDEX files by anonymous ftp .
The full version of this announcement is available.
We are glad to announce a new WWW information service for Mathematics, the Math-Net Links to the Mathematical World .
The Math-Net Links are a first collection of about 700 mathematical resources and related pointers into the Internet consisting of
The full version of this announcement is available.
We are happy to announce a new WWW page . containing unified complete bibliographies for the following journals and conferences:
Features of all the bibliographies include
In addition, the I&C and JACM bibliographies include
Update of information in [AL0205M3] .
An access list to papers, drafts etc. either presented or laid forth at the workshop is available via the ADT'95 homepage.
<location> := http://www.cs.utwente.nl/data/amast/
<location> := ftp://ftp.cs.utwente.nl/pub/doc/amast/
Date: 25/10/1995
Contents: Index.html, README, amast96/, workshops/, info/, links/,
sigala/, amast95/, amast93/, amast91/
ADY02N12 [26/07/1995--25/09/1995]
CAADY02 [01/01/1995--25/09/1995]
full/
[O1] Gregory Kucherov <Gregory.Kucherov@loria.fr>
[O1] Pierre Lescanne <Pierre.Lescanne@loria.fr>
[O1] Peter D. Mosses <pdmosses@brics.aau.dk>
[O2] Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
[M1] Anton Nijholt <anijholt@cs.utwente.nl>
[M2] Barbara Quigley <bquigley@dimacs.rutgers.edu>
[M3] Jean Charles Gregoire <gregoire@inrs-telecom.uquebec.ca>
[M3] Gerard Holzmann <gerard@research.att.com>
[M4] Thomas F. Fox <fox@triples.math.mcgill.ca>
[M5] Arnold L. Rosenberg <rsnbrg@elys.cs.umass.edu>
[M6] FST&TCS'95 Organization <fsttcs@tcs.tifr.res.in>
[M7] Sorin C. Istrail <scistra@cs.sandia.gov>
[M8] Giovanni Sambin <sambin@euler.math.unipd.it>
[M9] -- <tbilisi@cogsci.ed.ac.uk>
[MA] Jeremy Gunawardena <jhcg@hplb.hpl.hp.com>
[MB] Eva Tardos <eva@cs.cornell.edu>
[MC] Daniel Ouimet <ouimet@IRO.UMontreal.CA>
[MD] ISAAC'95 Organization <isaac95@sol.newcastle.edu.au>
[ME] Tracy Combe <tlc@dcs.ed.ac.uk>
[ME] -- <ajp@dcs.ed.ac.uk>
[MF] Andrew Pitts <<Andrew.Pitts@cl.cam.ac.uk>
[MG] Jose Luiz Fiadeiro <llf@di.fc.ul.pt>
[C1] Dan Ionescu <ionescu@trix.genie.uottawa.ca>
[C2] Tom Henzinger <tah@cs.cornell.edu>
[C3] Amy Felty <felty@research.att.com>
[C4] Margje Punt <margje@cs.ruu.nl>
[C4] Yoav Shoham <shoham@flamingo.stanford.edu>
[C5] Alexander V. Zamulin <zam@iisnw.iis.nsk.su>
[C6] Moses Yoram <yoram@cs.weizmann.ac.il>
[C7] Marloes Castaneda <castaned@cs.utwente.nl>
[C8] -- <twlam@csd.hku.hk>
[C9] Uzi Vishkin <vishkin@math.tau.ac.il>
[CA] Avrim Blum <avrim@blum.pc.cs.cmu.edu>
[CB] Tiziana Margaria <tiziana@fmi.uni-passau.de>
[CC] Peter Reintjes <peter_reintjes@vnet.ibm.com>
[CD] Thomas Cormen <thc@zayante.cs.dartmouth.edu>
[CE] Ian Parberry <ian@hercule.csci.unt.edu>
[CF] Jan Friso Groote <JanFriso.Groote@phil.ruu.nl>
[CG] Geoff Sutcliffe <geoff@cs.jcu.edu.au>
[CH] Lindsay Groves <lindsay@comp.vuw.ac.nz>
[CI] Bob Fields <bob@minster.york.ac.uk>
[CJ] Arnold L. Rosenberg (see [M5])
[CK] Al Roth <alroth@pap.com>
[CL] Roberto Gorrieri <gorrieri@cs.unibo.it>
[CM] Dominique Mery <Dominique.Mery@loria.fr>
[CN] Jiri Zlatuska <zlatuska@muni.cz>
[CO] Dov Gabbay <dg@doc.ic.ac.uk>
[J1] Weiping Zhu <Weiping.Zhu@unisa.edu.au>
[J2] -- <clyde@bellcore.com>
[J3] Edmund Kazmierczak <eka@cs.uq.oz.au>
[J4] Paul Grefen <grefen@cs.utwente.nl>
[J5] Fernando Zalamea <fzalamea@bacata.usc.unal.edu.co>
[J6] Ross Street <street@macadam.mpce.mq.edu.au>
[J7] -- <af1p+@andrew.cmu.edu>
[J8] Ranette Halverson <rhalver@nexus.mwsu.edu>
[J9] A.M.H. Gerards <bgerards@cwi.nl>
[JA] Tomasz Radzik <radzik@dcs.kcl.ac.uk>
[JB] -- <rebetez@ulb.ac.be>
[JC] Daniel De Wolf <dewolf@ulb.ac.be>
[JD] Johan Jeuring <johanj@cs.chalmers.se>
[L1] Mark Lillibridge <mdl@wily.fox.cs.cmu.edu>
[L2] Francois Lamarche <lamarche@lmd.univ-mrs.fr>
[L3] Doris Burns <burns@windfall.crl.mcmaster.ca>
[L4] James Otto <otto@triples.math.mcgill.ca>
[L5] Baltzer Science Publishers <publish@baltzer.nl>
[L6] David Aspinall <da@dcs.ed.ac.uk>
[L6] Adriana Compagnoni <Adriana.Compagnoni@cl.cam.ac.uk>
[L7] Oded Maler <Oded.Maler@imag.fr>
[L8] Günter M. Ziegler <ziegler@math.tu-berlin.de>
[L9] Jean-Marc Robert <Jean-Marc_Robert@uqac.uquebec.ca>
[LA] Walter Borden <wborden@springer-ny.com>
[LB] Evangelos Kranakis <kranakis@scs.carleton.ca>
[LC] Dennis Shasha <shasha@shasha.cs.nyu.edu>
[LD] Heinrich Wansing <wansing@rz.uni-leipzig.de>
[LE] Konrad Slind <slind@informatik.tu-muenchen.de>
[LF] Alan Jeffrey <alanje@cogs.susx.ac.uk>
[T1] Howard Wong-Toi <howard@cs.cornell.edu>
[T2] William McCune <mccune@mcs.anl.gov>
[T3] William McCune (see [T2])
[T4] Ronnie Brown <mas010@bangor.ac.uk>
[T5] Bishop C. Brock <brock@cli.com>
[T5] Warren A. Hunt Jr. <hunt@cli.com>
[T6] Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
[T6] Tobias Nipkow <Tobias.Nipkow@informatik.tu-muenchen.de>
[T7] Geoff Sutcliffe (see [CG])
[T7] Christian Suttner <suttner@informatik.tu-muenchen.de>
[S1] Peter D. Mosses <pdmosses@brics.aau.dk>
[S2] Carolyn Talcott <clt@sail.stanford.edu>
[S3] Kristoffer H. Rose <kris@diku.dk>
[S4] Anders Svensson <svensson@math.ubc.ca>
[S5] Juan Quemada Vives <quemada@dit.upm.es>
[S6] Joachim Luegger <luegger@zib-berlin.de>
[S7] David M. Jones <dmjones@theory.lcs.mit.edu>
[S8] Jo Erskine Hannay <joh@ifi.uio.no>
This issue of AMAST Links is available in four forms:
(+) within the AMAST directory of the Twente WWW server, at URLwhere `<pp>' is either `-ToC' (for the ToC-page),or the 2-character page identifier (for one-page files), or empty (whole-issue file).
http://www.cs.utwente.nl/data/amast/links/v02/i07/AL0207<pp>.txt
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 .