Comments are welcome!
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _
date: 10 February 1995
e-mail to: amast@cs.utwente.nl
________________________
e-mailed to: 340 subscribers
Helena Rasiowa, descendant and member of the Polish School of Logic, died on 9 August, 1994. Born on 20 June 1917, she begun the studies of mathematics at the University of Warsaw in 1938. During the second world war she continued the studies at the Underground University. She wrote her Master's thesis under the supervision of Jan Lukasiewicz and obtained her M.Sc. degree in 1945. She received her Ph.D. degree under the supervision of Andrzej Mostowski in 1950. She held academic positions at the University of Warsaw from 1945 till 1992. She served as the Head of the Chair of Foundations of Mathematics (1964-1970) and the Head of the Chair of Mathematical Logic (1970-1992).
The study of the relationship between logic and algebra, originated by work of Boole and continued by Lindenbaum, Tarski, Stone, McKinsey, Mostowski, Henkin, was the main research subject of Helena Rasiowa. Two very important developments in the algebraic study of logic were the introduction by Lindenbaum and Tarski of the method of treating equivalence classes of formulas as elements of an abstract algebraic system, and the treatment of formulas as algebraic functions in certain algebras originated by Lukasiewicz and Post with their generalization of truth tables. Algebraic methods in investigations of intuitionistic and modal logics were originated by Stone, Tarski and McKinsey. Helena Rasiowa became very active in these areas in early fifties. Jointly with Roman Sikorski, she presented the first algebraic proof of Gödel's completeness theorem for classical predicate logic. Next, she proved the analogous theorems for intuitionistic and modal logics algebraically. Since then many logicians have employed algebraic methods in investigations of logical calculi. Her first monograph `The Mathematics of Metamathemathics' (Polish Science Publishers, Warsaw 1963), joint with Roman Sikorski, contains a comprehensive survey of algebraic theories of logical calculi. The algebraization is presented of classical, intuitionistic, modal and positive logics. The book concentrates on metalogical theorems concerning predicate calculi of these logics and on investigation of elementary theories based on these logics. In the next monograph `Algebraic Approach to Non-Classical Logics' (Studies in Logic and the Foundations of Mathematics, vol. 78, North Holland, Amsterdam 1974), Helena Rasiowa developed a general theory of algebraization of logical systems. Within the framework of this theory she presented algebraizations of a number of non-classical logics: classical and positive implicative logics, logics weaker than positive implicative logic, minimal logic, positive logic with semi-negation, constructive logic with strong negation, and multiple-valued Post logics.
From the early seventies on, Helena Rasiowa became interested in foundational problems in computation theory. She recognised that theoretical computer science has represented an important source of inspiration in development of logic. She initiated research on logics of programs; algorithmic logic and its theory was developed under her supervision. She was working on a theory of approximate reasoning and developed various AI-oriented logical systems for modeling cognitive processes.
She was active in her work till the last days, during the past two years she was working on a new monograph: `Algebraic Analysis of Non-Classical First Order Logics'.
Helena Rasiowa was the founder and the editor-in-chief of Fundamenta Informaticae, collecting editor of Studia Logica, and associate editor of the Journal of Approximate Reasoning. She received numerous honors and awards, including Sierpinski medal, the title of Honorary Member of the Polish Mathematical Society, the Stefan Mazurkiewicz Award of the Polish Mathematical Society, and the First Class State Science Award in Mathematics. She served as President of the Warsaw Division of The Polish Mathematical Society and as Assessor of the Division of Logic, Methodology, and Philosophy of Science of the International Union of History and Philosophy of Science. She served the Association for Symbolic Logic as a member of the Council. She was the Head of the Council of the Polish Association of Logic and Philosophy of Science.
Helena Rasiowa exerted a great influence on many logicians around the world, her death is a great loss for the logic community.
Ewa Orlowska.
Update of [AL0101C1] .
The list of accepted papers is available.
The full program will be announced in the first week of March.
Update of [SIAN05p2-1] .
Held in conjunction with POPL'95. Registration information .
SIPL'95 Advance Program
Update of [AL0103C1] : deadline extension
In view of its joint organization with the French Project `Modeles et Preuves', this AMAST workshop will feature a limited number of selected contributions -- in addition to the invited papers.
As an attempt to allow prospective authors to contribute their most recent work, the submission and selection deadlines are extended as follows:
submission: 5 March 95; notification: 5 April 95; final: 27 May 95
Update of [AL0101C3] .
The full version of the Final Call for Papers is available.
The purpose of CONCUR'95 is to bring together researchers, developers and students in order to advance the science of concurrency theory and promote its application. Submissions are invited in all areas of semantics, logics, and verification techniques for concurrent systems. Potential topics include, but are not limited to, process algebras, Petri nets, true concurrency, shared-memory and message-passing formalisms, operational and denotational models, programming language semantics, probabilistic and real-time processes, hybrid systems, concurrent logic and constraint programming, fairness, temporal logics, compositional analysis techniques, and verification tools. Submissions will be evaluated by the Program Committee for inclusion in the proceedings, which will be published by Springer-Verlag. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. CONCUR '95 will feature electronic submission of papers. E-mail postscript (tm) or uuencoded dvi files to: concur95-submit@cs.sunysb.edu .
When electronic submission is not possible (e.g. due to lack of internet access), five (5) hardcopies of the paper should be sent to:
CONCUR '95, Attn: Scott Smolka, Dept. of Computer Science
SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA
telephone: +1 516 632 8453, fax: +1 516 632 8334.
Submissions should contain a full paper of no more than 15 typed pages (11pt or 12pt, single-spacing, single-column, fullpage or a4 margins) accompanied by a one-page abstract. Mailing address (both postal and electronic), phone/fax number (if available) of the author to whom correspondence should be sent should be clearly indicated.
Dates: subm: 1 March 1995; notif: 1 May 1995; final: 1 June 1995.
The latest CONCUR'95 information may be obtained electronically via
Update of information in [AL0102M1] .
The new information in this announcement relates to the proceedings.
For other information, see the preliminary announcement.
The Workshop on Logic, Domains, and Programming Languages is aimed at computer scientists and mathematicians alike, who share an active interest in the mathematical foundations of computer science. The scope of the workshop encompasses all aspects of Programming Language Semantics ranging from purely theoretical topics to concrete applications and implementations of semantic methods. Possible workshop topics are, for example, Lambda Calculi and Functional Programming, Domain Theory, Denotational and Algebraic Semantics, Type Theories, Linear Logic, Process Algebras, and Concurrency.
Proceedings: will be published as a special issue of the journal Mathematical Structures in Computer Science. All participants may submit papers after the workshop will have taken place. Papers will be reviewed according to the usual journal standards. The deadline of submission will be fixed at the meeting.
Registration There will be no fee; participants will only be asked for a contribution to cover expenses for coffee breaks, reception, etc.
You are cordially invited to pre-register for this workshop. In that case, or for further information, please send all correspondence to ldpl95@mathematik.th-darmstadt.de (preferred) or to Dr. Michael Huth at
Workshop on Logic, Domains, and Programming Languages
AG 1 FB Mathematik, Technische Hochschule Darmstadt
D-64289 Darmstadt, Germany
Update of [AL0103C2] .
The full version of this Call for Papers is available.
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; concurrency control and synchronization; fault tolerance specification, semantics and verification and cryptography and security.
The conference will consist of two tracks of presentations.
Long presentations will be given slots of approximately 25 minutes and will be accompanied by papers of up to 10 pages in the proceedings.
Brief announcements will be given slots of approximately 10 minutes and will be accompanied by 1-page abstracts in the proceedings. This track is intended as a forum for reporting research at an early stage, unpolished recent results, and brief communications.
Submissions: For the long presentation track, please submit an extended abstract that provides sufficient detail to allow the program committee to assess the merits of the paper. It is recommended that each submission begin with a succinct statement of the problem, a summary of the main results, and a brief explanation of their significance, all suitable for a non-specialist. Submitted abstracts should be no longer than 4,500 words. Submissions for the brief announcement track should be a one-page abstract, including a statement of the problem, the results and their implications. Detailed submission information is given in the full version of this announcement and prospective authors should read these carefully.
Dates subm: Feb 10, 1995; notif: Apr 14, 1995; final: May 20, 1995.
Requests for information can be directed to the program chair:
Vassos Hadzilacos, Computer Systems Research Institute
Univ. Toronto, 6 King's College Rd Toronto, Ontario Canada M5S 1A1
e-mail: vassos@cs.utoronto.ca
Update of information in [AL0103C8] .
Due to clashes with other meetings, the workshop on termination previously scheduled for April will take place from May 29 to May 31.
A similar workshop on termination was organised in May 1993 at St. Andrews where around forty researchers in the field met for the first time. We are organising a second workshop which will take place in the La Bresse mountain resort, in les Vosges. We hope this congenial location will offer a friendly environment as at St. Andrews and will create the same fruitful exchanges. A bus trip will be organised with a visit to a picturesque Alsatian town followed by a dinner.
A non exhaustive list of topics that could be presented is: well-quasi orders, Kruskal's theorem; recursive path order, lexicographic path order & multiset path order; length of derivation and orders, order hierarchies; ordinals and termination; proofs by interpretation; study of hard termination problems; design and implementation of new algorithms; integration in theorem provers and experiments; applications of termination.
People who wish to present a communication are invited to submit a one page abstract by February 20th 1995, by e-mail to
termination@loria.fr
Dates:
- February 20
- deadline for submission of communications
- March 20
- announcement of the programme
- May 2
- deadline for registrations
Organizing Committee:
Francoise Bellegarde (U. de Franche-Comte, Besangon, France)
Adam Cichon (U. Henry Poincari, Nancy, France)
Isabelle Gnaedig (INRIA-Lorraine. Nancy, France)
Pierre Lescanne (CRIN-CNRS, Nancy, France)
Ursula Martin (U. St Andrews, Scotland)
The Full Call for Papers is available via the WWW page.
Topics. The scope of the workshop includes higher-order aspects of
Submission. Extended abstracts (up to 4 pages) of papers to be submitted should be sent to the programme committee chairman. Submission by email is preferred. Otherwise send 3 copies.
Submission deadline: May 1, 1995.
Programme committee chairman:
Bernhard Möller, Institut für Mathematik, Universität Augsburg
D-86135 Augsburg, Germany.
Fax +49 821 598 2274, Email: moeller@uni-augsburg.de
Programme committee:
Gilles Dowek, Mike Gordon, Jan Heering, Karl Meinke, Tobias Nipkow.
The Proceedings of HOA'93 are available in LNCS Vol. 816.
The full version of this Call for Papers is available.
The symposium is intended to provide a forum for researchers working in algorithms and the theory of computation. Papers presenting original research in the areas of design and analysis of algorithms, computational complexity, and theory of computation are sought.
Topics. Typical, but not exclusive, topics of interest include: Automata, languages and computability; Algorithms (combinatorial/graph/ geometric/randomized); VLSI and parallel algorithms; Networks and distributed algorithms; Theory of learning and robotics; Number theory and cryptography; Graph Drawing; Computational Logic.
Submissions. Authors are requested to submit 15 copies (in English) of an extended abstract by 12 May 1995 to:
Professor John Staples,
Department of Computer Science, University of Queensland
Queensland 4072, Australia.
The extended abstract should include the email address of the contact person and be printed on at most five double-spaced double-sided pages.
Dates: subm: 12 May 95, notif: 31 July 95, final: 4 Sept. 95
For information please contact:
Dr. Bob Cohen
Department of Computer Science, University of Newcastle
Callaghan, NSW 2308, Australia
Phone: +61 049 21 5291, Fax: +61 049 21 6929
E-Mail: isaac95@cs.newcastle.edu.au
The full version of this Call for Papers is available.
The direct execution of logical statements, through languages such as Prolog, has been influential in both Computer Science and Artificial Intelligence. Executable forms of temporal logics have been proposed in order to provide system developers with access to more appropriate logical techniques. A wide range of executable languages have appeared to fill this need, exhibiting a number of characteristics and execution mechanisms. Therefore, these languages have a wide range of application areas, including temporal databases, temporal planning, animation of temporal specifications, hardware simulation, and distributed AI.
Topics of interest include, but are not limited to: theoretical issues in executable temporal logics; design of executable temporal logics; relationship between execution and temporal theorem- proving; operational models and implementation techniques; programming support and environments; comparative studies of languages; relationship of executable temporal logics to (temporal) databases; applications and case studies.
Submissions should include: author's name(s), affiliation, complete mailing address, phone and fax number, e-mail address and an abstract of max. 300 words. Electronic submission is strongly encouraged (either as self-contained LaTeX, or postscript) and this, or five copies of submitted papers should be sent, by March 1st 1995, to:
Michael Fisher, Department of Computing Manchester
Metropolitan University, Chester Street, Manchester M1 5GD, UK
Email: M.Fisher@doc.mmu.ac.uk
Telephone: + 44 61 247 1488. Fax: + 44 61 247 1483
Dates: subm: Mar. 1, 95; notif: Apr. 1, 95; revised: May 1, 95.
Information about the workshop, together with abstracts of accepted papers, will be available via the WWW page .
If you are interested in attending this workshop please refer to the full version of this announcement referred to above.
Deadline Reminder: 10 February 1995 is the submission deadline for this workshop. See [SIAN03p2-3] for the Call for Papers.
The full version of this Call for Papers is available.
This symposium is a forum for researchers, practitioners, developers and users working on all aspects of graph drawing. The aim is to present recent research results, to demonstrate systems for graph drawing and to explore directions for future research and new applications. It is anticipated that the symposium will further collaborative efforts between computer scientists, mathematicians, and applied researchers.
Scope Graph drawing addresses the problem of visualizing structural information. More specifically it is concerned with the construction of geometric representations of abstract graphs and networks. The automatic generation of drawings of graphs has important applications in key computer science technologies such as database design, software engineering, VLSI and network design and visual interfaces and also in engineering, chemistry and biology. The range of issues being investigated in graph drawing includes algorithms, graph theory, order theory, graphic languages, applications and practical systems.
Papers and demonstrations are being sought. For a full list of topics for both papers and demos see the full version of this announcement or refer to the WWW page below.
Submission of papers and demos: The program committee invites submissions of papers (6 - 12 page extended abstract) and demos (2 - 6 page abstract, descriptive screen dumps, and a list of hardware needed). Submissions by email (in LaTeX, postscript or plain text) or hard copy (10 copies) should be sent to the program committee chairman:
Prof. Dr. Franz J. Brandenburg, Lehrstuhl für Informatik
Universität Passau, 94030 Passau, Germany.
E-mail: gd95@informatik.uni-passau.de
Dates: subm: June 1, 95; notif: July 15, 95; final: at the workshop
Further information: contact the chairman at the email address above, or have a go through the WWW .
ISCIS X is the tenth of a series of meetings which have brought together computer scientists and engineers from many countries. This year Computer Networks and Image Processing will be special topics of the conference. The conference will be held in a resort hotel near the ancient city of Ephesus, on the Agean coast of Turkey.
Organizing Committee: A. Emre Harmanci (ITU), Erol Gelenbe (Duke Uni.), Bulent Orencik (ITU), Fusun Tunali (ITU), Muhittin Gokmen (ITU)
Topics of interest: Computer Networks, Parallel Processing and Parallel Algorithms, Image Processing, Pattern Recognition, Artificial Intelligence, Programming Languages, Computer Graphics, Databases and Information Retrieval, Neural Networks, Performance Evaluation, Software Engineering, Distributed Systems, Computer Architecture, Theoretical Computer Science, Real Time Computing, Computer Vision.
Submission: Please submit four copies of the full paper in English, limited to eight pages, by May 1, 1995 to:
ISCIS X - Department of Control and Computer Engineering
Electrical and Electronics Faculty, Istanbul Technical University,
Ayazaga 80626, Istanbul, Turkey
E-mail: iscisx@tritu.bitnet or iscisx@cc.itu.edu.tr
Tel: +90 (212) 285 64 20 or 285 35 90, Fax: +90 212 285 36 79
Paper Format: on A4 or letter size paper, single space, 12 point font, single column, one inch margins on all four sides. The first page should have a two inch margin at the top. Centered at the top of the first page should be the complete title of the paper, author(s), affiliation(s), mailing and e-mail address(es), then the abstract, not exceeding 15 lines, followed by the text. In an accompanying letter, the following should be included: full title of the paper, author name(s), mailing address(es), telephone and fax numbers and e-mail address(es) of the author(s) indicating the presenter and technical session names (1st and 2nd choices) to be selected from the list of topics given above.
Dates: subm: May 1, 95; notif: Jul. 3, 95; final: Aug. 21, 95.
The 2nd Workshop (NSL'95) will be held in Irkutsk (near Lake Baikal), Russia, June 15 - 17, 1995. This is organized as an activity of the joint project on the study of non-standard logics between logicians in Japan and Siberia. The Workshop will be amalgamated with the Conference on Applied Logic. NSL'94 was held at Kanazawa, Japan, Dec. 5-8, 1994.
Organizing Committee:
H. Ono (JAIST), Yu. Ershov (Novosibirsk) (co-chair),
S. Goncharov (Novosibirsk), Y. Komori (Shizuoka),
L. Maksimova (Novosibirsk), A. Mantsyvoda (Irkutsk),
M. Sato (Tohoku), V. Rybakov (Krasnoyarsk),
M. Takahashi (Tokyo Institute of Technology), Y. Toyama (JAIST).
Scope:
Contributed Papers are invited from any research topic related to non-standard logics and logical aspects of computer science. Deadline of submitting abstracts is April 5, 1995. Abstracts written in English, in LateX-form, not more than one page long, should be sent to
Larisa Maksimova
Institute of Mathematics, Siberian Branch of Russian Acad. of Sci.
630090 Novosibirsk, Russia
Fax: +7 3832 35 78 08; Email: lmaksi@math.nsk.su
Information on registration:
Nikolai Peryazev, Irkutsk Univ, K.Marx str. 1, 664003 Irkutsk Russia
Tel: +7 3952 332178 Fax: +7 3952 332204 Email: applog@uni.irkutsk.su
This workshop is organized as a satellite activity of the TAPSOFT'95 conference, May 22-26, University of Aarhus. The meeting starts Friday, May 26th at 2:00 p.m., and ends May 27th at 12:00 noon.
Recent years have shown the advent of various analysis techniques based on logical inference systems, in particular variations of type systems. Proponents of the method claim that the analyses are easier to specify, achieve a cleaner separation between specification and implementation, and that it is easier to formulate fragments with a tractable efficiency.
Topics include: specification of specific analyses for programming languages; the role of effects, polymorphism, conjunction/disjunction types, dependent types etc. in specification of analyses; algorithmic tools and methods for solving general classes of type-based analyses; the role of unification, semi-unification etc. in implementations of analyses; proof techniques for establishing the safety of analyses; relationship to other approaches to program analysis, including abstract interpretation and constraint-based methods; exploitation of analysis results in program optimization and implementation.
Submissions: extended abstract, not exceeding ten pages (excluding references and appendices). Remember to incorporate an abstract, your address, e-mail address, and phone and fax numbers on the front page. The final version will be allowed 15 pages. Electronic submission is encouraged via e-mail to LOMAPSworkshop@daimi.aau.dk (either Postscript or self-contained TeX or LaTeX file). Alternatively, submissions may be sent by ordinary mail (six copies required) to:
Hanne Riis Nielson, Computer Science Department, Aarhus University
Bldg. 540, Ny Munkegade, DK-8000 Aarhus C, Denmark.
Dates: subm: Mar. 1, 95; notif: Apr. 10, 95, final: May 1, 95.
"Proceedings" will be published as a technical report from Aarhus University; this does not prevent papers to be submitted elsewhere (but we don't want to accept papers already accepted elsewhere).
Organization Committee: Hanne Riis Nielson, Kirsten Lackner Solberg
Programme Committee: Flemming Nielson, David Wright, Daniel Le Metayer, Fritz Henglein
The full version of this Call for Papers is available.
The previous workshops (DEON'91, Amsterdam, and DEON'94, Oslo) have brought together people working on various aspects of deontic logic and closely related areas of investigation, and their applications in computer science and public and private administration. With DEON'96 we propose to broaden the emphasis slightly, to encourage --even more than in the past-- contributions on the logic of action and its applications, and to encourage participation by linguists. The workshop is open to all those interested, subject to availability of places.
Scientific Contents The Program Committee seeks papers concerning:
Detailed lists of related areas are in the full version of this Call.
Submission Five hard copies, double-spaced, max. 20 pages, to be sent to one of the two co-chairs of the Program Committee. Electronic submissions not accepted. Submissions will be judged on significance, originality, quality and clarity. Reviewing will be blind to the identities of the authors. See the full version of this Call for detailed submission requirements and for full address information.
Dates subm: May 15, 1995; notif: July 15, 1995; final: Oct. 1, 1995
Publication Proceedings available at the workshop. We hope that, as in the case of the previous workshops, selected papers will also appear in a major international journal or by a major international publisher.
Program Committee CoChairs:
Jose Carmo (Dep't Mathematics, IST Lisboa; e-mail: jcc@inesc.pt)
Mark Brown (Dep't Philosophy, U. Syracuse; mabrown@mailbox.syr.edu)
Chair of the Organizing Committee: Jose Fiadeiro (Portugal)
Invited Speakers:
The full version of this announcement is available.
The Editors (listed in the full announcement) invite submission of articles for publication in the first volume (1995) of the journal. The Editorial Policy of the journal and some information for authors follow. Some information about subscribing is in the full announcement. More details are available from the journal's WWW server or by anonymous ftp .
Editorial Policy
The journal Theory and Applications of Categories will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.
Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.
The method of distribution of the journal is via the Internet tools WWW/gopher/ftp. The journal is archived electronically and in printed paper format.
Information for Authors
The typesetting language of the journal is TeX, and LaTeX is the preferred flavour. TeX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. Please obtain detailed information on submission format and style files by WWW or anonymous ftp from the sites listed above. You may also write to tac@mta.ca to receive details by e-mail.
The Department of Computer and Information Science invites applications for at least one tenure track faculty position. Candidates from all areas of Computer Science will be considered; however, we are particularly interested in the areas of programming languages, computational science, and software systems. Candidates should have a Ph.D. in computer science and a strong commitment to both research and teaching. We offer an excellent research environment. The department has major research strengths and funding in the areas of human/machine interfaces, parallel programming languages and environments, software engineering, computational science, distributed operating systems, electronic media, graphics, declarative languages, and the theory of computation. The department is associated with the NSF-funded Software Engineering Research Center (SERC) and the Computational Intelligence Research Laboratory (CIRL). Instructional laboratories consist of UNIX-based workstations and computer servers. Research facilities include special equipment for user-interface design, graphics, and parallel processing. A new computational science laboratory will house multiple parallel computers with high-performance graphics hardware.
The University of Oregon is located in Eugene, a community rated among the most livable in the USA. Qualified candidates should send their curriculum vitae and the names of at least four references to:
Faculty Search Committee, Computer and Information Science
University of Oregon, Eugene, OR, 97403-1202
or send email to:
faculty.search@cs.uoregon.edu
For full consideration, applications should be received by 3/1/95, but we will continue to accept applications until the position is filled. The University of Oregon is an Equal Opportunity/ Affirmative Action institution committed to cultural diversity and compliance with the Americans with Disabilities Act.
The Max-Planck-Institute for Computer Science is located on the campus of the Universität des Saarlandes in Saarbrücken, Germany. The institute was founded in 1990 and consists, at present, of two research units: Algorithms and Complexity, and Logic of Programming. Research groups for Distributed Systems and Computer Architecture will be added in 1995/96.
The research group Algorithms and Complexity offers postdoctoral fellowships. A fellowship is awarded for a one or a two year period and amounts to DM 36,000 per year, taxfree. Further information can be obtained from Michiel Smid (michiel@mpi-sb.mpg.de).
The main focus of the research group is data structures, graph and network algorithms, computational geometry, parallel algorithms, combinatorial optimization, randomized algorithms, and implementation of algorithms and program libraries. More information is available .
Applications (including curriculum vitae, list of publications, research plan, names of references with their e-mail addresses, and intended period of stay) should be sent by the end of February 1995 to Kurt Mehlhorn or Michiel Smid.
Max-Planck-Institut für Informatik
Im Stadtwald
D-66123 Saarbrücken
Germany
Computing and Information Sciences Department
Kansas State University
Manhattan, Kansas, USA
Applications are invited for one or more University Graduate Fellowships for PhD studies in Computer Science for August, 1994. The Fellowship pays approximately $12,000 per year and includes a waiver of the usual $6000 enrollment fee. Fellowships are awarded on a yearly basis.
Applicants whose research interests lie in formal aspects of programming languages and real-time systems are especially invited to apply. Research efforts in these areas are supported by the following faculty members: David Schmidt (denotational semantics), Allen Stoughton (denotational semantics), Brian Howard (type theory and logic), George Strecker (category theory), and Maria Zamfir-Bleyberg (semantics of concurrency), and Rodney Howell (real-time scheduling).
Qualified applicants will have an M.S. degree or its equivalent, a strong academic record, and a solid background in computing. The Fellowships are funded by the University's Graduate School, who requires that applicants must be U.S. citizens or permanent residents. International applicants are invited to inquire about Departmental Teaching and Research Assistantships, which possess approximately the same financial benefits as Graduate Fellowships.
The deadline for applications is February 15, 1995. Interested individuals can obtain applications materials at the WWW or they may contact David Schmidt (email: schmidt@cis.ksu.edu; phone: 1-913-532-6350) for information and applications materials.
Bogazici University
Istanbul, Turkey
Department of Computer Engineering
The Department of Computer Engineering Bogazici University invites applications for both visiting and tenure track assistant professorship positions especially in parallel systems and architectures, parallel algorithms, parallel and distributed databases, computer networks, and software engineering. However, applications in other areas of computer science and engineering will also be considered.
Applicants must demonstrate strong research and scholarship potential, as well as good teaching ability. Successful candidates are expected to pursue active research and to contribute significantly to the teaching programs of the department. The language of education is English.
All applications should include a resume with publication list and the names of at least three people who can comment on the applicant's professional qualifications, together with publications and transcript of records. Applications should be sent to:
Prof.Dr. Selahattin Kuru, Chairman
Department of Computer Engineering
Bogazici University
80815 Bebek-Istanbul
Turkey
E-mail: kuru@boun.edu.tr
Fax: + 90 (212) 265 84 88
Phone: + 90 (212) 263 15 40 Ext:1652-1323-1324
The Institut für Informatik of the Universität Hildesheim seeks a candidate for a C1 position (Scientific Assistant) starting April 1, 1995. The position is temporary for three years, with a possibility of extension for another three years. Candidates are required to know, or be willing to learn, the German language. They should be promoted in a subject closely related to Theoretical Computer Science. They are also assumed to be willing to assist in the regular computer science curriculum.
The possibility to write a Habilitation Thesis is offered. The Institut provides excellent research facilities. The group's active research interests include the verification and the semantics of parallel systems. The candidate's interests do not have to coincide with these topics; we are also looking to strengthen our group in the areas of complexity and parallel algorithms. Hildesheim is a small town of slightly more than 100 000 inhabitants providing a very good environment for accommodation and leisure. The C1 salary depends on personal circumstances.
Please apply or direct queries to Professor Eike Best, at
e.best@informatik.uni-hildesheim.de, or
FAX (+49) 5121 860 475, phone (+49) 5121 883 740.
Alternatively, please apply to the Kanzlerin (Vice Chancellor) of our University, at:
Universität Hildesheim, z.Hd. Die Kanzlerin,
Marienburger Platz 22, D-31141 Hildesheim, Germany
(FAX +49 5121 86156)
quoting "C1 Theoretische Informatik". The University strongly encourages applications from female candidates.
The full version of this announcement is available.
Applications are invited for a Postdoctoral Fellowship from persons who have completed or are about to complete a doctorate. The position is tenable immediately, and some preference will be given to candidates who can start at an early date.
The successful candidate will be based in the Artificial Intelligence Laboratory, Computer and Information Science, University of Otago, Dunedin, New Zealand. They will work in the project Developing a Computational Theory of Natural Language Understanding for use in Law.
The position will involve the design and implementation of a theory of natural language understanding based on the use of semantics of words. The theory is currently being developed and a program called LINGUIST has been written in CLOS for testing the theory. This is an exciting opportunity for someone to help shape a new theory of natural language understanding and apply what is developed in the area of law.
The ideal candidate should have a strong background in AI natural language research, well-developed programming skill in LISP and demonstrated competence in written English. However, candidates with lesser relevant experience are also invited to apply for this position.
The project is led by Dr W K Yeap to whom all queries regarding this position should be addressed. Other members working in this project include Professor P Sallis (Information Science), Professor R Sutton (NZ Law Commissioner), Ms Nicola Peart (Law Faculty).
The Fellowship is supported by a grant from the NZ Law Foundation and is tenable for a year. The project will be reviewed at the end of the year for a possible extension for another year. The emolument for each year will not exceed NZ$40,000 per annum.
Further information is obtainable by anonymous FTP . Enquiries can be made to
Dr W K Yeap, Computer and Information Science, University of Otago
PO Box 56, Dunedin (email: coscwky@otago.ac.nz)
or the Registrar, U. Otago, P O Box 56, Dunedin (Fax: +64 3 4741607).
Deadline passed, but further applications may be considered.
Applications are invited for a Postdoctoral Research Fellowship on an EPSRC funded project "Reasoning with Fairness" concerned with the study of processes under environmental constraints. Applicants should have a PhD in Computer Science or Mathematics and have knowledge of: process calculi, denotational semantics and/or process logics.
Informal enquiries to
Dr Marta Kwiatkowska
(tel +44 (0)121 414 7264; email M.Z.Kwiatkowska@cs.bham.ac.uk).
Starting salary on scale from 13,941 - 20,953 pounds a year for up to 15 months from as soon as possible.
Application forms (returnable by 1 February) and further particulars are available from (please quote the reference number S13619/95):
Mr P J F Scott, BA, MIPM
Director of Staffing Services
The University of Birmingham
Edgbaston, Birmingham B15 2TT, England
Tel: +44 (0)121 414 6483 (24 hours)
Fax: +44 (0)121 414 4802
The School of Computer Science is undergoing a programme of diversification and expansion. It is currently being developed in three areas: Theoretical Computer Science, Artificial Intelligence and Software Engineering. The School is in the process of appointing a Professor, who is likely to be in Theory or Software Engineering, with a further appointment in the other area to follow in the near future.
Further information is available .
We encourage applications from women and people from ethnic minorities or with a disability.
The University invites applications for a newly established Chair in Theoretical Computer Science, to be held within the Department of Computer Science. We seek a candidate who will further develop the strengths of the Department and its Laboratory for Foundations of Computer Science (LFCS).
In addition to outstanding strength in research and scholarship, the successful candidate should provide leadership and inspiration for fundamental research, encourage the integration of his/her own research with that of others, and play an active role in teaching and departmental administration.
The appointment is full-time, the salary will be within the normal professorial salary range and the person appointed will be required to retire at the end of the academic year in which he/she reaches the age of 65.
Letters of application should include a curriculum vitae, and the names and addresses of 3 referees. Please include fax numbers for referees if possible. Applications should be addressed to the Secretary to the University, University of Edinburgh, and sent, to arrive not later than 31st March 1995, by post (1 Roxburgh Street, Edinburgh, EH8 9TB, Scotland, UK), or fax +44 (0)131 650 6509. The taking up of references is selective and does not imply a decision that the applicant will be placed on the final short-list for interview.
Further particulars may be obtained from our WWW page or from the Head of Department:
Prof Roland N. Ibbett
Department of Computer Science
tel: +44 (0)131 650 5119
e-mail: hod@dcs.ed.ac.uk
The College of Computer Science invites applications for a tenure-track faculty position at all ranks especially in the areas of networks, distributed computing, information systems, high performance computing, software development, and graphics. Exceptionally qualified candidates in other areas will also be considered. Ph.D. in Computer Science or related field is required.
The College has a diverse full-time faculty of 19; 300 undergraduate, 150 Masters, and 40 Ph.D. students. The faculty has significant external support and is engaged in a broad range of successful research programs. Research seminars draw upon extensive computer science talent from the greater Boston area. The College maintains state-of-the-art equipment, including three parallel computer architectures (MasPar, CM-2, and transputer), a large network of SPARC and DEC workstations, and additional specialized laboratories: a virtual reality lab, a multi-media lab, and a Macintosh teaching lab.
Please send a resume, statement of research interests, and names of three references to:
Faculty Hiring Committee, College of Computer Science
161 Cullinane Hall, Northeastern University
Boston, Massachusetts 02115
Applications deadline is February 1, 1995. For further information, send e-mail to
hiring@ccs.neu.edu
Northeastern University is an Equal Opportunity/Affirmative Action Employer. We strongly encourage applications from women and minorities.
For more information on our research and faculty see on the WWW.
Applications are invited for a postdoctoral position in the Department of Computer Sciences for research in the area of models for parallel computation, and the design and analysis of parallel algorithms. The position is under Professor Vijaya Ramachandran and is funded by grants from the Texas Advanced Research Program and National Science Foundation.
Applicants must have a Ph.D. or equivalent in computer science or expect to receive one before starting on the postdoc position.
Applicants should submit a curriculum vita and representative publications, and should indicate the desired starting date for the postdoctoral position. Also, please arrange to have three letters of reference sent to:
Prof. Vijaya Ramachandran
Department of Computer Sciences
The University of Texas at Austin
Austin, Texas 78712--1188.
Applications and letters of reference may be sent by e-mail to vlr@cs.utexas.edu . However, please send hardcopies of representative publications; do not send latex or postscript files of publications.
The Network Design and Security Research Department at Bellcore currently has openings for two Research Director positions. One position is to head a group of researchers in security and cryptology research and the other position is to head a group of researchers in network design and optimization research. We are seeking outstanding candidates in these areas with a proven track record of research accomplishments, broad knowledge of the areas represented by the department activities, good managerial skills, and the ability to interface between the research area and the other business units.
The department currently consists of over thirty researchers working mainly in the following broad areas:
Work responsibilities include a broad range of activities from fundamental research to software prototyping to applied projects in support of the business units.
Send a vita with a statement of qualifications and four references to
Clyde Monma
Bellcore, Room 2L-387
445 South Street
Morristown, New Jersey 07960
Email: clyde@bellcore.com
Phone: (201) 829-4428
Fax: (201) 829-2645
Bellcore is an Equal Opportunity/Affirmative Action Employer. Women and minority applicants are encouraged to apply.
The full version of this announcement is available.
The Advanced Computing Research Centre (ACRC) is one of the University of South Australia's nine newly-endowed research centres. The ACRC encompasses three research groups based in the School of Computer and Information Science and is enjoying rapid growth in its research activity.
The Centre is seeking to appoint four postdoctoral candidates with excellent research potential to participate in the following projects.
Two ARC-funded projects within the Concurrent Systems Research Group:
Further information from:
Professor George Milne, Director, Advanced Computing Research Centre
phone: +61 8 302 3943; fax: +61 8 302 3988
e-mail: george.milne@unisa.edu.au
Two further posts are available in the following areas:
Dr. Millist Vincent, Advanced Computing Research Centre
phone: + 61 8 302 3166; fax: +61 8 302 3381
e-mail: millist.vincent@unisa.edu.au
Dr. Jim Warren, School of Computer and Information Science
phone +61 8 302 3446; fax: +61 8 302 3381
e-mail: James.Warren@unisa.edu.au
Annual salary AUS$36,793 to AUS$43,134 depending on credentials. Preference will be given to candidates with a relevant Ph.D. and strong research record pertinent to appointment area. Interested applicants should address specific enquiries to the appropriate contact person.
Applications close Friday 17th February 1995 (for further details, see the full version of this announcement).
The Department of Computer Science at the University of Rostock seeks a candidate for a C1 (BAT IIa) position at the Institute of Theoretical Computer Science starting March 1, 1995 (or later). The position is temporary for three years, with the possibility of extension for another three years.
Candidates are required to know (or be willing to learn in a reasonably short period) the German language. They should be interested in research and education in Computer Science and especially Theoretical Computer Science.
The candidate has the possibility to write a dissertation or habilitation thesis. The group's active research interest includes graph algorithms, structural properties of graphs and graph models in several fields of computer science including e.g. relational database schemes, parallelity and complexity.
For further information and applications please contact
Prof. Dr. A. Brandstädt
FB Informatik
Universität Rostock
18051 Rostock
e-mail: ab@informatik.uni-rostock.de or send applications directly to
Universität Rostock
Dezernat für Personalangelegenheiten
18051 Rostock
The university strongly encourages applications from female candidates.
The University of Idaho is expanding its engineering program in Boise (Idaho) and invites applications for two tenure-track faculty positions at assistant professor level and one at full/associate professor level in the computer engineering program for the fall semester 1995. Particular areas of interest include real-time systems, computer engineering, and software engineering. The program is offered jointly by the faculties of electrical engineering and computer science.
Qualifications for the positions include an earned Ph.D. in computer engineering, electrical engineering, or computer science; industrial experience; the ability to communicate effectively; and teaching and research ability. Preference will be given to applicants with previous teaching and research experience, and the ability to effectively work with industry. The incumbents will teach courses in the computer engineering program. Successful applicants will also conduct research, supervise M.S. and Ph.D. students, and assist in the development of the curriculum and laboratories to support the program in Moscow and Boise.
The University of Idaho is the land-grant university of Idaho and has statewide responsibility for engineering education. The main campus is located in Moscow, with branch programs in Boise and Idaho Falls.
Faculty are sought who can work cooperatively with engineers from regional manufacturers on both fundamental and applied research opportunities. Faculty can also participate in the Engineering Assistance Center that provides technology extension services to small and medium sized manufacturers.
Applicants should submit a curriculum vitae, a statement of both teaching and research interests, and the names of four references to:
Dr. Thomas Miller, Search Committee Chair, College of Engineering
University of Idaho, Moscow, ID 83844-1010 (search95@cs.uidaho.edu)
Applicants will be accepted until February 15, 1995 or until suitable candidates are selected.
To enrich education through diversity, the University of Idaho is an equal opportunity/affirmative action employer.
A more informative version of this announcement is on the WWW .
The Table of Contents of this book announcement is available.
This database theory book provides a focused presentation of the core material on relational databases, and presents a number of advanced topics in a unified framework. Some of the advanced material has never before been presented in book form. The style is rigorous, with detailed proofs and many exercises. The text and numerous examples highlight the intuition underlying the development. As a textbook, the book is aimed at graduate students and seniors who would use it as the main text in a database theory course, or as complementary material in a database systems course. It can also serve as a reference for database researchers and for other computer scientists interested in databases.
The book is published by Addison-Wesley and available wherever technical books are sold. To order the book directly from the publisher, call 1-800-447-2226 or 617-944-3700. Please supply the complete ISBN No. 0-201-53771-0 when ordering.
Author Information
My PhD thesis is available online, via my WWW page . or via anonymous ftp .
Abstract
The goal of my thesis is to extend current methods for compiler derivation and verification to languages which exhibit true concurrency. The work has proceeded through the following steps.
A process calculus, called CLAM, was defined, based on the lambda-calculus and modelling true concurrency. CLAM was used to define the semantics of a simple concurrent functional language, called Urlang, which was inspired by the programming language Erlang, which is in industrial use. A bytecode compiler for Urlang was then derived and proven correct, and a multiprocessor bytecode interpreter was implemented in Concert/C and proven correct. Finally it is argued that those features of Erlang which are not present in Urlang are easily added into our framework, either via source-to-source transformations into core Urlang or by means of straightforward additions to the operational semantics of CLAM.
The proceedings of Graph Drawing '94 (DIMACS International Workshop, Princeton, NJ, October 10-12, 1994) will be available in mid January:
Title: Graph Drawing
Editors: R. Tamassia and I. G. Tollis
Series: Lecture Notes in Computer Science
Volume: 894
Publisher: Springer-Verlag
ISBN number: 3-540-58950-3
The proceedings can be purchased through bookstores, or directly from any Springer office, in particular from:
Springer-Verlag, Order Processing Department
Postfach 31 13 40, D-10643 Berlin, Germany. Fax: + 49 30 8207301
Springer-Verlag New York, Inc.
P.O. Box 2485, Secaucus NJ 07096-2485, USA. Fax: + 1 201 3484033
Phone: 1 800 SPRINGER (1 800 7774647), toll-free from the US
The proceedings can also be ordered by email to: order@springer.de .
Authors or Editors of Springer books, as well as contributing authors (particularly to LNCS/LNAI Proceedings), are entitled to buy any book published by Springer-Verlag for personal use at the `Springer-author' discount of 1/3 off the list price. Such preferential orders can only be processed through Springer directly and not through bookstores). Reference to a Springer publication should be given in the order.
The list price of the GD'94 proceedings is DEM 94.00 (about USD 60). The special price for Springer authors is DEM 62.66 (about USD 40). Shipping charges are DEM 5.00 per book for orders sent to the Berlin office, and USD 2.50 (plus USD 1.00 for each additional book) for orders sent to the Secaucus office.
Payment of the book(s) plus shipping charges should be made by giving a credit card number together with the expiration date (Eurocard / Mastercard, Visa, Diners and American Express are accepted), or by enclosing a check (mail orders only).
This and other information on GD'94 (including the table of contents of the proceedings) is available via WWW and FTP .
Abstracts of the papers listed below, together with more detailed information (reading advice, instructions for FTP retrieval of the full papers, etc.) are in the full version of this announcement.
New Notions of Reduction and Non-Semantic Proofs of Beta Strong Normalization in Typed Lambda Calculi
by Joe Wells and A.J. Kfoury
Boston Univ. Comp. Sci. Dept. Tech. Rep. 94-014
transfer by anonymous ftp (93K).
Kripke models and the (in)equational logic of the second-order lambda-calculus
by Jean Gallier
transfer by anonymous ftp .
Proving Properties of Typed lambda-Terms Using Realizability, Covers, and Sheaves
by Jean Gallier
both dvi and postscript versions ftp-available.
Typing untyped lambda-terms, or Reducibility strikes again!
by Jean Gallier
both dvi and postscript versions ftp-available.
Parametricity and variants of Girard's $J$ operator
by Robert Harper and John Mitchell
available on the WWW .
or by transfer by anonymous ftp .
The paper is available by anonymous ftp, both in dvi and in postscript format.
One year ago I announced essential progresses on additives, both on proof-nets and on geometry of interaction. The paper on GOI was quickly written, but the paper on proof-nets was postponed, since I found a bug when I wrote the details. Recently I discovered the two systems with constant cut-elimination complexity, ELL and LLL. I tried to make a proof with old fashioned methods, i.e. sequent calculus. This was extremely painful (difficult to avoid the nonsense of double layer sequents, difficult to provide a natural size for proofs etc.) In fact -assuming I had the patience to cope with these minor technicalities, the reader would have got a symmetric problem, i.e. to find out what is the central idea in this bureaucratic mess. The use of sequents here was nothing but a childish game of encryption/decryption. This is why I decided to do it with proof-nets. The problem is that additives play an important role in LLL (not that much in ELL), and that I was never satisfied with the extant notion of proof-net. But it turns out that the extant notion (equipped with a lazy cut-elimination) normalizes in linear time, and that's enough for what I wanted to do. This is the reason why I decided to write a survey paper concerning proof-nets. Its aim is to provide an alternative syntax, in case one wants to do elegant proof-theory or achieve subtle aims, or simply protect forests...
The paper mainly deals with additive proof-nets, for which the best known solution is presented, and their lazy normalization. The discussion about possible improvements and the description of the full procedure are postponed to an appendix. The paper proceeds with the unproblematic extension to quantifiers (which look like oversimplified additives), and the treatment of exponentials, for which we restrict to weakening and contraction: the other rules, e.g. the rules for LLL or ELL, will be considered in a forthcoming paper. The weakening rule is also slightly problematic, but this is a rather minor question.
A simple semantic consistency proof for Map Theory
based on $\xi$-denotational semantics
by Ch. Berline and K. Grue
berline@logique.jussieu.fr
grue@diku.dk
Map theory, which is a foundation of mathematics based on lambda-calculus instead of logic and sets, has been introduced in [Grue, TCS 102(1), 1992].
Map theory is an equational theory which embodies predicate calculus; from the metamathematical point of view its strength lies somewhere between ZFC and ZFC+SI , where SI asserts the existence of an inaccessible cardinal.
The first result is proved in [G] by means of a syntactical translation of ZFC (including classical predicate calculus) within map theory, and the second by building a model of map theory within ZFC+SI. This latter construction is however highly technical, though the starting intuitions are quite natural.
We present here a semantic proof of the consistency of map theory within ZFC+SI, which is in the spirit of denotational semantics and relies on mathematical tools which reflect faithfully, and in a transparent way, the intuitions behind map theory.
This paper (submitted) is now available on the WWW . and by anonymous ftp, either in GNU-compressed form . or as a non-compressed dvi or Postscript file.
Both papers are available (and code also) by anonymous ftp .
My thesis presents this work more clearly and should be available within the next month.
Semantic Lego (written December 1993)
This paper describes an approach to monad transformers based on lifting. A monad may have several operators defined on it besides unit and bind. When we transform the monad, we lift the operators through the transformer and also add new operators. This approach comes almost directly from Moggi's 1989 notes, which are also available from the above ftp site. We present examples in Scheme and work in terms of functional programming rather than denotational semantics.
Stratified Monads (written June 1994)
We improve on the above by formalizing an intermediate interface between the basic denotational semantics and the language constructs, called a stratified monad. Using stratified monads, we can split semantics into two parts, a semantic algebra, implemented by a stratified monad, and a language algebra, implemented by a set of constructs definitions over the semantic algebra. The advantages are:
This approach differs from Mosses's action semantics because we form specialized semantic algebras from component modules. That is, we are no longer limited to a single, fixed semantic algebra. Furthermore, we can reason equationally over the algebra in a disciplined way using the stratified monad laws (these are presented in my thesis).
Ph. de Groote (Ed.), Volume 8 of the Cahiers du Centre de logique
(Univ. catholique de Louvain), Academia, Louvain-la-Neuve (Belgium),
1995, 364 pages. ISBN: 2-87209-363-X, ca. BEF 1450 or US$ 50.
Table of Contents
Summary
Study of the Formulae-as-Types correspondence, also known as the Curry-Howard isomorphism, has been recently revived by theoretical computer scientists, through the program-as-proof correspondence.
The first four papers are introductory. The volume starts with a reproduction of the seminal papers by Curry-Feys and Howard. Then de Bruijn motivates his Automath language, bringing to light the program-as-proof correspondence. Finally, the very detailed paper of Gallier presents and discusses the correspondence between natural deduction proofs and $\lambda$-terms.
The next three papers are concerned with applications. First, Geuvers presents the Calculus of Constructions, a typed $\lambda$-calculus for higher order intuitionistic logic. Next, Girard provides a survey of his linear logic. The volume ends with a synthetic description of Intuitionistic Zermelo-Fraenkel set theory by Lipton, including realisability and categorical interpretations. Those three papers are self-contained and include extensive lists of references.
If you want more information, please write to either of
Marcel Crabbe' (crabbe@risp.ucl.ac.be) Departement de philosophie
Daniel Dzierzgowski (ddz@agel.ucl.ac.be) Departement de mathematique
both at Universite' catholique de Louvain.
The complete bibliography of the first ten Workshops on Abstract Data Types is available as technical report of the Genova University (number PDISI-95-01). The postscript file can be obtained by anonymous ftp.
In the same directory a bibtex file can be found too. The bibtex file includes all the entries of this bibliography.
Anonymous ftp is still experimental at our site; in case of technical troubles with using it, please contact cerioli@disi.unige.it .
If you have no access to ftp facilities or to a postscript printer, a hard copy of wadts-bib.ps can be required to
DISI - Dipartimento di Informatica e Scienze dell'Informazione
Viale Benedetto XV, 3, I-16132 Genova, Italy
Abstract of wadts-bib.ps
We look back on ten Workshops on Abstract Data Types. Organizers and publications, a list of authors referencing their talks and papers on the workshops, and a workshop bibliography are presented.
Contents of wadts-bib.ps
Contents of wadts.bib
The data used to build section 4, in bibtex format.
Recently, Lincoln, Scedrov, and Shankar proved that IMLL2 and MLL12 are undecidable by simulating the rules of contraction and weakening using second order propositional quantifiers and the multiplicatives (see the last message of the linear list).
Here is a new result:
Theorem: MALL2 is undecidable.
This is proved by a direct encoding of Minsky machines. We do not use the contraction axiom C = forall X. X -o X*X, but a `soft' version:
C' = forall X. X&1 -o X*X.
Our encoding is essentially Kanovich's one with A&1 in place of !A. Of course, the main difficulty is to show that C' does not produce fake computations. For this, we introduce a specific phase model.
Two remarks:
When I first introduced the notions of algebraically complete categories (every endo-functor has an initial algebra) and algebraically compact categories (every endo-functor has an initial algebra naturally isomorphic to a terminal co-algebra) I thought that such things would exist in the classical foundations only in degenerate form. It was a surprise when I noticed that the categories of countable sets and of countably dimensioned vector spaces are algebraically complete. I'm now surprised by:
The category of separable Hilbert spaces and linear operators of
bound at most 1 is algebraically compact.
As in the earlier cases one doesn't really need the controlling cardinal number to be aleph-naught. To avoid using the axiom of choice one can state the more general result by taking an arbitrary Hilbert space A and defining A by:
Then:
A is algebraically compact.
The theorem holds for both the real and complex cases.
In the proof I use the surprising (to me) fact that in the categories in question every half-invertible map has a unique half-inverse. (That is, every map has at most one left-inverse and one right-inverse.) All the other examples from nature that I can think of are categories in which the only half-invertibles are invertible. Are there others?
Update of [SIAN05p4-2] .
The 27th Annual ACM Symposium on Theory of Computing (STOC 95), to be held in Las Vegas, NV, May 29-June 1, 1995, now has a WWW page . Please browse it for more information about the conference.
The special interest group on parallel and distributed algorithms of the German computer science society maintains a collection of WWW pages that are related to the topics of the SIG. Here is the home page .
Among others, there is a page where calls for papers to conferences, journals etc. are collected, programs to conferences, announcements to graduate programs and so on. This page is available .
It's not necessary to understand German for reading this page because almost all information is in English.
If conferences offer WWW pages, links to them are also provided.
In addition to the WWW site maintained by the special interest group on parallel and distributed algorithms of the German computer science society recently mentioned, another WWW page of interest to the theory community is. available (sorry for the long URL).
This site contains some general theory-related papers, pointers to software, conference CFPs and programs, pointers to other sites as well as searchable lists of theory conference attendees.
The full version of this announcement is available.
Work on formal semantics of programming languages is an area of intensive research. Several successful approaches exist, and numerous books on the subject have been published. See, e.g., Gunter, Nielson and Nielson, Schmidt, Tennent, or Winskel.
There are a number of formal semantics of real-world programming languages. In order to establish which approach has been used to describe the semantics of which language, we would like to maintain corresponding lists.
We are seeking formal semantics of languages such as SML, Erlang, Haskell, Miranda, Clean, Gofer, Opal, Prolog, C, C++, Smalltalk, Pascal, Cobol, Fortran, Sisal, Modula-2, Oberon, Occam, Lisp, Scheme, Ada, Eiffel, Spark, etc. We are not looking for formal semantics of languages such as PCF, simple `while' languages or xy-`like' languages.
Semantics given in formalisms such as Action, axiomatic, natural, SOS, or denotational semantics, or evolving algebras are welcome.
There will be two lists: (1) one for complete semantics, and (2) the other for formal semantics of significant and large parts of languages, including information on which constructs are not covered. Please submit only semantics that are published or available by ftp or WWW, to ensure public access to the semantics.
The lists (1) and (2) are respectively available. Please send your entries (in the format used in these URL's) to Peter Baumann (E-mail: baumann@ifi.unizh.ch).
To start fresh a new year, we have moved the LOTOS bibliography database into
(:source
:version 3
:ip-address "138.4.2.10"
:ip-name "sanson.dit.upm.es"
:tcp-port 210
:database-name "lotos"
:cost 0.00
:cost-unit :free
:maintainer "pepe@dit.upm.es"
:description "LOTOS bibliography"
)
For some www browsers, the following should work.
It is a sum of Ken Turner's and my own. Sorry for the duplicates, but it is too much work to sort them out.
The full version of this announcement is available.
There are close to 1,100 sites where the SPIN verification software is now installed. This is a nice enough number to start supporting SPIN users a little more actively. This first issue of the SPIN News mailing goes only to a select number of people (approx 140) that have in the last few months asked about the verifier and its applications, and a few honorary recipients. The next issue will only go to those who ack this mail (see pt 1. below).
The main reason for these mailings is to have a channel to send out brief reminders whenever an update of the SPIN software takes place - bug fixes, extensions, or major improvements such as the switch to Version 2.0.
Two other types of items can also be included in such mailings: answers to frequently asked questions from SPIN users about modeling, complexity control, algorithms etc., and announcements or question from people who would like to get in touch with other SPIN users.
The new SPIN Version 2.0, available from January 1 1995 on, includes a significantly richer specification language, as well as an implementation of a partial order reduction technique that preserves all safety and liveness properties, and that is compatible with all existing verification modes supported by SPIN. With the reduction, problem sizes of yet another order of magnitude larger may have come within reach of formal verification techniques.
SPIN Version 2.0 can be retrieved in source form together with some documentation and with a graphical interface called xspin - freely via anonymous ftp .
The full version of this announcements contains a short description of some current SPIN projects.
This time we have double good news for the those interested in the FoReST seminar, the colloquium on Formal Representation and Specification Techniques
First of all, we are happy to invite you to our first meeting in the FoReST Spring '95 program. This time, again we have two speakers:
The other good news is that we have succeeded in developing a www page for the FoReST seminar. The page is. available .
On or via this page, you can find information about how to reach Utrecht University, there are abstracts of the talks just announced, and you can even find a complete FoReST Spring '95 program.
If you have problems with reaching this page, please send an email to wiebe@cs.ruu.nl then you will be put on a separate mailing list, and you will keep receiving abstracts of our presentations by electronic mail.
For further information about the seminar, please contact any member of the board of FoReST. This board consists of the following people:
<location> := ftp://ftp.cs.utwente.nl/pub/doc/amast/
<location> := http://www.cs.utwente.nl/data/amast/
Date: 10/02/1995
...
Ewa Orlowska [O1], V. S. Alagar [M1],
Types Forum [M2], Didier Begay [C1],
Richard Gerber [C2], Michael Huth [C3],
Vassos Hadzilacos [C4], Pierre Lescanne [C5],
Jan Heering [C6], DMANet [C7],
Marianne Baudinet [C8], Jörg Desel [C9],
Roberto Tamassia [CA], [L3], Ugur Halici [CB],
Hajime Ishihara [CC], Hanne Riis Nielson [CD],
Jose Luiz Fiadeiro [CE], Bob Rosebrugh [CF],
Zena Matilde Ariola [J1], Michiel Smid [J2],
Dave Schmidt [J3], H. Levent Akin [J4],
Eike Best [J5], Michael Johnson [J6],
Marta Kwiatkowska [J7], Gordon Plotkin [J8],
Boaz Patt-Shamir [J9], Vijaya Ramachandran [JA],
Clyde Monma [JB], George Milne [JC],
A. Brandstädt [JD], Mike Barnett [JE],
Richard Hull [L1], Dave Gladstein [L2],
Joe Wells [L4], Jean Gallier [L4],
John Mitchell [L4], Jean-Yves Girard [L5],
Ch. Berline [L6], David Espinosa [L7],
Marcel Crabb'e [L8], Maura Cerioli [L9],
Yves Lafont [P1], Peter Freyd [P2],
Ian Parberry [S1], Rolf Wanka [S2],
Dennis Grinberg [S3], Peter Baumann [S4],
Jose A. Manas [S5], Gerard Holzmann [S6],
Wiebe van der Hoek [S7].
This issue of AMAST Links is available in four forms:
Note: This issue will also be available, in all of its four forms, by anonymous ftp from the AMAST repository at the University of Twente. File names will be the same as above, but under the ftp directory .