Contributions are welcome!
_ _ _ _ _ _ _ _ _ _ _ _ _ _
date: 31 August 1995
e-mail to: amast@cs.utwente.nl
________________________
e-mailed to: 766 subscribers
Update of information in [AL0204M2] . Preliminary Announcement
This workshop will focus on algebraic methods in formal languages, programming languages and natural languages. The aim of this workshop is to bring together those researchers on formal language theory, programming language theory, and natural language description theory, who have a common interest in the use of algebraic methods to describe syntactic, semantic and pragmatic properties of language. The workshop does not concentrate on natural language only. There is interesting use of algebraic methods in programming language processing (compiler construction and development of programming language environments) and (obviously) in formal language theory. Moreover, it is becoming clear that some of the methods developed in these fields can play a role in natural language description and processing.
Invited Speakers (preliminary list)
Some other speakers will be added to this list. A complete program of the workshop and information about registration will be available in September 1995. For more information contact: anijholt@cs.utwente.nl .
The full version of this announcement is available.
McMaster University's Faculty of Engineering is pleased to present two courses on Software Engineering: Inspecting Critical Software was presented last summer and was well received by all who attended. Software Development: An Engineering Approach, a course previously taught on-site at several development organizations, provides a broader, more basic, introduction to software design principles and will be useful for those developing software that does not require critical inspection. It is aimed at engineers who want to know how to design software well. Background, content and program for either course can be found in the full version of this announcement.
The Instructor Dr. David L. Parnas is an internationally known expert and researcher in the area of software engineering. He is well known as the first person to write about ïnformation hiding" which is the basis of modern öbject-oriented" techniques. He has also been a leader in the development of mathematical models for software description. See the full version of this announcement for further information. Interested people may contact him at:
Communications Research Laboratory
Department of Electrical and Computer Engineering
McMaster University, Hamilton, Ontario Canada L8S 4K1
Phone: + 1 905 525 9140 Ext. 27353, Fax: + 1 905 521 2922
email: parnas@triose.crl.mcmaster.ca
Administrative inquiries about either course should be directed to:
Jan Arsenault
McMaster University, Hamilton, Ontario Canada L8S 4K1
Phone: (905) 525-9140, ext. 24910, Fax: (905) 577-9099
e-mail: arsenau@mcmaster.ca
Update of information in [AL0205MO] .
The SEGRAGRA'95 Final Program and Information is available in two
forms: plain-text and LaTeX respectively.
Update of information in [AL0205MP] .
The CP'95 Final Program is available in two forms:
plain-text and LaTeX respectively.
Update of information in [AL0205CA] .
The full version of this announcement is available.
The list of accepted papers for this workshop, taking place at CP'95, is available -- see the full version of this announcement.
In August the Victoria Free-Net Association and the University of Victoria have hosted Telecommunities '95 -- a conference where members of Canadian and international telecommunities could discuss technical, legal, political and organizational trends and problems in Internet communications.
In preparation for the conference we have posted a page on the World Wide Web, with important registration and program information about Telecommunities '95 as well as general entertainment and travel tips. We have also been posting pages with valuable resource information for Free-Net users, like a comprehensive list of Canadian Free-Nets and their addresses on the web and discussion papers on Free-Net use.
We hope that you will help us promote Telecommunities '95 by posting a notice about the conference in your web pages, or note our address in any discussion groups, newsletters or news groups that you belong to.
We are expecting an energetic response to the conference, and would like to reach as many interested people as possible through these web pages. Your assistance is greatly appreciated, and we welcome any comments or questions you have about the conference. Please direct your queries to rowena@softwords.bc.ca . Many thanks,
Rowena Hart, Victoria Free-Net Association, Telecommunities '95
rowena@softwords.bc.ca
Advance Program and Registration Information are available.
Aim of the Symposium
This symposium is the eighth in a series of high-quality technical forums. It is the continuation of the previous High-Level Synthesis workshop and symposium events. The symposium is oriented towards design automation professionals and presents the latest results in emerging synthesis and system design technologies. This includes: System-level synthesis, programmable processor based design and software synthesis, hardware-software co-design and behavioral synthesis.
The program committee has selected 25 out of 79 submissions.
Regular papers will be presented in five sessions of two hours, starting with a 10 minutes verbal presentation and followed by a poster session during which refreshments will be served. In addition there will be two invited presentations in the emerging areas of multi-media system design and state-of-the-art real time system technology. An original element of the symposium is a series of workgroup focus discussion periods that will involve all attendees.
Finally two panels will address power issues at the system level and the convergence of industry expectation and system synthesis research.
WWW and Inquiries
All the latest information on ISSS'95, can now be accessed via a WWW page .
For all other inquiries send email to jerraya@imag.fr or call (+33) 76 57 47 59 during office hours (GMT+2)
Update of information in [AL0203C4] .
The (LaTeX) full version of this announcement is available.
The COCOON'95 Program and Registration Form are available, as a LaTeX file, in the full version of this announcement.
For more information, see the WWW COCOON'95 home page .
Update of information in [AL0102C9] .
The Program and Call for Participation are available.
The full version of this announcement contains the following information:
For registration to the conference, and for hotel reservations, please fill in the appropriate forms in the appendix to the full version announcement and send them to the Organisation Chair.
Further information can be found using WWW .
Update of information in [AL0205MD] .
The CONCUR'95 Preliminary Program is available.
Update of information in [AL0201C6] .
The HOA'95 Call for Participation is available.
Please visit this WWW page for the final program and registration information.
HOL'95 Information and Registration is available.
Objectives.
This meeting is the seventh in a series of annual workshops on higher order logic theorem proving and its applications, with a primary focus on the HOL system and similar systems. Previous workshops were held in Cambridge, Aarhus, Davis, Leuven, Vancouver, and Malta. Mechanized theorem provers for higher order logic have been applied to many areas, including design and verification, security, real-time systems, semantics, compiler verification, program correctness, concurrency, and program refinement. The theorem proving technology itself is also an active area of research. This conference will bring together researchers in these and related areas of investigation for the dissemination and discussion of new developments in the field.
Conference
The Conference will consist of morning and afternoon sessions during which invited papers and refereed papers will be presented and discussed. Formal proceedings will be published by Springer Verlag in the Lecture Notes in Computer Science Series. Papers discussing work in progress will also be presented, and will be circulated in an informal participants' proceedings. The Organizing Committee has invited three guest speakers, who will be announced when they have been formalized. There will also be a special session on teaching formal methods.
Registration
We prefer that you register for the conference on-line. Registration can be done on-line by using your web browser to open the HOL'95 page .
Alternately, you can fill out the registration form given in the full version of this announcement and email it to hol95-reg@lal.cs.byu.edu or fax it to 801.378.7775.
More information concerning the venue, organizers, conference program, accommodation and registration, can be found in the full version of this announcement mentioned above.
Update of information in [AL0204C3] .
The Workshop Call for Participation is available.
Update of information in [AL0204CF] .
The IWPTS'95 Final Program is available.
To obtain current information, please browse the IWPTS'95 WWW pages .
The full version of this announcement is available.
A registration form is attached to the full version of this announcement. A list of submitted abstracts is available.
Student accommodation has been adopted in order to keep the costs down.
Registrations should be sent to Angela Leeke <akl@cl.cam.ac.uk>
The Proceedings have been sent for printing: 17 papers, 264 pages.
The Preliminary Programme is now available.
If you are attending the Isabelle Workshop, please check that your entry is correct.
If you would like to attend and have not done so, please register immediately, using the form .
General comments on the programme are also welcome.
Update of information in [AL0102C1] .
The MFCS'95 Information Bulletin is available.
Up-to-date information is maintained on the MFCS'95 WWW page .
Editor's Note. To-date, here's the actual MFCS'95 WWW page .
Update of information in [AL0204C6] .
The SAS'95 2nd Call for Participation is available.
Note: This is the second announcement of this conference; this version includes registration information at the end.
The programme, call for participation, and registration information are available .
Upon request, latex sources will be mailed out to people who cannot access WWW documents. (email: helen@dcs.gla.ac.uk)
The FORTE'95 Preliminary Program is available.
The full version of this Call for Papers is available in two
forms: plain-text and LaTeX respectively.
The goal of the AMAST Conferences is to put software development technology on a firm, mathematical foundation. Particular emphasis is given to algebraic and logical foundations of software technology. An eventual goal is to establish algebraic and logical methodology as a practically viable and attractive alternative to the prevailing ad hoc approaches to software engineering.
Topics of interest include, but are not limited to, the following:
Prospective authors are invited to submit 6 copies of unpublished papers (double spaced, max 15 pages for papers, 4 pages for system demo proposals) in an area relevant to the conference theme. Papers should provide adequate information for the reviewers to assess significance and anticipated impact on the foundations of software technology.
Submissions (papers and system demo proposals) must be sent toImportant Dates
Martin Wirsing, AMAST'96 Program Chair, Institut für Informatik,
Universität Muenchen, Leopoldstr. 11B D-80802 München, Germany
e-mail: amast96-info@informatik.uni-muenchen.de
Submission of Papers: November 15, 1995Further Information
Submission of System Demo Proposals: December 15, 1995
Submission of Student Research Papers: June 1, 1996
Notification of Acceptance/Rejection: February 1, 1996
Camera-ready Version of Accepted Papers: March 15, 1996
Education Day: July 1, 1996
Conference: July 2-5, 1996
The full version of this Call for Papers is available.
The 3rd AMAST Workshop on Real-Time Systems is aimed at the promotion and development of mathematical foundations of real-time systems. The theoretical investigation of real-time systems, however, has still not reached maturity. The variety of approaches distance designers from theoretical methodologies and their implementations described in the literature. Abstract and formal methods, although providing powerful tools for designers, are applied only by academics. It is the aim of the third AMAST Workshop to launch a challenge for unified approaches in modeling and designing real-time systems. For this reason the organizers will try to gather together top researchers in the area of real-time systems from both the computer science and control areas of expertise. As in all AMAST conferences and workshops, emphasis will be given to algebraic and logical foundations of software technology.
Submissions
The program will consist of invited talks and twelve selected papers. We invite papers reporting original research in algebra and logic. Prospective authors are invited to submit 6 copies, at most 15 double spaced pages in length, in an area relevant to the conference theme. Submissions must be sent to the program chair at the address below.
Aurel Cornell, III International AMAST Workshop on Real-Time SystemsMore detailed submission information can be found at the URL at the top of this page and prospective authors are advised to consult this.
Program Chair, Department of Computer Science
230 TMCB Brigham Young University, Provo, Utah 84602, USA
e-mail: AUREL@csoffice.byu.edu
Important Dates
Submission of Papers: October 15, 1995
Submission of System Demo Proposals: November 15, 1995
Notification of Acceptance/Rejection: December 1, 1995
Camera-ready Version of Accepted Papers: January 15, 1996
(LaTeX) Preliminary Announcement and Call for Papers .
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, Swarm, 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.
A typical, but not exclusive list of topics of interest are: coordination problems within concurrent, distributed, object oriented, functional and logic programming; concurrent computation, constraint programming, computation models based on the chemical reaction metaphor and related areas; software environments for the development of coordinated applications; semantics and reasoning about coordination; case studies with industrial relevance.
Submissions. Authors are invited to send full papers (in English, up to 15 pages) to the PC chairman, at the address mentioned below. Simultaneous submission to other conferences or journals is not allowed. Electronic submission is encouraged via e-mail, in the form of uuencoded compressed PostScript(TM) files. Each submission should be accompanied by a 100 word summary and a single postal and e-mail address for communication. Further information about COORDINATION'96 may also be obtained from the program chair.
Program Chair: Chris Hankin (London) <coord@doc.ic.ac.uk>
Department of Computing, Imperial College
180 Queen's Gate, London SW7 2BZ, UK
Important Dates
Deadline for submissions: October 30, 1995
Notification of acceptance: December 15, 1995
Camera-ready version due: January 15, 1996
The full version of this announcement is available in two
forms: plain-text and LaTeX respectively.
This conference, to be held in conjunction with the 12th Shanks Lectures, will highlight significant recent developments in modern algebra and its interdisciplinary interactions with logic, combinatorics and computer science. The aims of the conference are to bring together researchers working in a broad range of contemporary algebra and its applications, and provide a forum for the participants to meet and jointly explore unsolved problems of common interest in an informal atmosphere. The following areas will be emphasized.
Researchers in neighboring areas whose interests fit the general aims of the conference are encouraged to participate. The scientific program of the conference will consist of eight plenary hour lectures of general interest, and six special sessions each featuring an invited hour lecture and 30--minute contributed talks.
Organizing Committee: W. J. Blok (Illinois at Chicago), R. Freese (Hawaii), G. F. McNulty (South Carolina at Columbia), M. Mislove (Tulane), K. Keimel (Darmstadt), R. McKenzie (Vanderbilt), D. Pigozzi (Iowa State), R. W. Quackenbush (Winnipeg), M. Sapir (Nebraska at Lincoln), S. Tschantz (Vanderbilt), C. Tsinakis (Vanderbilt), R. Willard (Waterloo).
Conference Co-Chairs: R. McKenzie and C. Tsinakis.
Expression of Interest. If you are interested in the conference, please fill in and return (preferably by email) the Expression of Interest Form --- see the full version of this announcement.
Conference e-mail address: cmaa@math.vanderbilt.edu
A Call for Papers is available.
Deadline for submission: 19 September 1995
CAAP Colloquium on Trees in Algebra and Programming
This colloquium series was originally devoted to the algebraic and combinatorial properties of trees and their roles in various fields of Computer Science. Its scope has extended to several other structures, such as words or graphs, which play similar roles and deserve similar theoretical studies. In keeping with these traditions, CAAP'96 will cover algebraic, logical and combinatorial properties of discrete structures and their application to Computer Science.
CC International Conference on Compiler Construction
The International Conference on Compiler Construction provides a forum for presentation and discussion of recent developments in the area of compiler construction, language implementation and language design. Its scope ranges from compilation methods and tools to implementation techniques for specific requirements of languages and target architectures. It also includes language design and programming environment issues which are related to language translation. There is an emphasis on practical and efficient techniques.
ESOP European Symposium on Programming
This conference is devoted to fundamental issues in the specification, analysis and implementation of programming languages and systems. It particularly welcomes research which bridges the gap between theory and practice: for example, practical studies based on theoretical developments and theoretical developments with a clearly identified potential for practical application. The emphasis is on the soundness and correctness of the approach.
Further information, including detailed lists of topics, submission requirements and addresses, program committee, invited speakers, local arrangements, system exhibitions, and satellite meetings, can be found in the Call for Papers mentioned above. A full version and further information are available .
The full version of this announcement is available.
The mission of the bi-annual TARK conferences is to bring together researchers from a number of fields, including A.I., Cryptography, Distributed Computing, Economics, Game Theory, Linguistics, Philosophy, and Psychology, in order to further our understanding of interdisciplinary issues involving formal reasoning about rationality and knowledge. Topics of interest include, but are not limited to, semantic models for knowledge, for belief, and for uncertainty, bounded rationality and 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. TARK-VI is the first to be held outside the United States.
Information for Authors
Submissions are invited to TARK-VI. Two types of submission are invited, papers reporting on novel research, and expository papers. Each submission should be clearly identified as belonging to one category or the other. Prospective authors should consult the detailed submission information in the full version of this announcement.
Deadline for Submissions
The deadline for submission of abstracts is October 10, 1995.
Authors will be notified of acceptance by December 15, 1995.
Camera-ready copies will be due by January 15, 1996.
Conference Chair
Johan van Benthem, ILLC,
Dep't of Mathematics & Computer Science, University of Amsterdam
Plantage Muidergracht 24, NL-1018 TV Amsterdam, The Netherlands
email: johan@fwi.uva.nl
Program Chair
Yoav Shoham, Computer Science Department, Stanford University,
Stanford, CA 94305, USA
email: shoham@cs.stanford.edu
The First Announcement and Call for Papers is available.
The original announcement is also available.
Object-based Distributed Computing are being established as the most pertinent basis for the support of large, heterogeneous computing and telecommunications systems. The advent of Open Object-based Distributed Systems, OODS, brings new challenges and opportunities for the use and development of formal methods.
The objective of FMOODS is to provide an integrated forum for the presentation of research in several related fields, and the exchange of ideas and experiences in the topics concerned with the formal methods support for Open Object-based Distributed Systems.
Topics of interest include but are not limited to: formal models for object-based distributed computing; semantics of object-based distributed systems and programming languages; formal techniques in object-based and object-oriented specification, analysis and design; refinement and transformation of specifications; multiple viewpoint modelling and consistency between different models; formal techniques in distributed systems verification and testing; types, service types and subtyping; specification, verification and testing of quality of service constraints; formal methods and object life cycle.
Submission. Please send 5 copies of your manuscript to:
Elie NAJM, ENST, Networks DepartmentProspective authors should consult the detailed submission information in the full version of this announcement.
46, Rue Barrault, 75013 Paris, France
E-mail: najm@res.enst.fr
Important Dates
10 November 1995 Submission deadline
10 January 1996 Notification of acceptance
30 January 1996 Camera ready copy due
Inquiries can be sent to: fmoods96-request@res.enst.fr
The Call for Papers is available.
The 23rd annual meeting of the European Association for Theoretical Computer Science will take place in Paderborn, Germany. Papers presenting original contributions in any area of theoretical computer science are being sought. Topics include (but are not limited to): computability, automata, formal languages, term rewriting, analysis of algorithms, computational geometry, computational complexity, symbolic and algebraic computation, cryptography, data types and data structures, theory of data base and knowledge bases, semantics of programming languages, program specification, transformation and verification, foundations of logic programming, theory of logical design and layout, parallel and distributed computation, theory of concurrency, theory of robotics.
Submissions. Authors are invited to submit seven copies of an extended abstract, not exceeding 12 pages, by November 15th, 1995, to:
Friedhelm Meyer auf der HeideSimultaneous submissions of papers to any other conference with published proceedings are not allowed.
Dept. of Mathematics and Computer Science, & Heinz Nixdorf Institute
University of Paderborn, D-33095 Paderborn, Germany
Important Dates
Deadline for submission: November 15th, 1995
Notification of acceptance: February 16th, 1996
Final manuscript: April 1st, 1996
More Information. See the Call for Papers. A WWW page for ICALP'96 has been installed.
The final program will be sent to those who have submitted a paper and to all EATCS members. To add your name to the mailing list or to obtain further information, please contact:
Walter Unger, Rolf Wanka
Dept. of Mathematics and Computer Science
University of Paderborn, D-33095 Paderborn, Germany
email: icalp96@uni-paderborn.de
The First Call for Papers is available in two forms:
plain-text and LaTeX respectively.
In various areas of logic, computation, language processing, and artificial intelligence there is an obvious need for using specialized formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialized systems must be combined with each other, and they must be integrated into general purpose systems. The development of general techniques for the combination and integration of special systems has been initiated in many areas, and the Workshop ``Frontiers of Combining Systems'' intends to offer a common forum for these research activities.
Suggested, but not exclusive topics of interest for the workshop are: combination of logics; combination of constraint solving techniques and combination of decision procedures; integration of equational and other theories into deductive systems; combination of term rewriting systems; integration of data structures into CLP formalisms and deduction processes; hybrid systems in computational linguistics, knowledge representation, natural language semantics, and human computer interaction; logic modelling of multi-agent systems.
Submissions: A PostScript version of the full paper (preferable LaTeX format) via e-mail, and one hard copy, should be received by the due date. Results must be unpublished and not submitted for publication elsewhere. For other submission requirements, see the Call for Papers.
Please send submissions to the local organizer:
K.U. Schulz, CIS, University of Munich,
Wagmüllerstr. 23, D-80538 München, Germany
E-mail: schulz@cis.uni-muenchen.de
Important Dates
Submission Deadline: October 16, 1995
Notification of Acceptance: December 1, 1995
Final Versions due: January 1, 1996
Further Information on FroCoS'96 is available by WWW (under ``events'').
The (LaTeX) full version of the Call for Papers is available.
Following the previous meetings in Tübingen (1989), Kista (Sweden) (1991), Bologna (1992) and St Andrews (1993), and the post-conference workshop at ICLP'94 on Proof-Theoretical Extensions of Logic Programming, the 5th international workshop on Extensions of Logic Programming will be held in Leipzig (Germany).
Topics. ELP aims at stimulating research on extensions of logic programming languages, especially those based on proof theory, and at disseminating insights into the relations between the logics of those languages, implementation techniques and the use of these languages in applications. Typical, but not exclusive, topics of interest are: proof-theoretic foundations; integration with functional programming; non-classical and linear logic programming; non-monotonicity; disjunctive logic programming; negation as failure; constructive negation; applications and implementations.
Submissions. Send four copies of your manuscript to:
ELP'96/Heinrich Herre, Institut für Informatik,Alternatively, electronic submission of Postscript files is welcome. The final version will need to be prepared using the Springer style files or an approved simulation thereof. Papers must describe original, previously unpublished research, be written and presented in English, not exceed 15 A4 pages, and not be simultaneously submitted for publication elsewhere. Prospective authors should consult the detailed submission information in the full version of this announcement.
Universität Leipzig, Augustusplatz 10-11, D-04109 Leipzig, Germany
Further Information is available .
Important Dates
Deadline for submissions: September 15, 1995
Notification of acceptance/rejection: November 1, 1995
Deadline for final text: December 15, 1995
The full version of the First Call for Papers is available.
This workshop is a continuation of workshops on the same topic held in Lautenbach near Karlsruhe (1992), Marseille (1993), Abingdon near Oxford (1994) and St. Goar near Koblenz (1995).
Topics. Given the increased interest in tableaux-based theorem proving, the workshop intends to bring together researchers interested in the mechanisation of reasoning with tableaux and related systems. Included (but not exclusively) will be: analytic tableaux; model elimination; connection method; sequent calculi.
The workshop has a dual focus, bringing together people who develop tableaux-like calculi for classical and non-classical logics and people involved in the practical implementation of tableaux-like calculi.
Submissions. Submit papers in one of the following categories:
All submissions must be in English. Authors should send four copies, preferably in LaTeX llncs style to:
Ugo Moscato, Information Science Department, University of MilanElectronic or fax submissions are not acceptable. Submissions of the work to other conferences or journals are not allowed.
Via Comelico 39/41, 20135 Milan, Italy. E-mail: tab96@dsi.unimi.it
Important Dates
Deadline for submissions: November 17th, 1995
Notification of acceptance: middle of February 1996
Proceedings. It is intended to publish the conference proceedings within the LNAI series of Springer. All accepted papers from category 1. will be included.
Latest Information regarding Tableau'96 can be found via
The full version of this announcement is available.
The IEEE Computer Society Technical Committee on Parallel Processing invites engineers and scientists from around the world to participate in the 10th International Parallel Processing Symposium. Established to advance knowledge in all areas of parallel processing and related technologies, the symposium is the committee's primary event for presenting the most recent research and development findings. In its 10th year, the now standard IPPS events include contributed technical papers, keynote speeches and panels, workshops and tutorials, and an industrial track and commercial exhibits.
Workshops offer the opportunity for in-depth exploration of selected topics.
Tutorials. Proposals are solicited for organizing full or half-day tutorials.
Industrial Track/Commercial Exhibits. These paired activities give manufacturers of commercial products the opportunity to both explain and demonstrate their wares.
Important Dates
Paper Submission Deadline: September 20, 1995
Workshop Proposal Deadline: September 29, 1995
Tutorial Proposal Deadline: October 31, 1995
Industrial Track Deadline: October 31, 1995
Paper Review Decisions Mailed: December 20, 1995
Camera Ready Manuscript Due: January 23, 1996
The full version mentioned above contains the following information:
Call for Participation (Workshops, Tutorials, Industrial/Commercial)To receive a hard copy of the announcement send e-mail to Regina Morton at morton@pollux.usc.edu
Call for Papers (Instructions, Program Committee)
Organization (Organizers/Advisors, Location, Dates)
Updated meeting information may be retrieved from the Web.
The full version of this Call for Papers is available.
The aims of the Workshop are to promote the interests of researchers and users of software development methods which combine the use of formal methods with other heuristic or semiformal methods (including structured and object-oriented methods), to evaluate integrated methods in the light of current research and practice, and discuss future research directions and priorities. The Workshop will include both technical presentations and working groups with active participation.
Contributions are invited in the following areas (but this list is not exclusive): different approaches to integration; process models; object orientation; integrating formal methods with object-oriented analysis and design methods; using integrated methods for verification and validation; tool support for integrated use of formal and structured methods; industrial experience/case studies; using integrated methods in education and training.
Submissions. There are three types of submissions: research papers (up to 20 pages in length) describing new theoretical work; industrial experience reports. These may be much shorter, and need not give so much technical detail; posters (four A4 sheets) outlining work in progress. Submissions should be sent to:
Tony Bryant, Leeds Metropolitan University,Prospective authors should consult the more detailed submission information in the full version of this announcement.
Faculty of Information and Engineering Systems, The Grange,
Beckett Park, Leeds, LS6 3QS, England,
Email: a.bryant@lmu.ac.uk
Important Dates
Intention to submit: 31 July 1995
Deadline for submission: 29 Sep 1995
Authors notified: 8 Dec 1995
Camera-ready copy: 26 Jan 1996
The full version of this Call for Papers is available.
The ACM SIGPLAN International Conference on Functional Programming is a new annual conference combining the established LISP and Functional Programming (LFP) and Functional Programming and Computer Architecture (FPCA) conferences. Papers presented at the conference must describe new ideas or experimental results that have not previously been published. Suggested areas for submissions include (but are not limited to) the following: language design; compilation methods; architectural support and interaction; program analysis and optimization; programming logics; program transformation; semantic foundations; type theory; garbage collection and run-time systems; input/output, control, and store effects; extensions for parallelism, non-determinism, and concurrency; implementation paradigms: direct- and continuation-passing, graph reduction, and data flow; parallel and distributed implementations; applications and case studies. Languages of interest include established languages such as Lisp, Scheme, Sisal, ML, Haskell, and Id, as well as novel designs.
Submissions should be sent to the program chair:
R. Kent Dybvig, Computer Science Department, Lindley Hall 215Prospective authors should consult the detailed submission information in the full version of this announcement or at the URL below.
Indiana University, Bloomington, IN 47405-4101, USA
dyb@cs.indiana.edu
Important Dates
Submission: October 27, 1995
Notification of acceptance or rejection: December 22, 1995
Final camera-ready versions: January 27, 1996
Submission Information and other inquiries:
contact icfp96@cs.indiana.edu
Additional information
The full version of this announcement is available.
The aim of this workshop is to bring together researchers in the areas of proof theory, logic programming language design, programming language semantics. At a time when there are many new developments occurring in each of these disciplines, it is important that each community be well-informed about the others' progress. In particular, we suggest that it is only by such communication that progress will be made in understanding the design and semantics of logic programming languages. Moreover, we suggest that both proof theory and semantics may find challenging new problems arising in logic programming.
Another important aspect of this workshop is its potential to bring together logic and functional programmers via the common grounds of proof theory and semantics. Logic programming is often thought of as interpreting formulae as programs and proof-search (including unification) as computation, whereas a functional programmer's view of proof theory is often that a proof is a program and cut-reduction is computation. Hence a common focus on the applications of proof theory to programming tasks has the potential not only to explore new logic programming techniques but also to provide a forum for the integration of the logic and functional programming paradigms.
Important Dates
Intention to submit: September 1
Submissions due: September 15
Notification: October 27
Final version due: November 20
Contact Address
James Harland, Dep't of CS, Royal Melbourne Institute of Technology
GPO Box 2476V, Melbourne, 3001 Australia
email: jah@cs.rmit.edu.au, phone: +613 96602045, fax: +613 96621617
See the full version of this announcement for: specific technical issues addressed by this workshop, submission guidelines, organizers.
The Call for Papers & Call for Participation is available.
The objective of the workshop is to bring together researchers from the Nordic and Baltic countries interested in programming theory, in order to improve mutual contacts and cooperation. Typical topics of the workshop include (but are not limited to): o Semantics of programs o Programming logics o Program verification o Formal specification of programs o Program synthesis o Program transformation and program refinement o Modelling of concurrency o Programming methods o Tools for program construction and verification
The workshop will mainly consist of 30-minute presentations, in parallel sessions, with time between these for informal discussions. Participants are encouraged to present work in progress. A collection of abstracts of presentations will be distributed at the start of the workshop. The proceedings will be published as a technical report.
Submission: If you wish to give a presentation, please enclose a one-page abstract of the talk. If the number of proposed talks exceeds the number of slots available, the Programme Committee will make a selection, based on the submitted abstracts.
Demonstrations: If you wish to demonstrate a non-commercial system that is related to the workshop topics, please specify what hardware and software is required, and enclose a one-page summary of the system. Demonstrations will only be organized if there is sufficient demand.
Further details about participation (limited to 75 participants!), program committee, organization, cost, accommodation, and registration form, are available in the full version of the Call mentioned above.
Deadline for submission and registration: September 25.
Applications are invited for a two year postdoctoral position to start as soon as possible to work with Abbas Edalat on the EPSRC project "Foundational Structures in Computer Science" under the subtitle "Computational Measure and Integration Theory". The post is one of four in the project; other investigators include Samson Abramsky, Mike Smyth and Steve Vickers. It has arisen as a result of the develpment of a new order-theoretic measure and integration theory at the interface of mainstream mathematics and theoretical computer science. The aim will be to investigate various topological, measure-theoretic and domain-theoretic aspects of the new theory as well as its various applications. Candiates should have a PhD in Mathematics or Theoretical Computer Science with a strong background in General Topology. They should also have knowledge of at least one of Classical Measure Theory and Continuous Lattice Theory (Domain Theory), as well as the serious willingness to acquire knowledge of the other.
Salary (including London allowance) will be on the R&A IA scale (17,700-19,947 pounds a year).
Informal enquiries should be directed to Abbas Edalat.
Applicants are required to send a CV, a list of publications, a description of current and past research interests and the names and addresses (including email) of two referees either by post or email to
Abbas Edalat (ae@doc.ic.ac.uk)
Department of Computing
Imperial College
180 Queen's Gate
London SW7 2BZ.
The full version of this information is available.
The Department of Computer Science is calling for applications for financial awards to support three students to pursue a doctoral program in computer science, at least one in theoretical computer science.
The Department offers graduate programmes leading to the PhD degree with specialisations including (but not limited to) algorithmic information theory, artificial intelligence, combinatorics, data compression, data communications and networks, distributed computing, graphics, multimedia and hypermedia systems, neural networks, parallel computation, programming languages and systems, program derivation, rehabilitation computing, software engineering, theory of computation, and visual programming.
Financial aid comes in the form of scholarships of around NZ$12,000 and fellowships of around NZ$5000 (the latter are subject to tax). Limited opportunities also exist for teaching assistantships, providing a similar level of support.
Further information on the Department may be obtained from our world wide web pages .
To investigate and champion the integration of formal design verification techniques into the design cycle of one of the development projects within AT&T, in one of the labs near Murray Hill in New Jersey.
The job requires the construction of a machine readable database that collects project design decisions at the earliest possible stage of a system design. The database should be compatible with existing CASE tools, and support links to verification tools such as SPIN. The formal verification framework is intended to support the entire software design cycle, from requirements analysis up to and including automated test sequence generation and assessment techniques.
Solid background in system engineering, preferably with exposure to telephony network operation systems. The ideal candidate has several years of experience being part of a system design team, and has experience with the application of formal verification techniques. Familiarity with programming languages such as C or C++, with documentation tools such as FrameMaker, and with CASE tools, are all a plus.
gerard@research.att.com
The Department of Computational & Applied Mathematics invites applications for tenure-track assistant professorship appointments in all areas of mathematical programming, particularly the computational aspects of integer programming, combinatorial optimization, and interior point methods. Applicants should demonstrate both breadth of interest and promise in research and teaching. Appointment at more senior rank may be possible for exceptional candidates with appropriate records of accomplishment.
Rice University is a private research university with an exceptional undergraduate population and a long tradition of excellence in undergraduate science and engineering education. The Computational & Applied Mathematics Department hosts research programs in Linear and Integer Programming, Nonlinear Optimization, Numerical Linear Algebra, Parallel Computing, and Numerical Solution, Optimal Design, and Inverse Problems for Partial Differential Equations. The department also has close ties to the Center for Research in Parallel Computation, an NSF Science and Technology Center.
Please furnish vita, transcripts, reprints, and three letters of recommendation before 31 December 1995 to:
Chair, Staffing Committee
Computational & Applied Mathematics Department
Rice University
PO Box 1892
Houston, TX 77251-1892
The full version of this contribution is available.
The department of Computer Systems at Uppsala University offers several positions as visiting researcher starting in Autumn 1995.
Uppsala is located 70 km north of Stockholm. The departments of computer systems, computing science, mathematics, numerical analysis, and automatic control, are located together on a newly renovated campus. Research at the department of Computer Systems is focussed on
The positions are intended for one (possibly two) years. We seek applicants with a PhD and a research record in area(s) that are relevant to the research at the department. In particular we are looking for applicants in the following areas.
more information: contact Bengt Jonsson, bengt@docs.uu.se
more information: contact Hans Hansson, hansh@docs.uu.se
more information: Per Gunningberg, per.gunningberg@docs.uu.se
Interested? Please send CV and state your interests and requirements by e-mail, fax or physical mail to
(Bengt Jonsson | Hans Hansson | Per Gunningberg)
Uppsala University, Dept of Computer Systems
Box 325, S - 751 05 Uppsala, Sweden,
fax: +46 - 18 - 55 02 25
e-mail: (bengt|hansh|perg)@docs.uu.se
Two Research Fellows are required for a 3-year project entitled ``Foundations for the Integration of Concurrent Distributed and Functional Computation'', under the direction of Prof. M. Hennessy and funded by the EPSRC.
The aim of the project is to
The project will start on 1/10/95 and salary will be related to the academic 1A scale. A Ph.D. in Computer Science or Mathematics or equivalent experience is required. In addition to normal research duties the successful candidate will be expected to provide some assistance to undergraduate teaching.
More details of the project and the conditions of service are available .
To apply please submit applications to
Prof M Hennessy
School of COGS
University of Sussex
Falmer
Brighton BN1 9QH
UK
Tel: +44 01273 678101
email: matthewh@cogs.sussex.ac.uk
Applications should include a detailed curriculum vitae, names of three referees with their email addresses and copies of any relevant publications.
The Indiana University Computer Science Department seeks applicants for at least one tenure-track faculty position, beginning with the academic year 1996-97. Application deadline is February 1, 1996. We are looking for exceptional researchers at the forefront of their field, who will also make strong contributions to the educational mission of the department. The position is slated at the assistant professor level, but a senior appointment might be possible for truly exceptional candidates.
The department plans, over the next few years, to develop its strength in programming languages and methodology into a first-class group, one that would also enhances our vigorous interdisciplinary programs in applied logic, scientific computing, and cognitive science. For the position above we are looking for someone with a strong research program in programming languages, including the logical aspects of the subject and its relations to high performance computing.
The department occupies a recently renovated spacious limestone building, and has extensive state-of-the-art computing facilities. The attractive wooded campus of Indiana University is located in Bloomington, voted one of the most cultural and livable small cities in the US, and a mere 45 minute drive from an international airport.
Please send a detailed CV and a list of references to
Faculty Search, Computer Science Department,Please address email enquiries to search@cs.indiana.edu .
Indiana University, Bloomington, IN 47405.
Indiana University is an Equal Opportunity / Affirmative Action Employer.
Applications are invited for a new Chair in Computer Science in the Department of Mathematics and Computer Science, tenable from l January 1996, or as soon as possible thereafter. The creation of the chair will consolidate and extend the work of the Computer Science Group within the Department. Applicants should have strong research records in Computer Science, and be able to provide academic leadership to the Computer Science Group. The Department would particularly welcome applications from people working in applicable areas of Computer Science which would complement the existing research areas, while making use of the expertise already available. In addition to this appointment, it has been agreed that a Lectureship in Computer Science will subsequently be advertised, and the appointee should expect to play a major role in the filling of this position.
Salary will be within the Professorial Range.
Informal enquiries are welcome and should be addressed to Professor Will Light, Head of Department, telephone +44 (0)116 252 3884, or email jobs@mcs.le.ac.uk .
Further particulars may be obtained from the
Staffing Office (Academic Appointments)or from the WWW page .
University of Leicester
University Road
Leicester, LE1 7RH
U.K.
telephone +44 (0)116 252 2422, fax number +44 (0)116 252 5140,
U.K. candidates should submit thirteen copies of their application (overseas candidates may submit one copy).
Closing date for applications is 1 September 1995.
The Department of Mathematics is seeking a career-track lecturer in Mathematics from 1st January 1996.
The Department particularly encourages applications from those whose research interests lie either in the field of Discrete Mathematics, or in areas of Mathematics with applications in the Social Sciences (e.g., Game Theory, Applied Probability Theory, Stochastic Calculus, Non-Linear Analysis, Learning Theory). However, consideration will be given to outstanding applicants in any branch of Mathematics.
The salary will be on the Lecturer Scale A/B at a point commensurate with experience within the range of GBP 15514 to GBP 26430 plus GBP 2134 London Allowance per year.
The closing date for applications is 24 August 1995. It is expected that interviews will be held in September 1995.
For further details and an application form please send a large SAE to Personnel Services, London School of Economics, Houghton Street, London WC2A 2AE quoting reference LS/Maths.
The full version of this announcement is available.
The Advanced Decision Support System (ADSS) organization at AT&T Bell Labs is interested in outstanding candidates who are considering consulting and development careers in Operations Research and Computer Science.
What AT&T Bell Labs ADSS requires:
Education: Advanced degree (M.S. or Ph.D.) in Operations Research, Computer Science or related field required. In addition, an undergraduate degree in Engineering is desirable.
OR Expertise: Practical experience and a theoretical background in general optimization and/or stochastic processes required. Knowledge of network analysis, system design and analysis, decision support systems, and basic statistical analysis desirable.
Work Experience: A minimum of 2 years of non-academic professional experience required (may be waived for an applicant with a Ph.D.). Experience in the telecommunication area is desired. Previous consulting experience a plus.
Computer Skills: Proficiency in programming C++ or C required. Knowledge of UNIX, object-oriented methodology, use of state-of-the-art optimization and statistical packages desirable. Experience with graphics and spreadsheets a plus.
General: Highly developed oral and written communication skills as well as excellent interpersonal skills. Willingness to learn, self-motivation, and self-management.
What AT&T Bell Labs ADSS can offer:
A challenging and informal work environment. Work on leading-edge problems, develop innovative decision technologies, using the latest in high-performance commercial software technology (object oriented development, etc.). An opportunity to make an impact in a leading industrial laborotory environment.
Competitive salaries, excellent benifits, and exciting career growth.
How to apply: See the full version of this announcement.
The Decision Support Systems (DSS) organization of TransQuest Information Solutions, an AT&T and Delta Air Lines joint venture, is interested in outstanding candidates who are considering consulting and software development careers in Operations Research and Computer Science.
The qualified candidates will be responsible for the analysis of operational problems and the development of large-scale decision support systems for the transportation industry with immediate focus on the airline industry. Requirements include an advanced degree in Operations Research, Computer Science, or related field, strong software development capabilities (e.g. UNIX, Windows development environment, C++ programming, etc.), previous relevant work experience, good interpersonal skills, and a high aptitude for problem solving. Academic specialization and/or work experience in combinatorial/network flow problems, forecasting, routing and scheduling are desirable.
The selected candidates will work in Atlanta with a possibility of short term training at AT&T Bell Laboratories in Holmdel, NJ. TransQuest Information Solutions offers a competitive salary and a comprehensive benefits packages plus exciting career growth. For consideration, please send a resume with cover letter to:
Attn: Ms. Susan Sligh
Dept. 800
TransQuest Information Solutions
1001 International Boulevard
Atlanta, GA 30354-1801
e-mail: attmail!transqst!TRANSQUEST!A3!TNail
Fax: (404)714-1964
The Research Center in Computing Science at Nancy (CRIN Research Unit of CNRS 262) contains an active research group in formal methods and applications, namely MODEL lead by Prof D MERY. Major areas of research include:
Applications are invited from students with good graduates degrees in Computer/Computing Science or with a DEA (Computing Science) (or an equivalent degree) to join this group to study towards a D. Phil. degree. A scholarship for a suitably qualified candidate is for the october 1995 entry. The level of the maintenance grant is linked to the standard grant offered by CNRS which for 1994/1995 was approx. set at 8000 FF per month. The grant is a three-year contract.
Scholarship: The successful candidate will be expected to work on project in collaboration with industrial partner. The main topic is the formal specification of service in IN and the development of tools.
Further Information: On the WWW .
More detailed information on the studentship is available from mery@loria.fr .
How to apply:
Send a full and complete CV (poscript by email), a copy of the degree certificates and arrange for three references to be sent directly to:
Professor Dominique MERY
CRIN-CNRS & INRIA Lorraine
Batiment LORIA
BP 239
54506 Vandoeuvre-les-Nancy
France
email: mery@loria.fr, phone: +33 83 59 20 14, fax: +33 83 41 30 79
The Departamento de Informatica of the University of Minho has available, for the academic year 1995/96, the following positions:
Candidates are required to have a Ph.D in a suitable area and some research experience. The initial appointments will be made on the Assistente level (grade 135 of the Civil Service index) but, as a function of the research and teaching experience of the the candidate, can be upgraded to Professor Auxiliar level.
Details and closing dates for the application can be obtained at the Department Office at sec@di.uminho.pt .
The original announcement is available on the WWW.
Secretaria do Departamento de Informatica
Universidade do Minho, Campus de Gualtar
4700 Braga, Portugal
Tel: +351-53-604470, Fax: +351-53-612954
This paper, describing a further development of Isabelle's I/O-Automata theory, has been available for some time.
We propose a combination of model checking and interactive theorem proving where the theorem prover is used to represent finite and infinite state systems, reason about them compositionally and reduce them to small finite systems by verified abstractions. As an example we verify a version of the Alternating Bit Protocol with unbounded lossy and duplicating channels: the channels are abstracted by interactive proof and the resulting finite state system is model checked.
The paper is available.
Update of information in [AL0103CB] .
The aim of the workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, was to bring together researchers and practitioners interested in the development and application of tools and algorithms for specification, verification, analysis and construction of distributed systems. The overall goal of the workshop was to compare the various methods and the degree to which they are supported by interacting or fully automatic tools.
The 23 papers of the proceedings cover the following topics: refinement-based verification and construction techniques; compositional verification methodologies; analysis and verification via theorem-proving; decision procedures for verification and analysis; specification formalisms, including process algebras and temporal and modal logics; analysis techniques for real-time and/or probabilistic systems; approaches for value-passing systems, tool sets for verification and analysis case studies. There were special sessions for demonstration of verification tools.
Copies of the Proceedings and of individual papers in A4 format are electronically accessible through WWW.
Email abstract95@cs.umd.edu to obtain LaTeX or postscript code for the abstracts.
These are short announcements of work in the field of Structures.
The full version of this information is available.
Linear Logic, introduced in 1986 by J.-Y. Girard, is based upon a fine grain analysis of the main proof-theoretical notions of logic. The subject develops along the lines of denotational semantics, proof-nets, geometry of interaction. Its basic dynamical nature has attracted computer scientists, and various promising connections have been made in the areas of optimal program execution, interaction nets and knowledge representation.
This book is the refereed proceedings of the first international meeting on linear logic held at Cornell University in June 1993. Survey papers devoted to specific areas of linear logic, as well as an extensive general introduction to the subject by J.-Y. Girard have been added, so as to make this book a valuable tool both for the beginner and for the advanced researcher.
Further details can be obtained from the publisher by email
science@cup.cam.ac.uk
A draft version of this paper is available.
We present a graph implementation of (optimal) $\lambda$-calculus reductions---here restricted to $\lambda{I}$-calculus---in the tradition of Lamping [1] and Gonthier et al. [2,3]. But, differing from the main literature, we unify all the kinds of control nodes into multiplexer nodes.
The techniques used to prove the algorithm correct are completely new and base on the so-called sharing-morphisms via which we simulate sharing-nets reductions by unshared-nets reductions.
By such techniques we prove to be sound a set of _propagation rules_, the $\pi$-rules, more general than any other one in literature, and among which there is an absorption rule which has no equivalent in the previously proposed algorithms. The $\pi$-rules give a solution to some nasty problems connected with the so-called ``spurious control nodes'' and allow the internalization of the read-back into the rewriting system: the $\pi$-normal formal of a sharing-net being the $\lambda$-tree represented by it.
Finally, by restricting the rewriting system to the shared $\beta$-rule and to a suitable subset of the $\pi$-rules it is indeed possible to recover L\'evy optimality.
Models and techniques borrowed from classical algebraic topology have recently yielded a variety of new lower bounds and impossibility results for distributed and concurrent computation. This paper explains the basic concepts underlying this approach, and shows how they apply to a simple distributed problem.
This article is available .
The full version of this information is available.
In this note I show how to give a continuation semantics to an extension of Parigot's mu-calculus from which there follows a simple equational presentation and rewrite semantics. Though I have had the semantics since quite a time the idea to use it for extending mu-calculus and deriving a nice rewrite semantics for it from this semantics came to me during a talk of Philippe Audebaud during his talk at the Scott conference in Darmstadt this spring/summer. I don't precisely remember his presentation, so I cannot compare what's below with his work; but it looks simpler to me than what I remember to have seen in the talk. Maybe Philippe has some further equations to guarantee confluence or things like that. I personally haven't checked confluence myself. But it is clear that the machine computations of an extended Krivine's machine are reflected one-to-one by rewrite derivations in the calculus below. Anyway the semantic justification of the rewrite rules may be of interest and facilitate understanding of the calculus.
Update of information in [AL0204L7] .
The thesis `Complexity Doctrines', was defended June 9. The June 13 corrected version is now linked to.
The full version of this information is available.
The following four papers are now availabile via anonymous ftp from colonsay.dcs.ed.ac.uk, in the subdirectory pub/sad -- thus via the WWW from the ftp directory .
The Oz Programming Model (OPM) is a concurrent programming model subsuming higher-order functional and object-oriented programming as facets of a general model. This is particularly interesting for concurrent object-oriented programming, for which no comprehensive formal model existed until now. The model can be extended so that it can express encapsulated problem solvers generalizing the problem solving capabilities of constraint logic programming. OPM has been developed together with a concomitant programming language Oz, which is designed for applications that require complex symbolic computations, organization into multiple agents, and soft real-time control. An efficient, robust, and interactive implementation of Oz is freely available.
The paper will appear in: Current Trends in Computer Science, Jan van Leeuwen, editor, Lecture Notes in Computer Science, Volume 1000, Springer-Verlag, Berlin, 1995.
The paper is available by anonymous ftp .
The full version of this information is available.
This book was due to be published on August 18.
Interest in formal methods continues to grow; unfortunately myths and misconceptions regarding their benefits and application continue to grow also. Applications of Formal Methods is a collection of articles by internationally renowned contributors from both academia and industry which will dispel many of these myths.
Each of these essays illustrates the application of formal methods to realistic problems, each with an industrial relevance, in various application domains, describing how they can be scaled to large-scale problems, and providing an evaluation of methods, tools, and validation and verification techniques.
Key features include:
The paper Interaction Combinators is available by anonymous ftp.
The paper shows that a very simple system of interaction combinators, with only 3 symbols and 6 rules, is a universal model of parallel computation. This paper is the continuation of the author's work on interaction nets, inspired by Girard's proof nets for linear logic, but no preliminary knowledge of these topics is required for its reading.
This paper is available .
Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanised using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is K*K=K, where K is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, Equivalents of the Axiom of Choice. The definitions used in the proofs are largely faithful in style to the original mathematics.
The full version of this announcement is available.
Cogito is the generic name of the methods and tools focus of the Software Verification Research Centre (SVRC). It encompasses and integrates the results of numerous methods, tools and reasoning projects carried out within the SVRC. The first iteration of integrated methods and tools is Cogito 1: it includes the specification language `Sum', a Repository Manger, a theorem prover `Ergo', several analysis and translation tools and supporting documentation and educational material.
The specification language Sum is Z-based, extended to facilitate refinement to code. It is therefore a key component of the Cogito development methodology. Sum extends Z with modules, syntactically distinguishes state and operation schemas, explicitly states operation preconditions, and partially merges terms and formulae by including boolean as a toolkit type. Sum has both an ascii and a graphical syntax, and a pretty printer is available for the graphical version which includes mathematical notation.
Cogito 1 currently has the following `products':
Cogito 1.0 system and associated (selected) documentation can be retrieved by anonymous ftp .
This message is to announce the availability of the programming language Lygon. Lygon is a logic programming language based on linear logic, and hence is a generalisation of (pure) Prolog. Due to the resource-oriented nature of linear logic, Lygon can be used to provide simple and elegant solutions for graph manipulations, bin packing problems, counting programs, and programs which requiring reasoning about state.
Lygon can be executed on a variety of architectures, and the implementation includes a variety of facilities to support debugging. Lygon is freely available, and feedback on any aspect of the language is most welcome.
More information (including how to obtain the system) may be found on the Lygon WWW page .
This May Be Of Interest To Some Users: I Have An Implementation Of Isabelle 94 In Linux Using New Jersey Ml 1.07. It Seems To Work Well.
This is the announcement for the release of the Coq Proof Assistant, Version 5.10.
It may be taken as usual from anonymous ftp .
For users who are already using one of the beta-test versions of V5.10, this final release has improved documentation, streamlining of tactics (Some adaptation of your scripts may be necessary because the names of inversion tactics have changed), and compressed theory files (.vo) which keep the size of the installation much smaller and are uniform across architectures. This substantial improvement necessitates however the installation of the latest release of Caml Light; see Warning below.
For users who are still using our old release V5.8, it is high time to switch to this new system, which has been completely rebuilt, authorizes mutually recursive inductive families, compiled theory modules, extensible parsers and pretty-printers, user-programmable tactics, synthesis of implicit type arguments, and many other goodies. The distribution also includes numerous new user-contributed libraries.
The current release works under most modern UNIX platforms. A specialised interface with the Centaur environment, called CTCoq, is under completion in Sophia-Antipolis and should be available soon in beta-test.
A Macintosh version will be available next Fall.
Warning: In order to install Coq V5.10 you need to install the latest release of Caml Light 0.7, available by anonymous ftp . You also need to install the Caml Light contribution `libunix'.
As always, anomaly reports to coq@pauillac.inria.fr and general questions to coq-club@pauillac.inria.fr
We apologize for possible multiple copies of this message.
I have the pleasure to announce that the new release of the list of problems in finite model theory is now available by anonymous ftp or by WWW .
New problems, solutions and other updates to it are always welcome.
I would like to welcome those of you, who haven't done it yet, to join our finite model theory mailing list. It can be achieved by sending an empty letter with Subject: subscribe to
finite-model-theory-request@informatik.rwth-aachen.deIn case of problems please send the request directly to me:
jurek@mephisto.informatik.rwth-aachen.de
On request I can send the list of present subscribers and a technical information about our (quite unusual) listprocessor.
I apologize if you have got this mail in several copies due to cross-posting.
Jurek Tyszkiewcz, RWTH Aachen
The book
Tommy R. Jensen and Bjarne Toft:was published in December 1994 in the United States and Canada, and it is now available also in Europe. The list price of the book is 44.95 US$, but most booksellers in the United States charge only 39.95 US$ for it.
GRAPH COLORING PROBLEMS
Wiley Interscience 1995
ISBN 0-471-02865-7
The book describes some 200 unsolved graph colouring problems with discussions of history, related problems and results and pertinent literature. The material is divided into 17 selfcontained chapters: Introduction to graph coloring, Planar graphs, Graphs on higher surfaces, Degrees, Critical graphs, The conjectures of Hadwiger and Hajos, Sparse graphs, Perfect graphs, Geometric and combinatorial graphs, Algorithms, Constructions, Edge colorings, Orientations and flows, Chromatic polynomials, Hypergraphs, Infinite chromatic graphs, Miscellaneous problems.
We are most interested in information/ corrections/ comments/ problems/ solutions related to the topics treated in the book. For this purpose the e-mail address graphcol@imada.ou.dk may be used. We shall make contributions available to the graph theory community via World Wid Web. The home page of the book can be obtained.
Bjarne Toft
Mathematics and Computer Science
Odense University
I have the following question : can the adjunction between topological spaces and locales be lifted to an adjunction between Generalised Spaces and Grothendieck toposes. I.e. we are looking for
locales:spaces = Groth. toposes:? (*)
Clearly, for any Grothendieck topos E the category of points of E is an accessible category. But if A is an accesible category then the accessible functors to Set are the preshaeves over A_pres the category of presentable objects of A (surely one has to fix a cardina, say alpha_0). So things don't work so easily.
I mean there is already a problem that (*) does not specify the ? (generalised spaces) uniquely.
So my question is whether there is a notion of accessible category + some further conditions which is an appropriate fill-in for ? in (*).
Maybe the answer is well-known but I simply couldn't find it easily in the literature.
Thomas Streicher
Update of information in [AL0205S4] .
Information about Computer Aided Design and Test is now available .
We would like to announce a web page collecting our recent papers on a theory of objects.
Object calculi are formalisms at the same level of abstraction as lambda calculi, but based exclusively on objects rather than functions. Unlike lambda calculi, object calculi are designed specifically for clarifying features of object-oriented languages. There is a wide spectrum of relevant object calculi, just as there is a wide spectrum of lambda calculi. We investigate untyped, simply-typed, and polymorphic calculi, with both functional and imperative semantics.
This home page is all about the theory of parameterized computational complexity developed by Downey and Fellows -- what it is, who works on it, what's been written on it, and whatever else we can think of that is relevant and we can throw in. Drop by and visit .
R.G. Downey and M.R. Fellows (1992) ``Fixed-Parameter Intractability (Extended Abstract)''. In Proceedings of the Seventh Annual Conference on Structure in Complexity Theory, IEEE Press, Los Alamitos, CA. 36-49.
Baltzer Science Publishers are pleased to announce the creation of our new Homepage site on the World Wide Web.
The homepage provides full details of all our journals together with ordering information, author instructions and a copy of the Baltzer Style File for use by authors. There are also links to other useful sites.
<location> := http://www.cs.utwente.nl/data/amast/
<location> := ftp://ftp.cs.utwente.nl/pub/doc/amast/
Date: 31/08/1995
Contents: Index.html, README, amast96/, workshops/, info/, links/,
sigala/, amast95/, amast93/, amast91/
CallForPapers.txt
CallForPapers.tex, CallForPapers.dvi, CallForPapers.ps
ADY02N11 [26/07/1995--07/08/1995]
CAADY02 [01/01/1995--07/08/1995]
full/
[M1] Anton Nijholt <anijholt@cs.utwente.nl>
[M2] David L. Parnas <parnas@triose.crl.mcmaster.ca>
[M3] Andrea Corradini <segragra@di.unipi.it>
[M4] Ugo Montanari <ugo@di.unipi.it>
[M5] Rowena Hart <rowena@softwords.bc.ca>
[M5] Jihad Jaam <gil@lim.univ-mrs.fr>
[M7] Bernard Courtois <Bernard.Courtois@imag.fr>
[M8] Ming Li <mli@math.uwaterloo.ca>
[M9] Falko Bause <bause@yvonne.informatik.uni-dortmund.de>
[MA] Richard Gerber <rich@cs.umd.edu>
[MB] Jan Heering <Jan.Heering@cwi.nl>
[MC] Phil Windley <windley@cs.byu.edu>
[MD] Jose D. P. Rolim <rolim@cui.unige.ch>
[ME] Ana Rosa Cavalli <Ana.Cavalli@hugo.int-evry.fr>
[MF] Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
[MG] Jiri Wiedermann <wieder@uivt.cas.cz>
[MH] Simon Peyton-Jones <simonpj@dcs.gla.ac.uk>
[MI] Harry Rudin <hr@zurich.ibm.com>
[C1] AMAST'96 Organization <amast96-info@informatik.uni-muenchen.de>
[C2] Dan Ionescu <ionescu@trix.genie.uottawa.ca>
[C3] Roberto Gorrieri <gorrieri@cs.unibo.it>
[C4] CMAA'96 Organization <cmaa@math.vanderbilt.edu>
[C5] Helene Kirchner <Helene.Kirchner@loria.fr>
[C6] Margje Punt <margje@cs.ruu.nl>
[C7] Jose A. Manas <pepe@dit.upm.es>
[C8] Rolf Wanka <icalp96@uni-paderborn.de>
[C9] Stephan Kepser <kepser@cis.uni-muenchen.de>
[CA] Peter Schroeder-Heister <psh@hume.informatik.uni-tuebingen.de>
[CB] ugo tab <tab96@dsi.unimi.it>
[CC] Richard Muise <rmuise@dragon.acadiau.ca>
[CD] Lesley Semmens <L.Semmens@lmu.ac.uk>
[CE] Robert Harper <Robert_Harper@terrier.fox.cs.cmu.edu>
[CF] James Harland <jah@cs.rmit.edu.au>
[CG] Vladimiro Sassone <vladi@daimi.aau.dk>
[CG] Bengt Nordstrom <bengt@cs.chalmers.se>
[J1] Abbas Edalat <ae@doc.ic.ac.uk>
[J2] Cris Calude <cristian@cs.auckland.ac.nz>
[J3] Gerard Holzmann <gerard@research.att.com>
[J4] --- <bixby@pivot.cam.rice.edu>
[J5] Bengt Jonsson <bengt@elaine.docs.uu.se>
[J6] Matthew Hennessy <matthewh@cogs.susx.ac.uk>
[J7] Indiana U. CS Faculty Search <search@cs.indiana.edu>
[J8] Roy L. Crole <rlc3@mcs.le.ac.uk>
[J9] --- <anthony@vax.lse.ac.uk>
[JA] Jiming Liu <jiming@kingfish.att.com>
[JB] Jiming Liu (see [JA])
[JC] Dominique Mery <Dominique.Mery@loria.fr>
[JD] Jose Manuel E. Valenca <jmv@di.uminho.pt>
[L1] Tobias Nipkow <tobias.nipkow@informatik.tu-muenchen.de>
[L2] Uffe Engberg <engberg@daimi.aau.dk>
[L3] Luc Longpre <longpre@cs.utep.edu>
[L4] Yves Lafont <lafont@lmd.univ-mrs.fr>
[L5] Stefano Guerrini <guerrini@di.unipi.it>
[L6] Maurice Herlihy <mph@cs.brown.edu>
[L7] Thomas Streicher <streicher@mathematik.th-darmstadt.de>
[L8] James Otto <otto@triples.math.mcgill.ca>
[L9] Davide Sangiorgi <davide@duick.cma.fr>
[LA] Gert Smolka <smolka@dfki.uni-sb.de>
[LB] Edmund Kazmierczak <eka@cs.uq.oz.au>
[LC] Yves Lafont (see [L4])
[LD] Lawrence C Paulson (see [MF])
[T1] Edmund Kazmierczak (see [LB])
[T2] James Harland (see [CF])
[T3] Jose Manuel E. Valenca (see [JD])
[T4] Coq Team <coq@pauillac.inria.fr>
[P1] Jerzy Tyszkiewicz <jurek@mephisto.informatik.rwth-aachen.de>
[P2] Bjarne Toft <btoft@imada.ou.dk>
[P3] Thomas Streicher (see [L7])
[S1] Jan Rossmann <rossmann@ti.uni-trier.de>
[S2] Luca Cardelli <luca@src.dec.com>
[S3] Todd Wareham <harold@csr.uvic.ca>
[S4] Baltzer Science Publishers <publish@baltzer.nl>
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/i06/AL0206<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 .