[ToC] ==================\=====================/====== AMAST Links 02 03 _____________________ \ / _____________________ Contributions are / \ AMAST Links / \ 15 March 1995 welcome! e-mail to ( / \ ) e-mailed to: amast@cs.utwente.nl \ / Vol. 02 Issue 03 \ / 622 subscribers ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^ An index to all issues of the AMAST newsletter is available on the WWW: URL: http://www.cs.utwente.nl/data/amast/links/AL-Index.html A general index to AMAST information on the WWW server in Twente is at: URL: http://www.cs.utwente.nl/data/amast/Index.html The hypertext version of this issue is available at: URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/AL0203-ToC.html _________________ Table of Contents Meetings [M1] AMAST'95 prelim. programme available on March 16 (upd. [AL0201M1]) [M2] Mailing list and discussion at TAPSOFT'95 (update of [AL0202M2]) [M3] TAPSOFT'95: Reminder & More Information (update of [AL0202M2]) [M4] Workshop on Real Numbers and Computers (update of [AL0202CI]) [M5] ICALP'95 Program & Registration Information (upd. of [SIAN05p2-5]) [M6] LICS'95 Accepted Papers (update of [SIAN05p2-8]) [M7] MCU'95 Workshop Programme (update of [AL0202M6]) [M8] Spring School Adv. Functional Prog. Techniques (upd. [AL0102M3]) [M9] Dutch/German Workshop Nonmonotonic Reasoning (upd. [SIAN03p2-5]) [MA] Paderborn Spring School on Efficient Use of Parallel Systems [MB] 7th Eur. Summer School on Logic, Language & Information, ESSLLI'95 [MC] Course: Introduction to Theorem Proving Using Isabelle [MD] Workshop Theorem Proving with Analytic Tableaux & Related Methods [ME] 12th Int'l Conf. on Logic Programming, ICLP'95 [MF] 5th meeting on Order in Algebra and Logic [MG] Colloquium on Constructivity in Mathematics and in Vision [MH] Forum on Parallel Computing Curricula [MI] Summer School on Chaitin Complexity and Applications CfPs [C1] 23rd Int'l Colloquium Automata, Languages & Programming, ICALP'96 [C2] Annual Conf. European Assoc. for Computer Science Logic, CSL'95 [C3] Int'l Conf. Constraint Programming, CP'95 (update of [AL0103C6]) [C4] COCOON'95: Reminder and More Information (update of [AL0102C7]) [C5] Joint Workshop on Graph Rewriting and Computation, SEGRAGRA'95 [C6] I.C. Structural Information & Communication Complexity, SIROCCO'95 [C7] 7th IEEE Symp. Parallel and Distributed Processing, SPDP'95 [C8] 1st Int'l Symposium on Language, Logic and Computation, LLC'95 [C9] Logic Colloquium 1995 [CA] Int'l Static Analysis Symposium, SAS'95 [CB] 36th Annual IEEE Symp. on Foundations of Computer Science, FOCS'95 [CC] Isabelle Users Workshop [CD] 10th Latin American Symposium on Mathematical Logic [CE] 4th Int'l Conf. on Information and Knowledge Management, CIKM'95 [CF] 15th Conf. Found. Softw. Technol. & Theor. Comput. Sci., FSTTCS'95 [CG] 9th Conf. on Neural Information Processing Systems, NIPS'95 Jobs [J1] Two openings at Honeywell Technology Centre, Minneapolis, MN, USA [J2] Postdoc at Royal Institute of Technology, Stockholm, Sweden [J3] Postdoctoral position at Xerox PARC, Palo Alto, CA, USA [J4] Associate Professorship in Computer Science, Univ. of Aarhus, DK [J5] Research Fellowships, Queen Mary & Westfield C., Univ. London, UK [J6] Postgraduate Bursaries in TCS, Computing Lab., Univ. of Kent, UK [J7] Research Studentships in CS, Univ. of East Anglia, Norwich, UK Literature [L1] AMAST Book: Algebraic Specification Techniques...the ACT Approach [L2] AMAST Book: Theories & Experiences for Real-Time System Developm. [L3] AMAST Book: Construction & Analysis of Transition Systems with MEC [L4] Book: System Software & Software Systems - Concepts & Methodology [L5] PhD Th: Performance-Oriented Spec. of Communication Protocols... [L6] Proc. 6th Nordic Workshop on Programming Theory (Aarhus, DK, 1994) [L7] Proc. CAEN'94 (Categories, Algebres, Esquisses, Neo-esquisses) [L8] Paper: Higher-dimens. algebra and topological quantum field theory [L9] Paper: Light Linear Logic [LA] Paper: What is a Categorical Model of Intuitionistic Linear Logic? [LB] Paper: A Mixed Linear and Non-Linear Logic: Proofs, Terms & Models [LC] Paper: Higher-Order Logic Programming [LD] Course notes on category theory Tools [T1] Axiomatic type classes in Isabelle, documentation (upd [AL0202T4]) [T2] LOLA (LOtos LAboratory) 3R6 release announcement (upd. [AL0202T5]) [T3] Logic courseware: Turing's World, Tarski's World, Hyperproof [T4] LiDIA: A library for computational number theory Problems [P1] Kleisli category for multiple monads? Services [S1] AMAST Series in Computing: Address and Order Information [S2] Gathering Information about Teaching in Computable Analysis [S3] Assembling a WWW page on Isabelle projects [S4] Information request from ACM SIGACT Long Range Planning Committee Archive [A1] New items in Twente AMAST repository [A2] This issue [M1] ================================================ AMAST Links 02 03 Algebraic Methodology And Software Technology, AMAST'95 Montreal, Canada, July 3-7, 1995 *Update* of [AL0201M1] A preliminary version of the AMAST'95 programme is planned to be available on Thursday March 16 at URL: http://www.cs.utwente.nl/data/amast/amast95/PreliminaryProgramme.txt [M2] ================================================ AMAST Links 02 03 Mailing list and discussion at TAPSOFT'95 *Update* of information in [AL0202M2] There will be a discussion at TAPSOFT'95 on "The Future of European Spring Conferences on Theory and Practice of Software Science". It is proposed to set up an annual joint conference, taking place in Europe each spring, and covering a wide range of topics in Software Science. This will be a loose and open confederation of existing and new conferences and other events. The overall aim is to create a popular annual meeting that will act as a strong magnet for academic and industrial researchers working on topics relating to Software Science. For more information, including instructions on how to join the mailing list for discussion of the proposal prior to TAPSOFT'95, see the WWW page at URL: http://www.dcs.ed.ac.uk/~dts/tapsoft [M3] ================================================ AMAST Links 02 03 TAPSOFT'95: Reminder and More Information *Update* of information in [AL0202M2] *Reminder:* *Deadline* for *receipt* of registrations at reduced rate is *15 March*. The final TAPSOFT '95 programme (currently in preparation) includes the following extra event, not previously announced: *Invited Lecture:* Vaughan Pratt (Stanford Univ.): _Anatomy of the Pentium Bug_ Vaughan Pratt has been closely involved with analysing the significance of a recently-revealed bug in the Intel Pentium computer chip. His topical paper on the Anatomy of the Pentium Bug presents general background and new results. This extra invited lecture has been squeezed into the programme on the Thursday afternoon, immediately preceding the discussion session. The presentation is to include an online demonstration of the bug. The hypertext version of the *Preliminary Programme* has already been updated to reflect this addition; it can be accessed via the WWW URL: http://www.brics.aau.dk/tapsoft/ The Schedule of Events there now has links to: o *Abstracts* of all TAPSOFT '95 papers o *Proposals* concerning the future of European Spring conferences on Software Science (discussion session, Thursday afternoon). For further information about TAPSOFT '95, please see the WWW pages or contact the Secretariat: TAPSOFT '95 BRICS, Dept. of Computer Science, University of Aarhus Ny Munkegade, Bldg. 540, DK-8000 Aarhus C, Denmark E-mail: tapsoft@brics.aau.dk, Fax: +45 8942 3255 WWW URL: http://www.brics.aau.dk/tapsoft/ [M4] ================================================ AMAST Links 02 03 Workshop on Real Numbers and Computers Ecole des Mines de Saint-Etienne, Saint-Etienne, France, 4-6 Avril 1995 *Update* of information in [AL0202CI]. The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M4.txt It contains the _Call for Participation and Information Package_, including Preliminary Programme, Registration Information, and General Information. *Reminder:* A special issue of the new journal JUCS, dedicated to the "practical aspects" of the implementation of real number arithmetic, and a special issue of TCS dedicated to the "theoretical" aspects will follow. People still can submit papers to the special issue of TCS. (for information, send an e-mail to jmmuller@lip.ens-lyon.fr) *Important:* You can get more information from this WWW page URL: http://www.emse.fr/english/stetienne.html as well as from the WWW page at URL: http://www.ens-lyon.fr/~jmmuller/conf_st_etienne/real_numbers.html [M5] ================================================ AMAST Links 02 03 22nd Int'l Colloquium on Automata, Languages, and Programming, ICALP'95 Szeged, Hungary, July 10--14, 1995 Program and Registration Information *Update* of information in [SIAN05p2-5] The (LaTeX) full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M5.tex The full announcement contains the ICALP'95 program, registration form, and general information about the conference. *Further information* is available on the WWW at URL: http://www.inf.u-szeged.hu/~icalp95 [M6] ================================================ AMAST Links 02 03 Tenth Annual IEEE Symposium on Logic In Computer Science, LICS'95 San Diego, California, June 26-29, 1995 *Update* of information in [SIAN05p2-8] The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M6.txt The full announcement contains the list of _Accepted Papers_, cronologically presented according to a preliminary version of the LICS'95 programme. [M7] ================================================ AMAST Links 02 03 Int'l Worlshop on Universal Machines And Computations, MCU'95 Paris, France, March 29, 30, 31 *Update* of information in [AL0202M6] The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M7.txt The full announcement contains the _MCU'95 Workshop Programme_, both in French and in English. Abstracts of the invited talks are available by anonymous ftp at URL: ftp://capella.ibp.fr/pub/mcu95/ (Get the file README first, then follow its instructions.) *Further information.* Correspondence: Maurice Margenstern International Workshop "Universal Machines and Computations" LITP, 55-56, b.119 Universite' Paris 7 2, place Jussieu F - 75251 PARIS CEDEX 05 E-mail: mcu95@capella.ibp.fr, Fax: (33 1) 44 27 68 49 [M8] ================================================ AMAST Links 02 03 1st Int'l Spring School on Advanced Functional Programming Techniques Baastad, May 24--31, 1995, Sweden *Update* of information in [AL0102M3] The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M8.txt _Abstracts of the talks_ are in the springschool's WWW page, at URL: http://www.cs.ruu.nl/people/erik/springschool.html *Reminder:* The deadline for applications is April 1, 1995. The spring school will be held in Baastad, a small town between Copenhagen and G"oteborg on the Swedish west coast. Participants are expected to arrive on Tuesday May 23 1995. The spring school lasts until Wednesday May 31 1995. The number of attendants is limited, so it is important to apply as soon as possible by completing the form at the end of the full version of [AL0102M3]. Further information can be obtained via email from the address baastad@cs.chalmers.se or via the springschool's WWW page (see above). [M9] ================================================ AMAST Links 02 03 Dutch/German Workshop on Nonmonotonic Reasoning Utrecht, March 29 - 31, 1995 *Update* of information in [SIAN03p2-5]. The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203M9.txt The full announcement contains the _Final Call for Participation_, with registration information, details relating to accomodation and travel, and the _list of accepted papers_. There's room for about 40-50 people. So please register as soon as possible. For the latest information regarding the workshop, please consult the workshop's WWW page at URL: http://www.cs.ruu.nl/~bernd/nmr-ws.html [MA] ================================================ AMAST Links 02 03 Paderborn Spring School on Efficient Use of Parallel Systems Paderborn, Germany, April 25 - 28, 1995 The full version of this information is available in two forms, plain-text (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MA.? *General Information:* This school is organized within the ESPRIT project ALCOM II and the HCM project "Efficient use of parallel computers: architectures, mapping and communication". Its goal is to give an overview of recent research lines in the field of parallel algorithms and their efficient implementation on parallel computers. It is addressed to graduate students and postdocs with knowledge or interest in parallel algorithms, especially to those involved in the above projects. *Location:* In order to minimize the cost for the participants the school will take place in Paderborn near the university, and accommodation (single room, double room on request,shower and rest-rooms on the corridor) will be provided about 30km away from Paderborn. A bus service between the sites will be offered to the participants. *Lectures:* The program will consist of six lectures of about 3 to 4 hours each. Speakers include Jean-Claude Bermond (Nice), Michel Cosnard (Lyon), Alan Gibbons (Warwick), Juraj Hromkovic (Kiel), Friedhelm Meyer auf der Heide (Paderborn), Burkhard Monien (Paderborn). *Talks and Discussions:* One afternoon is reserved for short talks given by the participants, discussions, and presentations of open problems. Participants willing to give a talk should send an abstract of at most 2 pages written in LaTeX by email to spring@uni-paderborn.de *Fees:* The fee is 520.-DM for registrations before March 17th and 550.-DM for late registrations. The fee covers accommodation, lectures, full board, reception, conference dinner and printed information. For forty participants from the above projects a grant of 400.-DM is available. To receive this grant, please contact Walter Unger before registration (preferably by email spring@uni-paderborn.de). [MB] ================================================ AMAST Links 02 03 7th European Summer School in Logic Language and Information, ESSLLI'95 Barcelona, Spain, August 14-25 1995 The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MB.txt *Topics* The main focus of the Summer School is the interface between logic, linguistics and computation, where it concerns the modelling of human linguistic and cognitive abilities. The 1995 School programme will include courses, workshops, and symposia covering a variety of topics within six areas of interest: Logic, Language, Computation, Logic and Computation, Computation and Language, Language and Logic. *Lecturers* Logic and Language : G Link, J van Eijck, J Jaspars, A Visser, C Vermeulen, M Kracht, B Keller, M Kanazawa, D de Jongh, F Moltmann, C Fox, H Rott, R Cooper, M Poesio. Logic : R Jansana, I Hodkinson, J Flum, P Blackburn, M de Rijke, Y Venema, J Font, K Devlin. Computation and Logic : D Basin, S Mathews, F Baader, G Koestler, H Barringer, D Gabbay, C Brink, L Wallen, M Marx, S Mikulas, F Baader, K Schlecta, S Biundo. Computation : M Nielsen, C Paulin-Mohring, N Jones, L Meertens, S Peyton-Jones, B Haglund. Language and Computation : E Stabler, M Johnson, R Bod, R Scha, M Moortgat, M Dalrymple, R Kaplan, B Carpenter, G Morrill, V Abrusci, R Dale, M Ellison, F verdejo, R Kempson. Language : P Miller, J Bresnan, H Verkuyl, H Clahsen, D Oehrle, J Doerre, S Manandhar, A Zaenen, L Sadler. *Further Information* ESSLLI95, GILCUB, Avda. Vallvidrera 25, E-08017 Barcelona Fax +43 3 2054656. Tel. +43 3 2033597. E-mail esslli95@gilcub.es [MC] ================================================ AMAST Links 02 03 Introduction to Theorem Proving, Using Isabelle (Course) 12-14 July 1995, Cambridge, England The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MC.txt Immediately prior to Mathematics of Program Construction (MPC '95). *Full information:* available via the WWW page at URL: http://www.cl.cam.ac.uk/users/lcp/isabelle-course.html *Topics* The course uses lectures and practical sessions to teach students how to use the Isabelle system to perform proofs in higher-order logic. Main points: o Single-step proof checking. Forward and backward proof. o Declaring types and constants. Quantifier reasoning. o Higher-Order Logic in Isabelle. Advanced proof tools. *Lecturer* Lawrence C Paulson, the originator of Isabelle. *Cost* 650 pounds sterling (350 pounds for academics) plus accommodation. *Technical Correspondence* Lawrence C Paulson, Computer Laboratory, Pembroke Street, Cambridge CB2 3QG, England. E-mail lcp@cl.cam.ac.uk *Administrative Correspondence* The Registration Administrator, Programme for Industry 1 Trumpington St, Cambridge CB2 1QA, England. Tel +44 (0)1223 302233. E-mail: rjs1008@cus.cam.ac.uk [MD] ================================================ AMAST Links 02 03 Workshop On Theorem Proving With Analytic Tableaux And Related Methods castle Rheinfels, St. Goar am Rhein, Germany, May 7-10, 1995 Full information on the WWW at URL: http://www.uni-koblenz.de/~tab95/CallForParticipation.html *Topics.* Mechanisation of reasoning with tableaux and related systems (analytic tableaux, model elimination, connection method, sequent calculi). Covered are theoretical aspects of classical and non-classical logics, as well as topics related to practical implementations. *Invited speakers.* Wolfgang Bibel, Ricardo Caferra. *Program Committee.* Peter Baumgartner, Krysia Broda, Marcello D'Agostino, Melvin Fitting, Ulrich Furbach, Dov Gabbay, Rajeev Gore, Jean Goubault, Reiner H"ahnle, Ryuzo Hasegawa, Rob Johnson, Thomas K"aufl, Reinhold Letz, Neil Murray, Ugo Moscato, Joachim Posegga, Peter Schmitt, Camilla Schwind, Graham Wrightson. *Local Arrangements.* Ulrich Furbach, Computer Science Institute, University of Koblenz Rheinau 1, 56075 Koblenz, Germany Fax: ++ 49 261 9119 499. Phone: ++ 49 261 9119 433 E-mail: tab95@informatik.uni-koblenz.de [ME] ================================================ AMAST Links 02 03 Twelfth International Conference On Logic Programming Kanagawa, Japan, June 13--18, 1995 The Preliminary Call for Participation is available through URL: http://daigo.sfc.keio.ac.jp/iei/iclp95.html *ICLP'95 Workshops:* o Abstract Interpretation of Logic Languages o Deductive Databases and Logic Programming o Abduction in Deductive Databases and Knowledge-based Systems o Inductive Logic Programming o Parallel Logic Programming *Further Information.* Contact the local arrangements chair: Dr. Mutsumi Imai Faculty of Information Environment, Keio University 5322 Endo, Fujisawa-shi, Kanagawa 252, Japan Phone: +81-466-47-5111 ext. 3223. Fax: +81-466-47-5350 Email: imai@sfc.keio.ac.jp [MF] ================================================ AMAST Links 02 03 Conference on Order in Algebra and Logic Merton College, Oxford, UK, 21-25 March 1995 This meeting continues a successful series held in Naples over the last few years, generously funded by Istituto Italiano per gli Studi Filosofici. On this occasion there is additional funding from The British Council, The British Logic Colloquium, the London Mathematical Society and The Royal Society. *Programme* *Tuesday 21 March* Dr A. Bichara (Roma) Order structure and algebraic varieties; Professor A. Baudisch (Berlin) A new stable group; Dr A.J. Wilkie (Oxford) On the decidability of the real exponential field; Professor L.P.D. van den Dries (Urbana) New o-minimal structures on the real field. *Wednesday 22 March.* Dr C.J. Mulvey (Sussex) Pure states of quantales; Professor M. Dalla Chiara (Florence) Quantum MV-algebras - a survey; Dr A. Ekert (Oxford) Quantum computation; Professor Sir Roger Penrose (Oxford) Is mathematical understanding fundamentally non-computable?. *Thursday 23 March.* Professor P. Longobardi (Naples) A problem of combinatorial type - finite groups containing many subgroups; Professor M Curzio (Naples) Kernels of congruences of some lattices of subgroups; Professor M. Tallini-Scafari (Roma) Combinatorial questions in infinite linear spaces (now being transferred to become first lecture on the 2 March) - half hour lecture. Dr J. Truss (Leeds) Cycle free partial orders; Dr P.M. Neumann (Oxford) Relations related to semilinear orderings and betweenness. *Friday 24 March.* Professor R. Grigolia (Tbilisi) Automorphism groups of free MV-algebras; Professor A. Di Nola (Naples) l-rings and Lukasiewicz logic; Professor R. Cignoli (no title as yet); Dr D. Gluschankoff (Angers) The prime ideal spectrum of a class of l-groups; Dr H. Priestley (Oxford) Duality theory in logic and logic in duality theory. *Saturday 25 March.* Informal arrangements. There will be a conference banquet at Merton College on 22 March and a dinner at an Indian restaurant on 24 March. *Further Information.* Angus Macintyre (email; ajm@vax.ox.ac.uk) [MG] ================================================ AMAST Links 02 03 "Constructivity, in Mathematics and in Vision" Colloquium, Ecole Normale Superieure, Paris, France Salle Dussane, 45, Rue D'Ulm, F-75005 Paris, Vendredi 31 Mars 1995 *Programme* o 9.30 Introduction au Colloque (Giuseppe Longo) o 9.45 Jean-Yves Girard (LMD, CNRS, Marseille) _Constructivite': vers une dualite' moniste_ o 11.15 Jean-Michel Morel (CEREMADE, Paris Dauphine) _Reconstruction visuelle et ge'ne'ricite'_ o 12.30 Pause o 14.00 J. Kevin O'Regan (CNRS et Univ. de Paris V) _La perception visuelle: Le monde comme me'moire externe_ o 15.15 Per Martin-L"of (Univ. Stockholm) _Mathematical constructions: mental or real_ o 16.30 Pause o 16.45 Conclusion et Discussion (introduites par Gerard Huet (INRIA), Giuseppe Longo et Jacques Ninio, CNRS et ENS). Entre'e libre. Organizateur: G. Longo. *Dept. Mathematiques et Informatique, ENS* *Renseignements:* Mme B. Van Elsen, DMI, ENS tel. ++33-1-4432-2034; fax 4432-2080; e-mail: vanelsen@dmi.ens.fr [MH] ================================================ AMAST Links 02 03 Forum on Parallel Computing Curricula March 31 - April 1, 1995 Wellesley College Science Center The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MH.txt *Important Notes:* o Please Note the change in the dates: the forum will be 2 full days, Friday 3/31/95 and Saturday, 4/1/95. o Even if you have already pre-registered, we need to know if you're planning to attend the banquet on Friday, March 31. Please let us know by March 15, 1995. o Directions to Wellesley and information on accommodations in the Wellesley area appear at the end of (the full version of) this announcement. In the last few years, courses on parallel computation have been developed and offered in many institutions as a recognition of the growing significance of this topic in computer science. Parallel computation curricula are still in their infancy, however, and there is a clear need for communication and cooperation among the faculty who teach such courses. This workshop will attempt to address this need by bringing together parallel computing researchers, faculty who teach parallel computing courses, and faculty who are interested in developing parallel computing courses in their own schools. It is expected that this workshop will create a forum that will facilitate the exchange of ideas, syllabi, course materials, software, and experiences among instructors of parallel computation courses. The intention of this workshop is to maximize interaction among those using innovative techniques, tools or strategies to teach parallel computation. We also want to encourage those faculty who are interested in using innovative materials to come and present to us the problems they have encountered. The results of this workshop will be compiled into a report, and resources will be placed on the internet. You are invited to the Forum on Parallel Curricula, March 31 - April 1, 1995. More information is available in URL: http://www.wellesley.edu/CS/forum.html [MI] ================================================ AMAST Links 02 03 Chaitin Complexity and Applications - Summer School Mangalia, Romania, 27 June - 6 July 1995 The LaTeX full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MI.tex The course will focus on basic results regarding the information theoretic limits of mathematics and their relevance for understanding the Universe. It will be supported by lab sessions in which Lisp programs will be used to explain and illustrate the theoretical ideas. *Key-Note Lecturer:* G. J. Chaitin, IBM Thomas J. Watson Research Center, New York, USA *Guest Lecturers:* o D. S. Bridges, University of Waikato, New Zealand o H. J" urgensen, University of Western Ontario, Canada o G. Markowsky, University of Maine, United States o K. Svozil, Technical University of Vienna, Austria *Course Secretary:* M. Tuatuar^am, Black Sea University 50, Primuaverii Blvd. Bucharest 1, Romania. Phone & Fax 401-312-8327 *Information Contact:* C. Calude, Computer Science Department, University of Auckland Private Bag 92019 Auckland, New Zealand. Phone +64-9-373-7599 x 5751 Fax: +64-9-373-7453. Email: cristian@cs.auckland.ac.nz *Topics* o Classical vs Constructive Mathematics o Algorithmic Information Theory o G"odel Incompleteness Theorem Revisited o Coding the Universe *General Information:* The working language is English. Participation fee of US $500 includes course attendance fee, printed materials, accommodation in two-bed rooms and meals. Special arrangements will be made for participants from countries of the Black Sea area and for those in Central and Eastern Europe. *Deadline* for application is 13 June 1995. *Payment* Participation fee of US $500 will be paid by mail, at the Romanian Bank of Foreign Trade, Bucharest, Romania, Account no 46.10.109.162.300.8 of the Black Sea University or in cash on arrival. [C1] ================================================ AMAST Links 02 03 23rd Int'l Colloquium on Automata, Languages, and Programming, ICALP'96 Paderborn, Germany, July 8th - 12th, 1996 The full version of this Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C1.txt ICALP'96 is the 23rd annual meeting of the European Association for Theoretical Computer Science. 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. *Submission* Authors are invited to submit 7 copies of an extended abstract not exceeding twelve pages by November 15th, 1995 to: Friedhelm Meyer auf der Heide Dept. of Mathematics & Computer Science and Heinz Nixdorf Institute University of Paderborn, D-33095 Paderborn, Germany Simultaneous submissions of papers to any other conference with published proceedings are not allowed. *Important Dates* Deadline for submission November 15th, 1995 Notification of acceptance February 16th, 1996 Final manuscript April 1st, 1996 Conference July 8th - 12th, 1996 *Further Information* A WWW page for this conference has been installed under URL: http://www.uni-paderborn.de/~icalp96/ This page will contain information and latest news. 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 [C2] ================================================ AMAST Links 02 03 Annual Conf. European Association for Computer Science Logic, CSL'95 Paderborn, Germany, September 22-29, 1995 The LaTeX full version of this Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C2.tex CSL '95 is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working in areas related to computer science. The scientific program consists of a tutorial on Finite Model Theory organized by H.-D. Ebbinghaus (Freiburg) with lectures by J. Flum (Freiburg) and E. Gr"adel (Aachen), during Sept 22. - 24, and of invited lectures and contributed papers, Sept. 25 - 29. The conference will be immediately preceded by the workshop on Higher-Order Algebra, Logic and Term Rewriting, HOA '95 which is announced separately. *Submissions:* Authors are invited to submit five copies of a draft of a full paper (5-12 pages) and twelve copies of a two page abstract to the chairman of the program committee. The cover page should include title, authors, and corresponding author: name, address, phone number, email address, and fax number (when available). The deadline for submissions is _May 1st, 1995_. The authors will be notified of acceptance for presentation at the conference by July 15th. The preliminary version of the full paper to be submitted to the Proceedings volume (LNCS Springer Verlag) should be available at the conference. Authors will be notified of the acceptance of their paper by _January 15th, 1996_. *Grants:* For young scientists living at least one year in EU-countries some grants are available from the HCM Euroconferences program of the EU. For more information please contact the _Chair:_ Prof. Dr. Hans Kleine B"uning (CSL '95), FB 17 Mathematik--Informatik Universit"at-GH Paderborn, 33095 Paderborn, Germany E-mail: csl95@uni-paderborn.de, Fax: +49 5251 60 3338 The final application should be sent not later then May 1st, 1995. See also the CSL'95 WWW page at URL: http://www.uni-paderborn.de/fachbereich/AG/agklbue/csl.95/start.html [C3] ================================================ AMAST Links 02 03 Int'l Conf. on Principles and Practice of Constraint Programming, CP'95 Cassis, France, September 19-22, 1995 *Update* of information in [AL0103C6] The full version of this Final Call for Papers is available in two forms: plain-text (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C3.? *Aims of the Conference* The area of constraint programming and constraint-based systems has recently developed an appreciable identity. The new area needs an international forum to compare the results and discuss the new lines of development. *Topics of Interest* a full list of topics for this conference can be found in the full version of this announcement mentioned above. *Conference Chair* Alain Colmerauer, Laboratoire d'Informatique de Marseille Faculte' des Sciences de Luminy 163, Avenue de Luminy, F-13288 Marseille CEDEX 9, France E-mail: alain.colmerauer@lim.univ-mrs.fr *Program Chair* Ugo Montanari, Dipartimento di Informatica, Universita' di Pisa Corso Italia, 40, I-56100 Pisa, Italy. E-mail: ugo@di.unipi.it *Paper Submissions* Authors are invited to submit full papers (in English, up to 18 pages, typeset 12 point) to the PC chairman. Simultaneous submission to other conferences or journals is not allowed. If ordinary mail is used, five copies of the paper should be sent by express or courier mail. Electronic submission is encouraged via e-mail, in the form of uuencoded compressed PostScript(tm) printable files sent to cp95@di.unipi.it; however a printed reference copy should be sent anyway by express or courier mail. Each submission, both by ordinary mail and by e-mail, should be accompanied by a separate message to cp95@di.unipi.it with a single postal and e-mail address for communication, complete title, author(s), affiliation(s) and 200 word abstract. *Important Dates* Submissions: March 15, 1995. Notification of acceptance: May 15, 1995 Camera-ready papers due: June 26, 1995. [C4] ================================================ AMAST Links 02 03 COCOON'95: Reminder and More Information First Annual International Computing and Combinatorics Conference *Update* of the Call for Papers in [AL0102C7] o COCOON'95 will be held Aug. 24-46, 1995, Xi'an, China. o The deadline for receiving the submissions is March 17, 1995. o In addition to the conference proceedings to be published in the Springer-Verlag LNCS series, _Theoretical Computer Science_ will publish a Special Issue of selected papers from COCOON'95, [C5] ================================================ AMAST Links 02 03 Graph Rewriting and Computation, SEGRAGRA'95 Joint COMPUGRAPH/SEMAGRAPH Workshop Volterra (Pisa), Italy, August 28 - September 1, 1995 The (LaTeX) full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C5.tex Graphs are a very natural medium to intuitively explain complex situations. Graph rewriting is a comprehensive framework where the transformation of a variety of different structures can be modelled and studied in an uniform way. In particular, Term Graph rewriting refers to techniques and theories for representing terms and term rewrite rules as graphs and graph rewrite rules. Graph rewriting and Term Graph rewriting is the focus of two Esprit Basic Research Working Groups, COMPUGRAPH II and SEMAGRAPH II. Both working groups have been active in the three year period 1992-95 and are the continuation of homonymous actions in the 1989-92 period. They have decided to organize their final workshop as a common initiative, with the aim of presenting a coherent, detailed account of the achieved results and their view of the state of the art in the field. *Topics of interest:* The topics of interest to SEGRAGRA'95 can be found in the full version of this announcement mentioned above. Relevant submissions from outside the COMPUGRAPH and SEMAGRAPH communities are actively sought, especially if they are applications. *Submissions:* Authors are invited to send extended abstracts (in English, up to 5 pages, typeset 12 point) to the PC chairman, at the address below. Prospective authors should consult the detailed submission information given in the full version of this announcement. *Program Chair:* Ugo Montanari, Dipartimento di Informatica, Universita` di Pisa, Corso Italia, 40, I-56100 Pisa, Italy. *Important Dates* Deadline for submissions: April 21, 1995 Notification of acceptance: June 5, 1995 Camera-ready version due: July 7, 1995 *Information* SEGRAGRA'95, Andrea Corradini, Dipartimento di Informatica Corso Italia, 40, I-56125 Pisa, Italy. Tel: +39 50 887266, Fax: +39 50 887226, Email: segragra@di.unipi.it [C6] ================================================ AMAST Links 02 03 Structural Information and Communication Complexity, SIROCCO '95 International Colloquium, Olympia, Greece, June 12 - 14, 1995 The full version of this Call for Papers is available in two forms: plain-text (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C6.? The 2nd in a series of annual colloquia on Structural Information and Communication Complexity will be held in the Olympic Academy, next to the archaeological site of Olympia (the location is picturesque and serene, and the facilities, situated among pine and cypress trees were designed to host the members of the Olympic Games Committee). Original papers are solicited on the interaction between structural information and communication complexity in parallel and distributed computing. *Topics of interest* include: o topological awareness o sense of direction o metric information (e.g. number of nodes, diameter,...) o implicit routing (e.g. compact, interval,...) o complexity of constructing structural information o complexity of maintaining structural information *Submission* The colloquium will comprise position papers (outlining open problems, research directions etc.), presentations of current research and group discussions. Authors should send 10 copies of an extended abstract of at most 15 double-spaced pages, clearly indicating the results achieved, their significance, and their relation to other work in the area, to: SIROCCO95; c/o Evangelos Kranakis, Carleton University, School of Computer Science, Ottawa, ON, K1S 5B6, Canada *Important Dates* The submission deadline for papers is April 7. Authors will be notified of acceptance by electronic mail on or before May 2, 1995. Authors should include their electronic address. *Registration* The registration fee is US$400. The price includes all expenses (lodging and meals; all events and the volume of proceedings). Depending on the availability of funds, scholarships will be given to a number of student participants and chosen by the program committee. *More information* is on the WWW at URL: http://www.scs.carleton.ca email: sirocco95@scs.carleton.ca phone: 613-788-4333, fax: 613-788-4334 [C7] ================================================ AMAST Links 02 03 Seventh IEEE Symposium on Parallel and Distributed Processing, SPDP'95 San Antonio, Texas, October 25-28, 1995 The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C7.txt The symposium will provide a forum for the presentation and exchange of current work in parallel and distributed processing including, but not limited to, the following areas: Artificial Intelligence; Computer Architecture; Data- & Knowledge-Base Systems; Distributed Computing; Image Processing; Interconnection Networks; Neural Networks; Operating Systems; Parallel Algorithms; Programming Languages; Scheduling & Resource Management; Applications. *Important Dates:* The Theory Track Program Committee has decided to extend the deadline for submission _to the Theory Track_ from Friday, March 17, 1995, to _Monday, April 3, 1995_. This is a *firm* deadline: 8 copies of submitted papers must reach the Theory Track Chair by that date. The System Track deadline is still _Monday, April 3, 1995_. Authors will be notified of the acceptance/rejection of papers by June 30, 1995. Final, camera-ready papers are due by July 31,1995. *Submissions:* Prospective authors should consult the detailed submission information in the full version mentioned above. *Workshops:* People wishing to organise a Full- or half-day workshop on specialized topics, can be held concurrently with SPDP, please send the following to the Workshops Chair: a detailed proposal, including workshop title, description of its scope and format, list of invited participants, and a summary vita of the workshop organizer(s). Workshop proposals are due March 17, 1995. _Theory Track Chair:_ Prof. Arnold L. Rosenberg University of Massachusetts, Computer Science Dep't A243 Lederle, Amherst, MA 01003-4610 E-mail: rsnbrg@cs.umass.edu, Phone:(413) 545-2743 _Systems Track Chair:_ Prof. Sartaj Sahni University of Florida, CIS Department CSE, 301 Gainesville, FL 32611 E-mail: sahni@cis.ufl.edu, Phone: (904) 392-1527 _Workshops Chair_ Prof. S. Lakshmivarahan, Univ. of Oklahoma School of CS, 200 Felgar Hall/Rm. 114 Norman, OK 73019 E-mail: varahan@constellation.ecn.uoknor.edu, Phone: (405) 325-4042 [C8] ================================================ AMAST Links 02 03 The Tbilisi Symposium on Language, Logic and Computation Tbilisi, Republic of Georgia, October 19-22, 1995 The full version of this First Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203C8.txt In order to foster communication between researchers in the Republic of Georgia and the international research community, the Georgian Centre for Language and Speech, based at the Tbilisi State University, will host an international symposium on language, logic and computation in 19-22, October 1995. The Tbilisi Symposium is anticipated to be the first of a regular series. *Topics of Interest:* A full, but not exhasutive, list of topics is given in the full version of this announcement. *Invited Speakers:* R. Cooper (Edinburgh); P. Gardenfors (Lund); A. Joshi (Philadelphia); H. Ono (Ishikawa); A. Preller (Montpelier); H. Uszkoreit (Saarbruecken) R. Wojcicki (Warszawa). *Submissions:* Papers not exceeding 10-pages should be submitted electronically or, if electronic submission is problematic, in hard copy. Electronic submissions should be in plain text, latex, or ready-to-print postscript. Papers submitted by postal mail should be accompanied by 3 additional copies. No fax submissions. Papers should be accompanied by a two-page abstract. Prospective authors should consult the full version of this announcement for detailed submission information. The abstracts will be collated together and will be made available to all symposium participants. Papers should be submitted to: The Tbilisi Symposium Human Communication Research Centre, University of Edinburgh 2 Buccleuch Place, Edinburgh, EH8 9LW, Scotland, UK E-mail: tbilisi@cogsci.ed.ac.uk Phone: +44 131 650 4667, Fax: +44 131 650 4587 *Important Dates:* Submission deadline is 31 May 1995. Notification of receipt will be mailed to the (contact) author. Notification of acceptance will be given by 15 July 1995. Final versions of papers must be received by 31 October 1995. [C9] ================================================ AMAST Links 02 03 Logic Colloquium 1995 Israel (Haifa or Jerusalem), August 9-17, 1995 *Topics:* The focus will be mainly but not exclusively on Set Theory, Model Theory, Recursion Theory and Proof Theory, and their mutual interaction and on Logical Aspects of Computer Science and Linguistics. *Invited Speakers:* _Tutorials_ K Compton (0-1 Laws in Finite Model Theory), S Goldwasser (Interactive Proofs), D Marker (Stability: The Spectrum Problem to Geometric Stability), T Slaman (Recent Advances in Recursion Theory). _Plenary lectures_ H Becker (Set Theory), P Blackburn (Logic and Linguistics), W Buchholz (Proof Theory), Z Chatzidakis (Model Theory), B Cooper (Recursion Theory), A Dawar (Finite Model Theory), R Downey (Recursion Theory), L Harrington (Recursion Theory), I Herzog (Model Theory), E Hrushovski (Model Theory), P King (Logic and Linguistics), J Krajicek (Proof Theory & Complexity), J Lynch (Finite Model Theory), P Maddy (Set Theory: 100 years), M Makkai (Categorical Model Theory), D Martin (Set Theory: 100 Years), G Moore (Set Theory: 100 Years), A Nies (Recursion Theory), M Rathjen (Proof Theory), M Pentus (Logic and Linguistics), Y Peterzil (Model Theory), A Pillay, (Model Theory), S Shelah (Set Theory), L Soukup (Set Theory), A Stolboushkin (Theoret. Computer Science), S Wainer (Proof Theory). *Submissions:* Participants intending to present a contributed paper are requested to submit a one page abstract, preferably by e-mail to: logic95-abstracts@cs.technion.ac.il by April 30, 1995 *Grants:* Limited number available for participants in the following categories: graduate students in logic, participants from countries with severe foreign currency problems, and individuals without any external financial support. *Further Information:* WWW URL: http://www.cs.technion.ac.il/~logic95 E-mail: logic95@cs.technion.ac.il (general information) logic95-registration@cs.technion.ac.il (prereg. and registration) logic95-grants@cs.technion.ac.il (grants) logic95-abstracts@cs.technion.ac.il (submitting abstracts) *Correspondence:* Logic Colloquium 95 Yvonne Sagi, Dep't of Computer Science Technion-Israel Institute of Technology, Haifa 32000, Israel [CA] ================================================ AMAST Links 02 03 International Static Analysis Symposium, SAS'95 Kelvin Conference Centre, Glasgow, 25--27 September 1995 The LaTeX full version of this Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203CA.tex Static Analysis is increasingly recognised as a fundamental tool for high performance implementations and verification systems of high-level programming languages. The last two decades have witnessed substantial developments in this area, ranging from theoretical frameworks to design and implementation of analysers and their applications in optimising compilers. The technical program will consist of invited lectures, presentations of refereed papers and software demonstrations. Contributions are welcome on all aspects of Analysis, including, but not limited to: Abstract Interpretation; Optimising Compilers; Applications; Specific Analyses; Complexity; Theoretical Frameworks; Experimental Evaluation; Verification Systems; Fixpoint Algorithms; Type Inference; Partial Evaluation; Abstract Domains. *Important Dates* Subm: 15 April; Notif: 10 June; Final Vers: 3 July. *Contact and Submission address* Email: sas-95@cl.cam.ac.uk Tel: +44 1223 334621; Fax: +44 1223 334678 Post: Alan Mycroft, Computer Laboratory, New Museums Site Pembroke Street Cambridge, CB2 3QG, United Kingdom. Submissions can address any programming paradigm including concurrent, constraint, functional, imperative, logic and object oriented programming. Survey papers which present aspects of the above topics with a new coherence are also welcomed. Papers must be written in English, max 15 pages (excluding references and figures) and must contain a cover page including the following: a 200 word abstract, keywords, and postal and e-mail addresses as well as phone numbers and fax numbers of one of the authors. Submissions should be sent to the following addresses: either e-mail a WWW URL descriptor for your submission; or e-mail a Postscript or (uuencoded) DVI file; or send six paper copies. (Electronic submission is prefered but do ensure that your submission is self-contained and prints on A4 paper.) Also e-mail an ascii or Latex version of the cover page if possible. Information on SAS'95 is also on the WWW at URL: http://www.cl.cam.ac.uk/users/am/sas-95 [CB] ================================================ AMAST Links 02 03 1995 IEEE Symposium on Foundations of Computer Science, FOCS'95 Milwaukee, October 23-25, 1995 The full version of this Call for Papers is available in two forms: _plain-text_ (?=txt) and _LaTeX_ (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203cB.? The Annual Symposium on Foundations of Computer Science (FOCS), on Mathematical Foundations of Computing, will be held in Milwaukee on Oct. 23-25, 1995. Original research on theoretical aspects of computer science are sought. Typical but not exclusive topics of interest include: algorithms and data structures, complexity theory, computational algebra and geometry, computational biology, cryptography, databases, machine learning, algorithmic graph theory, applications of logic, parallel and distributed computation, probabilistic computations, computer architectures, and robotics. *Abstract submission:* Authors should send sixteen (16) copies of an extended abstract (not a full paper) to: Prabhakar Raghavan, FOCS 95, Program Chair 36-249 IBM T.J. Watson Research Center Route 134, Box 218 Yorktown Heights, NY 10598, USA Prospective authors should consult the detailed submission information in the full version mentioned above or on the WWW at URL: http://www.cs.uwm.edu/public/focs95/index.html *Important Dates:* Notification: The abstract (whether sent by hard copy or by electronic submission) must be received by 23:59 EST April 26, 1995 (or postmarked by April 20, 1995 and sent via airmail or express mail). This is a firm deadline. Authors will be notified of acceptance or rejection by a letter mailed by June 30, 1995. A final copy is required by August 10, 1995. This is again a firm deadline. *Information* about local arrangements can be obtained from the Local Arrangements Chairs: Aditi Dhagat and Rene Peralta Computer Science Department, P.O. Box 784 University of Wisconsin, Milwaukee WI, 53201 [CC] ================================================ AMAST Links 02 03 Isabelle Users Workshop Cambridge, UK, 18-20 September 1995 This workshop is to allow Isabelle users to exchange techniques and results. Both finished work and work in progress can be reported. There will be a programme of short talks and possibly demonstrations. A printed proceedings will be given out to workshop participants, provided there are enough papers to justify this. There will be no formal refereeing; within reason, all talks and papers will be accepted. There will also be time for informal discussions. Administration will be minimal in order to keep the costs down. However, we hope to be able to arrange College accommodation and meals for participants, at a cost of less than #200 (UK); as an alternative, we can supply a list of hotels. There will be a small registration fee. For information on how to get to the Computer Laboratory, please see the WWW at URL: http://www.cl.cam.ac.uk/site-maps/howtogethere.html Those people interested in attending should give a notice of this to L. C. Paulson at the address below. Those people intending to give a talk or demo, or submit a paper for the proceedings, should send the title and abstract to: Lawrence C Paulson, University Lecturer Computer Laboratory, University of Cambridge Pembroke Street, Cambridge CB2 3QG, England Tel: +44(0)21223 334623 Fax: +44(0)1223 334678 E-mail: Larry.Paulson@cl.cam.ac.uk Comments on how the workshop should be organised are welcome. [CD] ================================================ AMAST Links 02 03 X Latin American Symposium on Mathematical Logic Bogota, Colombia, July 24-29, 1995 The Tenth Latin American Symposium on Mathematical Logic will be held in Bogota from July 24 to 29, 1995, sponsored by the Universidad de los Andes, the Universidad Nacional de Colombia and the Association for Symbolic Logic. The main areas of the Symposium will be: Model theory and its applications, Set theory and its applications, Algebraic logic and non-classical logics, Applications of logic to computer science, Mathematical Logic in science and philosophy. *Conference:* The following is a partial list of invited speakers who have agreed to participate in the meeting: Andreas Blass (Ann Arbor), Joan Bagaria (Barcelona), Willem Blok (Chicago), Walter Carnielli (Campinas), Joerg Flum (Freiburg), Sy Friedman (Boston), Lauri Hella (Helsinki), Ward Henson (Urbana), Jerome Keisler (Madison), Michal Krynicki (Warsaw), Kenneth Kunen (Madison) E.G.K. Lopez-Escobar (College Park), Marcin Mostowski (Warsaw), Daniele Mundici (Milano), Juha Oikkonen (Helsinki), Anand Pillay (Notre Dame), Gonzalo Reyes (Montreal), A.M. Sette (Campinas). *Short Courses:* July 17-22. In the week previous to the meeting, a workshop will be held, centered around four courses given by A. Blass (Cardinal Characteristics of the Continuum), W. Blok (Algebraic Logic), J. Flum (Finite Model Theory), and A. Pillay (Model Theory of Algebra). *Dates:* Abstracts of contributed papers will be received until April 15, 1995; decisions on their acceptance will be communicated by May 15. *Program Committee:* I M L D'Ottaviano (Univ. Estadual de Campinas), R Lewin (Univ. Catolica de Chile), C Di Prisco (Inst. Venezolano de Investigaciones Cientificas), R Cignoli (Univ. de Buenos Aires), X Caicedo, Chair (Univ. de los Andes, Bogota). *Organizing Committee:* L J Corredor, S Fajardo, C Montenegro (Univ. de los Andes), J M Munoz, R de Castro, C H Sanchez, F Zalamea (Univ. Nacional de Colombia). *Registration and Further Information:* Secretary X-SLALM Departamento de Matematicas, Universidad de los Andes Apartado Aereo 4976, Bogota, Colombia e-mail: xslalm@cdcnet.uniandes.edu.co Tel. (571) 2838885, Fax (571) 2841890 [CE] ================================================ AMAST Links 02 03 4th Int'l Conference on Information and Knowledge Management, CIKM'95 November 8-11, 1995, Baltimore, Maryland, USA The full version of this Prel. Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203CE.txt Additional information on CIKM'95 is available on the WWW at URL: http://www.cs.umanitoba.ca/~randal/CIKM95.html CIKM'95 will bring together leading researchers and developers in a wide variety of scientific areas, with a common interest in improving information and knowledge management technologies. Its objective is to provide a forum for the discussion and dissemination of recent advances in the area, and to foster close international collaboration between the database, information retrieval, and artificial intelligence cmmunities. *Submission* Authors are invited to submit complete and original papers. Papers that may be submitted include those that have not previously been published in another forum, or are not currently being published or reviewed by another journal or conference. All submitted papers will be refereed for quality, correctness, originality and relevance. All accepted papers will be published in the conference proceedings. In addition, special issues of journals containing extended versions of outstanding papers from the conference have been planned. Prospective authors should consult the full version of this announcement for detailed submission information and scope of the conference. *Workshops* An important part of the conference is the workshop program, which focuses on timely research challenges and initiatives. Proposals are solicited for organizing workshops and tutorials. The details of the workshop organization are given in the full version of this announcement at the URL above. *Further Information* about the conference (as opposed to paper submissions) please contact Dr Charles Nicholas at nicholas@cs.umbc.edu or Tel: (410) 455-2594. *Important Dates* Paper submission deadline: May 1, 1995 Notification of acceptance: June 28, 1995 Camera ready papers due: July 31, 1995 [CF] ================================================ AMAST Links 02 03 Foundations of Software Technology and Theoretical Computer Science 15th Conference, Bangalore, India, December 18-20, 1995 The full version of this Call for Papers is available in two forms, plain-text (?=txt) and LaTeX (?=tex) respectively at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203CF.? *Scope:* Authors are invited to submit papers presenting original and unpublished research on theoretical aspects of Computer Science. Typical areas include (but are not limited to): Computational Complexity; Design and Analysis of Algorithms (including Parallel, Distributed, Probabilistic and Randomized Algorithms); Data Structures; Learning Theory; Computational Geometry; Temporal and Modal Logics of Programs; Rewrite Systems; Type Theory; Theory of Concurrency (including Reactive, Real-Time and Hybrid Systems); Theory of Logic Programming, Object-oriented, Functional and Constraints-based Programming; Formal Concepts in Programming Languages; Specification and Verification Methodologies. *Submissions:* Authors are invited to send *six* copies of a draft of a full paper or an extended abstract. It will not be possible to accept submissions by email. Papers should be limited to 4500 words (about 12 pages). If authors believe that more details are necessary, they may include a clearly marked appendix which will be read at the discretion of the Programme Committee. Each paper should also contain a short abstract of approximately 200 words. If available, e-mail addresses and fax numbers of the authors should also be included. Send papers to: P.S. Thiagarajan, FST & TCS 14, pst@imsc.ernet.in School of Mathematics, SPIC Science Foundation 92 G.N. Chetty Road, T. Nagar, Madras 600 017, India Alternatively e-mail: pst@ssf.ernet.in or fax: +91-44-825 6842. *Dates:* Subm: 15 May, Notif: 4 August, Final: 8 September 1995. *Further Information* V. Chandru, Computer Science & Automation Indian Institute of Science, Bangalore 560 012, INDIA. Fax: +91-80-334 1683, E-mail: fsttcs@csa.iisc.ernet.in [CG] ================================================ AMAST Links 02 03 Neural Information Processing Systems - Natural and Synthetic Denver, Colorado, Monday, Nov. 27 - Saturday, Dec. 2, 1995 The full version of this Call for Papers is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203CG.txt This is an interdisciplinary conference which brings together neuroscientists, engineers, computer scientists, cognitive scientists, physicists, and mathematicians interested in all aspects of neural processing and computation. The conference will include invited talks, and oral and poster presentations of refereed papers. There will also be one day of tutorial presentations (Nov. 27) preceding the regular session, and two days of focused workshops will follow at a nearby ski area (Dec. 1-2). Major categories for paper submssion are: Neuroscience; Theory; Implementation; Algorithms and Architectures; Visual Processing; Speech, Handwriting and Signal Processing; Applications; Cognitive Science & AI; Control, Navigation, and Planning; *Review Criteria:* All papers will be refereed on the basis of technical quality, novelty, significance, and clarity. Submissions should contain new results that have not been published previously. *Submission:* Send six copies of papers to the address below; electronic or Fax submission is not acceptable. Include one additional copy of the abstract only, to be used for preparation of the abstracts booklet distributed at the meeting. Submissions mailed first-class from within the US or Canada, or sent from overseas via Federal Express / Airborne / DHL or similar carrier must be *postmarked* by May 20, 1995. All other submissions must *arrive* by this date. Mail submissions to: Michael Mozer, NIPS*95 Program Chair Department of Computer Science, University of Colorado Colorado Avenue and Regent Drive, Boulder, CO 80309-0430, USA Prospective authors should consult the detailed submission information in the full version of this announcement mentioned above. *Further Information* NIPS'95 Registration, nips95@mines.colorado.edu Dep't of Mathematical & Computer Sciences, Colorado School of Mines Golden, CO 80401 USA. Fax: (303) 273-3875. [J1] ================================================ AMAST Links 02 03 Two openings at Honeywell Technology Centre Minneapolis, MN, USA The Systems and Software Technology Area at the Honeywell Technology Center in Minneapolis has two openings for Artificial Intelligence Interns with interest in applying AI in complex systems for real-time control. Special expertise in neural networks, fuzzy logic, temporal reasoning, decision analysis, agents, user/system interaction modeling, or a related field is preferred. Pre-Doctoral Internship applicants should have completed all coursework for a Ph.D. or equivalent in Cognitive Psychology, Computer Science, or a related field. Post-Doctoral Internship applicants are also welcome. The Honeywell Technology Center has sponsored a formal internship program for over 15 years; the program offers competitive salary and benefits over a 9-12 month period. The program is very competitive; typically, twenty to fifty applications are received for each position. The Systems and Software Technology Area develops and transfers systems technologies to help Honeywell Divisions better support their customers in Home and Building Control, Industrial Automation and Control, and Space and Aviation Control application domains. Honeywell is an equal opportunity employer. For more information, contact: Terri Sheehan Artificial Intelligence Internship Honeywell Technology Center 3660 Technology Drive Minneapolis, MN 55418 E-mail: sheehan_terri@htc.honeywell.com [J2] ================================================ AMAST Links 02 03 Theory Postdoc Opening Royal Institute of Technology, Stockholm, SWEDEN We are looking for a postdoc for the academic year 1995/96 with possible extension for a second year (depending on achievements and success of grant applications). The theory group at Royal Institute of Technology consists of 2 full professors (Arnborg, Hastad), 3 researchers (Goldmann, Kann, Lagergren) and a number of graduate students. Our interests include: o Complexity theory (in particular circuit complexity) o Approximation algorithms o Graph algorithms o Cryptography o Computational biology An applicant should be a recent Ph. D. of high international caliber who is interested in any of the above areas. For more information contact either Johan Hestad (johanh@nada.kth.se) or Stefan Arnborg (stefan@nada.kth.se). [J3] ================================================ AMAST Links 02 03 Postdoctoral Position at XEROX PARC Palo Alto, CA, USA The Theoretical Computer Science and Computational Methods Area of the Xerox Palo Alto Research Center is recruiting for a postdoctoral position in algorithms for the 1995-1996 academic year. The theory group at PARC is part of the larger Computer Science Laboratory, well known for over twenty years of influential basic research in computer systems. The theory group itself specializes in theory inspired by practical problems arising in graphics, physical simulation and modeling, and information retrieval. Ongoing research includes: work in triangulation and mesh generation, approximate searching, graph algorithms, partitioning and layout for parallel computation, sparse matrix algorithms, and approximation algorithms. The unifying theme of our work is its emphasis on algorithms that find provably good solutions to hard problems arising in practice. The postdoc will be expected to interact closely with the regular area members, but will also be free to pursue his or her own research interests. To apply please submit: a resume; a summary of research interests; and reprints of publications based on thesis and other research. Applicants are also responsible for requesting that three or more letters of reference be sent directly to us. To be assured of full consideration, all material including reference letters must arrive by March 17, 1995. Direct all material to: John R. Gilbert Xerox Palo Alto Research Center 3333 Coyote Hill Road, Palo Alto, CA 94304 E-mail: gilbert@parc.xerox.com; fax: 415-812-4471 Applications by email will be accepted. Applications will be acknowledged, by email if possible, and each applicant will be notified individually as soon as a decision has been reached on the application. [J4] ================================================ AMAST Links 02 03 Associate Professorship in Computer Science Department of Computer Science, University of Aarhus, DK Applications are invited for a position of Associate Professor at the Department of Computer Science, University of Aarhus. The position is open from May 1995 and the annual salary is in the range DKK 300,000-380,000 including contribution to pension fund. The position is to be filled to strengthen the Department's activities in the computer science research areas of formal semantics and logic. In particular, applicants with a broad research and teaching background in analysis, verification, and construction of computer systems and programs are sought. Applications should include a curriculum vitae giving evidence on which the evaluation of the applicant's scientific and teaching qualifications can be based, and a complete list of publications together with three copies of each of those publications which the applicant selects as the most relevant for the application. Other supportive material should also be submitted in three copies. The selection committee may include further material from the list of publications in its evaluation of the applicant. In that case the applicant should, upon request, submit the material to the selection committee. The selection committee's written evaluation of the applicants will be sent in full to all applicants. Applications marked 212/5-03 should be addressed to The Faculty of Natural Sciences, University of Aarhus Ny Munkegade, Building 520, DK-8000 Aarhus C, Denmark The deadline for the receipt of all application material is March 16, 1995, at 12.00. For more information, please, contact Karen K. Moller, e-mail: kkmoller@daimi.aau.dk phone: +45 8942 3188 direct: +45 8942 3262. Fax: +45 8942 3255 [J5] ================================================ AMAST Links 02 03 Research Fellowships Department of Computer Science Queen Mary & Westfield College, University of London As an important part of our strategy to accelerate research activity in this highly-rated research department we wish to appoint a small number of full-time Research Fellows in Computer Science. The fellowships will be of one to two years duration and are aimed at experienced researchers who would benefit from collaborating with staff at QMW in a lively and well resourced research setting. The department has strong well resourced research groups in several mainstream areas of computer science including artificial intelligence; computer graphics and virtual reality; distributed & parallel systems; human computer interaction, programming and the theory of computation. Applicants for an Advanced Fellowship (Ref: 95034) should have a PhD in a relevant area of computer science together with a minimum of two years research experience and sound publication record providing evidence of potential to lead research. Salary will be in the range 16,075 - 23,087 pounds. Applicants for a Senior Research Fellowship (Ref: 95035) must have a minimum of five years research experience since obtaining their PhD in a relevant area of computer science together with an excellent publication record providing evidence of a significant contribution to their chosen area of computer science and proven ability to lead research. Salary will be in the range 26511 - 32665 pounds. For informal discussions contact Mel Slater (mel@dcs.qmw.ac.uk) (0171 975 52..). Further information about the department can be found on the WWW at URL: http://www.dcs.qmw.ac.uk/ For an application form and further details, please telephone our 24 hour Recruitment Line on 0171 975 5171, quoting the relevant Reference Number. Completed applications forms should be returned by 14th March 1995 to the Recruitment Coordinator, Personnel Office Queen Mary and Westfield College, Mile End Road, London E1 4NS This announcement is also available on WWW at URL: http://www.dcs.qmw.ac.uk/~mel/Admin/fellowad.html [J6] ================================================ AMAST Links 02 03 Postgraduate Bursaries in Theoretical Computer Science Computing Laboratory, University of Kent, UK The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203J6.txt The Computing Laboratory at the University of Kent has available a number of bursaries for PhD students. Applicants must hold a good first degree in Computer Science or a closely related subject. The bursaries cover tuition fees (at the EC rate) and provide living expenses at the current research council rates. Bursaries are tenable for one year in the first instance but, subject to satisfactory research performance, will be extended for a further two years. We are offering Ph.D. studentships in the general area of Theoretical Computer Science. Applicants should have a strong background in Computer Science or Mathematics. Applications for the following projects are particularly encouraged (see the full version mentioned above for details about the projects, including contact addresses): o Computing with Exact Real Numbers o Program Development in Constructive Type Theories o Abstract Interpretation for Concurrent Constraint Program The Computing Laboratory has international reputation for computing research. There are approximately forty people on the research staff, with a similar number providing support and computing services. Students are normally expected to present their work in progress to a wider audience a number of times during their studies, and are encouraged to attend appropriate conferences and seminars. Postgraduate travel funds are available. Recipients of the awards are required to perform no more than 60 hours teaching per term (averaged over the year) for which there is no further remuneration. Research students have full access to the computing facilities of the laboratory. In addition, each postgraduate is equipped with a personal computer or X-terminal allowing direct access to central computing. For further information regarding application please write to: Postgraduate Bursaries, Computing Laboratory, University of Kent Canterbury, Kent, CT2 7NF, or e-mail: S.A.Hill@ukc.ac.uk On the WWW further information can be obtained from our entry at URL: http://www.ukc.ac.uk/computer_science [J7] ================================================ AMAST Links 02 03 Research Studentships in Computer Science University of East Anglia, Norwich, UK Applications are invited from graduates with a first or upper second class degree in Computer Science for three research studentships, as outlined below: 1. Preference for one studentship will be given to candidates whose interests are in the area of Declarative Systems, for example, novel techniques for implementation of concurrent programme languages on sequential and parallel machines. 2. A second studentship is a CASE award with Norwich Union investigating the use of Object Oriented techniques in information systems. 3. A third studentship is associated with a group researching in the broad area of the analysis of data from human-computer interaction. The studentships for 1) and 2) above are available immediately and candidates must be able to start before April 1995. Studentship 3) will be available from April 1995. For more information contact the Head of the Computing Sector, Dr R Dowsing tel [01603] 593102, email rdd@sys.uea.ac.uk [L1] ================================================ AMAST Links 02 03 Book: Algebraic Specification Techniques & Tools for Softw. Development The ACT Approach Ingo Classen, Hartmut Ehrig, Dietmar Wolz AMAST Series in Computing, Volume 1, 1993, ISBN 981-02-1227-5 World Scientific, Singapore. 254 pages, price: US$ 38. Order information: see [AL0203S1]. The ACT approach is a conceptual frame for software development based on algebraic specification techniques. It is intended to support the software development process in several stages and to enforce the construction of software systems with emphasis on correctness and compositionality. The first chapter provides an informal introduction to algebraic specification and the ACT approach as a formal method for software development. In the main part of the book algebraic specification techniques for data types and modular software systems are introduced and the specification language ACT ONE and the ACT environment are presented as developed at the Technical University of Berlin in several national and international research and development projects. Many expressive examples and one larger case study illustrate the provided concepts and techniques, leading to an easily accessible and application-oriented contribution to the use of algebraic methods in software development based on solid theoretical foundations. *Authors' Address:* Technische Universit"at Berlin, Sekr. FR 6-1, FB 13, Informatik Franklinstrasse 28/29, D-10587 Berlin, Germany e-mail: @cs.tu-berlin.de [L2] ================================================ AMAST Links 02 03 Book: Theories and Experiences for Real-Time System Development Teodor Rus & Charles Rattray (Editors) AMAST Series in Computing, Volume 2, 1994, ISBN 981-02-1923-7 World Scientific, Singapore. 444 pages, price: US$ 86. Order information: see [AL0203S1]. _More info_ at URL: ftp://cs.uiowa.edu/pub/rus/Books/realtime.ps To consider the AMAST perspective on real-time systems, a first AMAST Workshop on Real-Time Systems was held in Iowa City, in November 1993. All the speakers were invited. All the authors had the opportunity to refine their papers as a result of the lively discussions that took place during the Workshop. A tangible product of this procedure is the present volume. The contents and authors are listed below. 1. Real-time system = discrete system + clock variables (R Alur & TA Henzinger) 2. Real-time CSP (J Davies & S Schneider) 3. Visual tools for verifying real-time systems (J S Ostroff) 4. Designing supervisors for real-time systems (D Ionescu) 5. Real-time symbolic model-checking (SV Campos & EM Clarke) 6. Verification of an audio control protocol (D Bosscher, I Pollak & F Vaandrager) 7. Approximations for verif. timing properties (H Wong-Toi & DL Dill) 8. A Timed Full LOTOS with Time/Action Tree Semantics (T Bolognesi & F Lucidi) 9. A Timed LOTOS extension (J Quemada, C Miguel, D deFrutos & L Llana) 10. Status-oriented telephone service spec. (B Stepien & L Logrippo) 11. Experimenting with LOTOS in the aerospace industry (H Garavel & RP Hautbois) 12. Performance analysis and true concurrency semantics (E Brinksma, JP Katoen, R Langerak & D Latella) 13. State machines, temporal logic and alg. data models (A Gabrielian) 14. An experiment in developing real-time systems using Mec (D Begay, J Dormoy & P Felix) [L3] ================================================ AMAST Links 02 03 Book: Construction and analysis of transition systems with MEC A. Arnold, D. Begay, P. Crubille' AMAST Series in Computing, Volume 3, 1995, ISBN 981-02-1922-9 World Scientific, Singapore. 192 pages, price: US$ 42. Order information: see [AL0203S1]. This book explains how to model and to verify systems of processes using the mathematical formalism of synchronized product of transition systems and presents several examples of modeling and verification covering various domains: games, industrial processes, communication protocols, etc. These examples are worked out using the "MEC" software tool. This book is also intended to be an introduction to this tool which is described in full details. *Authors' Address:* LaBRI, Universite' Bordeaux I 351 cours de la Liberation, F-33405 Talence, France e-mail: @labri.u-bordeaux.fr [L4] ================================================ AMAST Links 02 03 Book: System Software and Software Systems: Concepts and Methodology T. Rus and D. Rus Vol 1 : Systems Methodology for Software, ISBN 981-02-1254-2, pr. US 38 Vol 2 : Execution Support Environment, ISBN 981-02-1255-0, price US 51 World Scientific, Singapore, 1995. *Order information*: contact one of the Publisher's offices (their addresses are listed in [AL0203S1]) *More information* is available on the WWW: Volume 1 : ftp://cs.uiowa.edu/pub/rus/Books/sysoft1.ps Volume 2 : ftp://cs.uiowa.edu/pub/rus/Books/sysoft2.ps _System Software and Software Systems: Concepts and Methodology_ is a work intended to offer a systematic treatment of the theory and practice of designing and implementing system software. This is achieved by structuring the hardware and software resources of a computer system as mathematical systems. The system software is defined as the collection of programs and documents that offer services to the users of a computer installation in order to make it convenient and efficient to use. There are two major classes of users of a computer installation: 1. processes executing programs on processors and 2. programmers developing their programs. Thus, the components of the system software are classified as the execution support environment providing services to program execution and programming support environment providing services to program development. Volume 1, _Systems Methodology for Software_, second edition, February 1995, presents the methodology used for this structuring. Volume 2, _Execution Support Environment_, December 1994, is dedicated to the design and implementation of the software tools managing program execution. *Authors' Address:* T. Rus, Department of Computer Science, The University of Iowa Iowa City, IA 52242, USA. E-mail: rus@cs.uiowa.edu D. Rus, Department of Computer Science, Dartmouth College Hanover, New Hampshire 03755-3510, USA. E-mail: rus@cs.dartmouth.edu [L5] ================================================ AMAST Links 02 03 Performance-Oriented Specification of Communication Protocols and Verification of Deterministic Bounds of their QoS Characteristics PhD-Thesis, Technical University Berlin, Nov. 1994, by Ina Schieferdecker The need for performance considerations at each level of the communication protocol development process arose and were forced by the advances in high-speed networks and the evolution of new communication services with their rigorous Quality-of-Service (QoS) requirements. This dissertation presents an approach for the QoS-oriented design of communication protocols using formal specifications. It includes a specification technique for the performance-oriented behavior description of communication protocols, a real-time temporal logic for the description of deterministic bounds, which are a special kind of QoS requirements, and decision procedures for verifying the fulfilment of deterministic bounds by a given communication protocol. The developed performance-oriented specification technique LotoTis extends LOTOS --- a standardized specification technique based on process algebras --- by means of quantified time, quantified parallelism, quantified nondeterminism, and monitoring of system execution. The central concept are structured actions which allow very concise and elegant description of performance-oriented behavior. The presented approach uses a real-time temporal logic called AMTL, the action-based version of MTL, for the description of deterministic bounds of performance characteristics. Deterministic bounds can be proven to be fulfilled by a given LotoTis protocol specification provided the specification possesses only a finite --- but possibly cyclic --- state space. The implementation of the developed verification method is conceived, which allows us to investigate realistic communication protocols. Author's WWW page at URL: http://www.fokus.gmd.de/htbin/info/step/ina [L6] ================================================ AMAST Links 02 03 Proceedings of the 6th Nordic Workshop on Programming Theory (Aarhus, Denmark, 17--19 October, 1994) Uffe H. Engberg, Kim G. Larsen and Peter D. Mosses (editors) The Nordic Workshop on Programming Theory brings together researchers from the Nordic and Baltic countries, in order to improve mutual contacts and collaboration. The invited speakers, however, generally come from non-Nordic/Baltic countries. The 6th Nordic Workshop attracted 63 participants. The workshop had three invited talks and 41 submitted talks. This proceedings contains full papers or extended abstracts of the talks. For completeness we have included short abstracts for the few remaining talks. Copies of the Proceedings and individual papers in A4 format are electronically accessible through WWW at URL: http://www.brics.aau.dk/BRICS/NS/94/6/BRICS-NS-94-6/ [L7] ================================================ AMAST Links 02 03 Proceedings of the C.A.E.N. Workshop September, 1994 This is to announce that the proceedings of the C.A.E.N. workshop, which was held in September 1994, will soon be available to everybody who is interested. Les actes des journees CAEN 94 (Categories, Algebres, Esquisses, Neo-esquisses) seront disponibles en principe a la fin du mois de fevrier 1995. Ils comprennent des contributions originales, soigneusement relues et corrigees, des auteurs suivants: Dehornoy, Porter, Duval et Reynaud, Lafont, Johnstone, Dreckmann, Van de Wiele, Gerner et Guitart, Guitart, Damphousse et Guitart, Gordon et Power, Senechaud, Lellahi, Bourn, Ageron, Burroni et Penon, Wehrung, Brown, Mathieu, Lair, Retore, Stell. La plupart de ces articles sont en francais, les autres sont en anglais; ils totalisent 142 pages. Le volume d'actes sera envoye gratuitement a chaque personne qui en fait la demande, ceci dans la limite du tirage prevu (un seul exemplaire par personne ou bibliotheque). Il suffit pour cela de m'envoyer votre commande par la poste, en indiquant clairement l'adresse a laquelle il devra etre expedie. Les commandes faites par courrier electronique ne seront pas prises en compte. Les auteurs n'ont bien evidemment pas a passer commande. Pierre Ageron Departement de Mathematiques Universite de Caen F-14032 Caen Cedex France [L8] ================================================ AMAST Links 02 03 Higher-dimensional algebra and topological quantum field theory by John Baez and James Dolan The study of topological quantum field theories increasingly relies upon concepts from higher-dimensional algebra such as n-categories and n-vector spaces. We review progress towards a definition of n-category suited for this purpose, and outline a program in which n-dimensional TQFTs are to be described as n-category representations. First we describe a `suspension' operation on n-categories, and hypothesize that the k-fold suspension of a weak n-category stabilizes for k greater than or equal to n+2. We give evidence for this hypothesis and describe its relation to stable homotopy theory. We then propose a description of n-dimensional unitary extended TQFTs as weak n-functors from the `free stable weak n-category with duals on one object' to the n-category of `n-Hilbert spaces'. We conclude by describing n-categorical generalizations of deformation quantization and the quantum double construction. This paper is now available by anonymous ftp as the file with URL: ftp://math.ucr.edu/baez/tqft.tex It is in LaTeX, but to LaTeX it you also need the files auxdefs.sty and diagram.sty, which are also in the directory baez at math.ucr.edu. [L9] ================================================ AMAST Links 02 03 Light Linear Logic and other papers by Jean-Yves Girard The paper is available through anonymous ftp in directory at URL: ftp://lmd.univ-mrs.fr/pub/girard The files are LLL.dvi.Z or LLL.ps.Z. It basically contains the detailed proofs that LLL normalizes in polytime, and that polytime functions can be represented in LLL. ELL and light set-theory/light arithmetic are only sketched. The main reference of this paper "Proof-Nets: The Parallel Syntax for Proof-Theory" is also available at the same source in the files Proofnets.dvi.Z or Proofnets.ps.Z. Finally a general survey paper "Linear Logic: Its Syntax and Semantics" can be obtained at the same source in the files Synsem.dvi.Z or Synsem.ps.Z. [LA] ================================================ AMAST Links 02 03 What is a Categorical Model of Intuitionistic Linear Logic? by G.M. Bierman *Abstract:* This paper re-addresses the old problem of providing a categorical model for Intuitionistic Linear Logic (ILL). In particular we compare the now standard model proposed by Seely to the lesser known one proposed by Benton, Bierman, Hyland and de Paiva. Surprisingly we find that Seely's model is unsound in that it does not preserve equality of proofs. We shall propose how to adapt Seely's definition so as to correct this problem and consider how this compares with the model due to Benton et al. This paper is due to appear in the Proceedings of Conference on Typed lambda calculus and Applications, LNCS, April 1995. An earlier version appeared as University of Cambridge Computer Laboratory Technical Report 333, April 1994. This version is available by anonymous ftp in directory at URL: ftp://theory.doc.ic.ac.uk/theory/imported/BiermanGM/ [LB] ================================================ AMAST Links 02 03 A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Preliminary Report) by P.N. Benton, CUCL, Sep. 1994, 352 This paper addresses some of the issues involved in categorical models of intuitionistic linear logic. In particular, one of the contributions of the paper is the result that the notion of model given in earlier papers (Benton, Bierman, de Paiva, Hyland) is equivalent to having a symmetric monoidal adjunction between a SMCC and a CCC. Thus, assuming one believes that logical operations should behave well with respect to contexts, our notion of model is just what one obtains by assuming that there is a way to embed ordinary IL into ILL. In other words, we have a semantic reconstruction of the ! operation. The paper is available via the WWW at URL: http://www.cl.cam.ac.uk/users/pnb/mixed3.dvi.Z Abstract: Intuitionistic linear logic regains the expressive power of intuitionistic logic through the ! (`of course') modality. Benton, Bierman, Hyland and de Paiva have given a term assignment system for ILL and an associated notion of categorical model in which the ! modality is modelled by a comonad satisfying certain extra conditions. Ordinary intuitionistic logic is then modelled in a cartesian closed category which arises as a full subcategory of the category of coalgebras for the comonad. This paper attempts to explain the connection between ILL and IL more directly and symmetrically by giving a logic, term calculus and categorical model for a system in which the linear and non-linear worlds exist on an equal footing, with operations allowing one to pass in both directions. We start from the categorical model of ILL given by Benton, Bierman, Hyland and de Paiva and show that this is equivalent to having a symmetric monoidal adjunction between a symmetric monoidal closed category and a cartesian closed category. We then derive both a sequent calculus and a natural deduction presentation of the logic corresponding to the new notion of model. [LC] ================================================ AMAST Links 02 03 Higher-Order Logic Programming by Gopalan Nadathur and Dale Miller "Higher-Order Logic Programming" can be obtained as an either DVI (?=dvi) or Postscript (?=ps) file respectively at URL: ftp://cs.duke.edu/dist/papers/lprolog/holp.?.Z You can also use the WWW page URL: http://www.cis.upenn.edu/~dale/recent_papers.html and trace the relevant links. This paper, which is to be a chapter in a handbook, provides an exposition of the notion of higher-order logic programming. It begins with an informal consideration of the nature of a higher-order extension to usual logic programming languages. Such an extension is then presented formally by outlining a suitable higher-order logic --- Church's simple theory of types --- and by describing a version of Horn clauses within this logic. Various proof-theoretic and computational properties of these higher-order Horn clauses that are relevant to their use in programming are observed. These observations eventually permit the description of an actual higher-order logic programming language. The applications of this language are examined. It is shown, first of all, that the language supports the forms of higher-order programming that are familiar from other programming paradigms. The true novelty of the language, however, is that it permits typed lambda terms to be used as data structures. This feature leads to several important applications for the language in the realm of meta-programming. Examples that bring out this facet of the language are presented. A complete exploitation of this meta-programming capability requires certain additional abstraction mechanisms to be present in the language. This issue is discussed, the logic of hereditary Harrop formulas is presented as a means for realizing the needed strengthening of the language, and the virtues of the features arising out the extension to the logic are illustrated. [LD] ================================================ AMAST Links 02 03 A First Course in Category Theory by Jaap van Ooosten Jaap van Oosten has written a first course in category theory which is intende to contain what's presumed knowledge in not too specialized papers and theses (in computer science). It's 75 pages long. The synopsis is: 1. Categories and functors. Definitions and examples. Duality. 2. Natural transformations. Exponents in Cat. Yoneda lemma. Equivalent categories; Set^op equivalent to Complete Atomic Boolean Algebras. 3. Limits and Colimits. Functors preserving (reflecting) them. (Finitely) complete categories. Limits by products and equalizers. 4. A little categorical logic. Regular categories, regular epi-mono factorization, subobjects. Interpretation of coherent logic in regular categories. Expressing categorical facts in the logic. Example of \Omega -valued sets for a frame \Omega. 5. Adjunctions. Examples. (Co)limits as adjoints. Adjoints preserve (co)limits. Adjoint functor theorem. 6. Monads and Algebras. Examples. Eilenberg Moore and Kleisli as terminal and initial adjunctions inducing a monad. Groups monadic over Set. Lift and Powerset monads and their algebras. Forgetful functor from T-Alg creates limits. 7. Cartesian closed categories and the \lambda-calculus. Examples of ccc's. Parameter theorem. Typed \lambda calculus and its interpretation in ccc's. Ccc's with natural numbers object: all primitive recursive functions are representable. The notes are available by anonymous ftp from URL: ftp://ftp.daimi.aau.dk/pub/BRICS/LS/95/1/BRICS-LS-95-1.ps.gz [T1] ================================================ AMAST Links 02 03 Axiomatic type classes in Isabelle - documentation *Update* of information in [AL0202T4] Users may be unaware of axiomatic type classes, a new feature implemented by Markus Wenzel at Munich. Some documentation, in German, is now available at URL: ftp://ftp.cl.cam.ac.uk/ml/axclass.dvi.gz [T2] ================================================ AMAST Links 02 03 LOLA (LOtos LAboratory) 3R6 release announcement *Update* of information in [AL0202T5] The full version of this announcement is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203T2.txt Release 3R6 of LOLA is now available at URL: ftp://ftp.dit.upm.es/pub/lotos/tools/TOPO_3R6/contrib/LOLA_3R6 including a compiled version for 386+. See the full announcement for details. [T3] ================================================ AMAST Links 02 03 Logic courseware: Turing's World, Tarski's World, Hyperproof WWW : http://csli-www.stanford.edu/hp/ _Authors:_ Jon Barwise (barwise@indiana.edu) John Etchemendy (etch@csli.stanford.edu) **Tarski's World** The Macintosh version of Tarski's World is available in two ways, either alone (called "Tarski's World 4.0") or as part of the logic textbook/software package called _The Language of First-order Logic_, by Barwise and Etchemendy. Tarski's World is also available for IBM-compatible computers equipped with Microsoft Windows. **Hyperproof** Hyperproof is proof system that allows the user to reason using both sentences of first-order logic and blocks world diagrams similar to those used in Tarski's World. It is an excellent companion to Tarski's World or The Language of First-order Logic. It is presently available only for the Macintosh. **Turing's World** The new version allows the user to build finite state machines and nondeterministic machines, in addition to Turing machines. It is currently available only on Macintosh. A version of Turing's World for IBM-compatible machines running Microsoft Windows is nearing completion and should be available in Spring, 1995. **Ordering Information** See the WWW page or contact the authors. [T4] ================================================ AMAST Links 02 03 LiDIA: A library for computational number theory The full version of this information is available at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203T4.txt LiDIA is a C++ library for computational number theory which provides a collection of highly optimized implementations of various multiprecision data types and time-intensive algorithms. LiDIA is developed by the LiDIA Group, at the Universit"at des Saarlandes. After having installed LiDIA, please send us an email saying that you have done so. This enables us to inform you about bugs, bug fixes, new version, etc. We would also appreciate all sorts of feedback, bug reports and bug fixes, enhancements etc. You can send your suggestions, enhancements, etc to lidia@cs.uni-sb.de Please, send bug reports (and fixes) to lidia-bugs@cs.uni-sb.de We will probably also set up a mailing list. *Contents* of the full announcement: 1. Abstract 2. LiDIA Group 3. Contents of this Release 4. How to get and install LiDIA 4.1 FTP procedure 4.2 Unpacking procedure 4.3 Installation procedure (short version 4.4 Calling a test program 4.5 Installation procedure (long version 5. Note [P1] ================================================ AMAST Links 02 03 Kleisli category for multiple monads? by David Espinosa Is it possible to form the Kleisli category of several monads at once? I can imagine an indexed product of the individual Kleisli categories, but I lack the technical facility to describe it. In my thesis, I have a category with multiple monads, relating the different "levels" of a denotational semantics (environments, stores, etc). _More info_ at URL: http://www.cs.columbia.edu/~espinosa/ The monad laws follow easily from the Kleisli formulation; they say that the Kleisli category is actually a category. The monad morphism laws say that an arrow between monads is a functor between Kleisli categories. What I expect from a "multi-Kleisli" formulation is that Kleisli compositions associate (when possible). Specifically, given monads P and PQ (where Q is another functor) and arrows f: A -> PQB, g: QB -> PQC, h: C -> PQD, we'd like (oPQ (oP f g) h) = (oP f (oPQ g h)) where oP and oPQ are the Kleisli compositions of the monads. I can postulate a category with this structure, but it would be nicer if it came from a general construction. P.S. Other formulations of associativity are: ;; bindT: TA * (A -> TB) -> TB f: A -> PQB, g: QB -> PQC (bindP (bindPQ pqa f) g) = (bindPQ pqa (lambda (a) (bindP (f a) g))) ;; mapT: (A -> B) * TA -> TB ;; joinT: TTA -> TA ;; f: A -> PQB, ;; g: QB -> PQC (joinP (mapP g (joinPQ (mapPQ f pqa)))) = (joinPQ (mapPQ (lambda (a) (joinP (mapP g (f a)))) pqa)) Can we rewrite this using join in a more natural way? [S1] ================================================ AMAST Links 02 03 AMAST Series in Computing: Address and Order Information The volumes published in the _AMAST Series in Computing_ contain presentations of those algebraic methods used for software development which are both theoretically well founded and efficiently implemented. The goal of these volumes is to provide comprehensive mathematical alternatives for software design and implementation. The scope of this series includes all areas of computer science. To *publish* your research in the _AMAST Series in Computing_ please contact the Managing Editor: T. Rus Department of Computer Science, The University of Iowa Iowa City, IA 52242, USA. E-mail: rus@cs.uiowa.edu To *order* contact one of the Publisher's offices: USA: World Scientific Publishing Co., Inc. 1060 Main Street, River Edge, NJ 07661 Toll-free: +1 800 2277562, fax: +1 201 4879656 e-mail: wspub@tigger.jvnc.net Europe: World Scientific Publishing Co. Ltd. 57 Shelton Street, London WC2H 9HE, England, UK Tel: +44 71 8360888, fax: +44 71 8362020 e-mail: wspc@wspc.demon.co.uk Singapore: World Scientific Publishing Co. Pte. Ltd. Farrer Road, P O Box 128, Singapore 9128 Tel: +65 3825663, fax: +65 3825919 e-mail: worldscp@singnet.com.sg Hong Kong: World Scientific Publishing (HK) Co. P O Box 72482, Kowloon Central Post Office, Hong Kong Tel: +852 2 7718791, fax: +852 2 7718155 India: World Scientific Publishing Co. Pte. Ltd. 4911, 9th Flr, High Point IV, 45 Palace Rd, Bangalore 560 001, India Tel: +91 80 2205972, Fax: +91 80 3344593, Tlx: 0845-2900 PCO IN [S2] ================================================ AMAST Links 02 03 Gathering Information about Teaching in Computable Analysis by Klaus Weihrauch While discrete computability and complexity theory is one of the main disciplines in theoretical computer science, seemingly computer scientists have neglected computability and complexity in *analysis* in research and especially in teaching. I would like to gather information about the present situaton in teaching. If you do teach *effective analysis* in your courses, please, send me some information, e.g. about the following: o undergraduate or graduate course? o as a part of a course on computability, complexity or calculus / analysis, as a tool in some other course, as a separate course? o which model? (algebaic, intuitionistic, Bishop, Russian, Polish, Pour-El and Richards, real RAM, BSS, IBC, Ko and Friedman, "bit-complexity", ...) o main topics? o further comments. I shall mail the answers (in condensed form, if there should be too many) to THEORYNT. [S3] ================================================ AMAST Links 02 03 Assembling a WWW page on Isabelle projects by Lawrence C Paulson I'd like to assemble a WWW page detailing some of the projects that people have done using Isabelle. If you would like to contribute, please send me a line or two describing what you have done. If possible, please include html links to relevant papers or proof files. I'll announce the final WWW page when it is ready. Thanks for your help! [S4] ================================================ AMAST Links 02 03 Information request from the ACM SIGACT Long Range Planning Committee The SIGACT Long Range Planning Committee is in the process of preparing a document to be distributed to relevant officials of funding agencies that highlights the impact that research in theoretical computer science has had on the practice of computing and on science in general. The idea is to emphasize the importance of maintaining a strong research program in theoretical computer science. If you know of a result that has recently had influence in some area outside of theoretical computer science, please send a paragraph intended for a lay audience describing the result and its impact to smith@cs.umd.edu Thank you for your cooperation. The SIGACT Long Range Planning Committee: A. Amir, M. Blum, M. Loui, J. Savage, C. Smith (chair) [A1] ================================================ AMAST Links 02 03 New items in AMAST repository at CS Faculty of University of Twente := http://www.cs.utwente.nl/data/amast/ := ftp://ftp.cs.utwente.nl/pub/doc/amast/ Date: 15/03/1995 Contents: Index.html, README, amast91/, amast93/, amast95/, info/, links/, pstv95/, sigala/ ... links/ : AMAST newsletter Contents : AL-Index.html, v02/, v01/, sample/ Note : The file AL-Index.html provides WWW users with links to individual issues of the AMAST newsletter (...) v02/ : second volume of AMAST Links (1995) Contents : i03/, i02/, i01/ i03/ : AMAST Links Vol. 02, Issue 03 [15/03/1995] full/ [A2] ================================================ AMAST Links 02 03 This issue was edited by Giuseppe Scollo, Arie van Deursen, Michael Johnson, Edmund Kazmierczak and Elena Trichina, thanks to contributions by: V. S. Alagar [M1], Donald T. Sannella [M2], Peter D. Mosses [M3], Jean-Michel Muller [M4], Tamas Gaizer [M5], Amy Felty [M6], Maurice Margenstern [M7], Erik Meijer [M8], Wiebe van der Hoek [M9], Walter Unger [MA], Kathrine Wenham [MB], Lawrence C. Paulson [MC,CC,T1,S3], Ulrich Furbach [MD], Mutsumi Imai [ME], Anne Hodgson [MF], Giuseppe Longo [MG], P. Takis Metaxas [MH], Cristian Calude [MI], Rolf Wanka [C1], Hans Kleine Buening [C2], Ugo Montanari [C3], Ming Li [C4], Andrea Corradini [C5], L. Kirousis [C6], Arnold L. Rosenberg [C7], HCRC Univ. Edinburgh [C8], Douglas Howe [C9,T3], Alan Mycroft [CA], Prabhakar Raghavan [CB], X-SLALM Secretary [CD], Randal Peters [CE], Vijaya Chandru [CF], NIPS*95 Organization [CG], COLIBRI 6-1995 [J1], Johan Hestad [J2], Marshall Bern [J3], Karen K. Moller [J4], Edmund Robinson [J5], A.M.King [J6], John Glauert [J7], Teodor Rus [L1,L2,L3,L4,S1], Andre' Arnold [L3], Ina Schieferdecker [L5], Uffe Engberg [L6], Pierre Ageron [L7], John Baez [L8], Jean-Yves Girard [L9], Gavin M Bierman [LA], Nick Benton [LB], Gopalan Nadathur [LC], Jaap van Oosten [LD], David Larrabeiti L. [T2], Thomas Papanikolaou [T4], David Espinosa [P1], Klaus Weihrauch [S2], Carl H. Smith [S4]. This issue of AMAST Links is available in four forms: o a collection of hypertext files, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/AL0203-ToC.html for the ToC-page, where links give access to individual pages; o a single hypertext file, available on the WWW at URL: http://www.cs.utwente.nl/data/amast/links/v02/i03/AL0203.html o a collection of plain-text files, one per page, each separately available (+) (see below) o a single plain-text file available by e-mail as well as (+) within the AMAST directory of the Twente WWW server, at URL http://www.cs.utwente.nl/data/amast/links/v02/i03/AL0203.txt where `' is either `-ToC' (for the ToC-page),or the 2-character page identifier (for one-page files), or empty (whole-issue file). *Note:* This issue will also be available, in all of its four forms, by anonymous ftp from the AMAST repository at the University of Twente. File names will be the same as above, but under the _ftp directory_ at URL: ftp://ftp.cs.utwente.nl/pub/doc/amast/links/v02/i03/ [end] =============================================== AMAST Links 02 03