A NEWTON INSTITUTE SUMMER SCHOOL: SEMANTICS AND LOGICS OF COMPUTATION September 25-29, 1995, Newton Institute, Cambridge, UK * Courses. The aim is to present a number of modern developments in semantics and logics of computation in a way that is accessible to graduate-level students. Courses: Samson Abramsky (Imperial) on "Semantics of interaction"; Thierry Coquand (Chalmers) on "Computational content of classical logic"; Martin Hofmann (Edinburgh) on "Dependent type theory: syntax, semantics, and applications"; Martin Hyland (Cambridge) on "Game Semantics"; Eugenio Moggi (Genova) on "Computational types and applications"; Mogens Nielsen & Glynn Winskel (Aarhus) "Models for concurrency"; Andrew Pitts (Cambridge) "Operationally-based theories for proving program properties". * Registration. Registrations from postgraduate students will be given priority, but applications by interested academics and industrialists are also welcomed. There are only a limited number of places available on the Summer School. Intending participants are advised to apply for registration as soon as possible, and in no case later than 31 May 1995. To apply, please send your name and address (including e-mail or fax number, if available) to: Florence Leroy, (SEM Summer School), Isaac Newton Institute, 20 Clarkson Road, Cambridge CB3 0EH. Tel: +44 1223 335984. Fax: +44 1223 330508. Email: f.leroy@newton.cam.ac.uk. * Fees. General rate: 400 pounds. Student rate: 250 pounds. The fee covers registration, accommodation, meals (breakfast, lunch, supper, tea & coffee breaks), and lecture materials. CONFERENCE ON COMPUTER-AIDED VERIFICATION (CAV '95) July 3-5, 1995, Liege, Belgium [Call for papers in Newsletter 20] * Deadlines. The deadline for early registration is June 12. A limited number of rooms are being held for participants. Reservation will be handled on a first-come first-served basis. Early reservation is advisable. * Further Information. Through the WWW, or by sending email to cav95@montefiore.ulg.ac.be. WORKSHOP ON VERIFICATION AND CONTROL OF HYBRID SYSTEMS October 22-25, 1995, New Brunswick, New Jersey, USA * Topics. Submissions are invited in all areas pertaining to the formal verification and control of hybrid systems, that is, systems in which digital devices interact with continuous objects. We are especially interested in methods that bring together in creative ways concepts from computer science and control theory. Topics include, but are not limited to, formal models and specification languages, algorithmic and deductive verification, control and optimization, simulation and testing, design and synthesis, complexity and decidability issues, probabilistic systems, automatic and interactive tools, experimental results and applications. * Submissions. An extended abstract not exceeding twelve pages, either six hard-copies or a postscript file, by July 26, to Rajeev Alur, 2D-144, AT&T Bell Laboratories, 600 Mountain Avenue, Murray Hill, NJ 07974, USA. Email: alur@research.att.com (postscript only). The full versions of selected submissions will be published after the workshop as a volume of the Springer-Verlag Lecture Notes in Computer Science series. * Program Committee. Rajeev Alur, Albert Benveniste, John Guckenheimer, Thomas A. Henzinger, Bruce Krogh, Amir Pnueli, Peter Ramadge, Shankar Sastry, Fred B. Schneider, Eduardo Sontag, Hector Sussmann, Joseph Sifakis. DIMACS SUMMER SCHOOL ON APPLIED LOGIC AND ALGORITHMS * Courses. The Summer School is intended to expose industry, graduate students, postdocs, and experienced researchers from other fields to the three focus areas of the DIMACS Special Year on Logic and Algorithms: Finite-Model Theory, Proof Complexity, and Computer-Aided Verification. The courses will provide students with a deep understanding of these research areas and will point out connections with applications. * Course on Finite-Model Theory. Dates: August 14-18, 1995. Organizer: James Lynch (jlynch@sun.mcs.clarkson.edu). Lecturers: Neil Immerman, Phokion G. Kolaitis, James F. Lynch. * Course on Bounded Arithmetic and Complexity of Proofs. Dates: August 21-25, 1995. Organizer: Toniann Pitassi (toni@cs.pitt.edu). Lecturers: Samuel R. Buss, Paul Beame, Alasdair Urquhart. * Course on Computer-Aided Verification. Dates: August 28 - September 1, 1995. Organizer: Kenneth McMillan (mcmillan@cadence.com). Lecturers: David L. Dill, Robert Kurshan, Kenneth McMillan, J Strother Moore, Pierre Wolper. * Registration. The DIMACS Conference Center at Rutgers can accommodate about 80 participants. Subject to this capacity constraint, courses are open to all researchers; there is no registration fee. Although registration at the door is permitted, we ask that you register by June 30, 1995, to give us some idea of attendance. Pre-registrants will be given priority in case of capacity constraints. In addition, information on local housing will be sent to people who pre-register. We are seeking funding to support attendance by graduate and postdoctoral students, emphasizing participation by members of underrepresented groups. NEWTON INSTITUTE WORKSHOP ON THEMES IN THE SEMANTICS OF COMPUTATION July 17-21, 1995, Newton Institute, Cambridge, UK. * Topics. The workshop will take place as part of the Newton Institute programme on the Semantics of Computation. The general aims of the programme are twofold. First, to refine the current framework for the semantics of computation so that it is capable of dealing with the more subtle computational features present in the programming languages of today and tomorrow. Secondly, to provide a framework for interaction between such fundamental research and the issues confronted by language designers and software engineers. We particularly have in mind current developments such as object-based concurrent programming, and projects to develop the next generation of advanced programming languages, such as ML 2000. The range of technical and conceptual challenges involved in this work requires active collaboration and flow of information between overlapping communities of mathematicians, computer scientists and computer practitioners. The workshop is intended to open up some of the themes to be pursued during the Semantics of Computation research programme, with some emphasis on the interplay between theory and practice. * Invited Speakers. Tony Hoare, Cliff Jones, Gilles Kahn, Robin Milner, John Reynolds, Akinori Yonezawa. * Submissions. The organizers invite offers of contributed talks. These will be selected on the basis of submitted abstracts. Abstracts in English (up to 2 pages) should be sent (preferably by email) to Prof. Samson Abramsky (TSC), Department of Computing, Imperial College, 180 Queen's Gate, London SW7 2BZ. Email: sa@doc.ic.ac.uk. * Further Information. Prof. Samson Abramsky (sa@doc.ic.ac.uk). J. OF SYMBOLIC COMPUTATION SPECIAL ISSUE ON EXECUTABLE TEMPORAL LOGICS * Editors. Editor-in-Chief: Bruno Buchberger. Guest Editors: Michael Fisher, Shinji Kono, Mehmet Orgun. * Topics. High quality original research papers are solicited on all aspects relating to the foundations, implementation techniques and applications of languages based upon temporal logic. The research described must not only incorporate an adequate level of technical detail, but must also provide a clear indication of both the utility and the applicability of the results. Topics of interest include, but are not limited to: theoretical issues in executable temporal logics; design of executable temporal logics; relationship between execution and temporal theorem-proving; operational models and implementation techniques; programming support and environments; comparative studies of languages; relationship of executable temporal logics to (temporal) databases; applications and case studies. * Submissions. In addition to longer papers, we would welcome short papers (5 to 10 pages) describing specific features or novel applications of executable temporal logic. Submissions should follow the JSC style guide available from ftp://ftp.risc.uni-linz.ac.at/pub/jsc LaTeX users are encouraged to use the jsc.sty file. Electronic submission is strongly encouraged (either as self-contained LaTeX, or postscript). Submissions, either electronic or a paper copy of the full paper, should arrive no later than October 15th 1995, and should be sent to the principal guest editor: Michael Fisher, Department of Computing, Manchester Metropolitan University, Manchester M1 5GD, United Kingdom. Tel: +44 161 247 1488. Fax: +44 161 247 1483. Email: M.Fisher@doc.mmu.ac.uk. FINITE MODEL THEORY BIBLIOGRAPHY * Further Information. Argimiro Arratia-Quesada (quesada@math.wisc.edu). LOGIC COLLOQUIUM 95 August 9-17, Haifa, Israel * Update. Price list and registration forms available. * Further information. WWW page, or Logic Colloquium 95, Yvonne Sagi, Department of Computer Science, Technion--Israel Institute of Technology, Haifa 32000, Israel. logic95@cs.technion.ac.il. SIXTH ANNUAL INT'L SYMPOSIUM ON ALGORITHMS AND COMPUTATION (ISAAC95) December 4-6, 1995, Cairns, Australia * Topics. Papers presenting original research in the areas of design and analysis of algorithms, computational complexity, and theory of computation are sought. Typical, but not exclusive, topics of interest include: automata, languages and computability, algorithms (combinatorial/graph/geometric/randomized), vlsi and parallel algorithms, networks and distributed algorithms, theory of learning and robotics, number theory and cryptography, graph drawing, computational logic. * Program Committee: John Staples (Chair), Peter Eades (Co-Chair), Naoki Katoh (Co-Chair), Sue Whitesides, Nick Wormald, Takeshi Tokuyama, Seinosuke Toda, Giuseppe DiBattista, Sing-Ling Lee, Xiang-Sun Zhang, Mikhail Atallah, Dorothea Wagner, Bruce Litow, Jeff Vitter, Norbert Eisinger. * Invited Speakers. Franco Preparata, John Crossley, Satoru Miyano. * Submissions. 15 copies (in English) of an extended abstract of at most 10 double-spaced pages by 12 May 1995 to: Professor John Staples, Department of Computer Science, University of Queensland, Queensland 4072, Australia. * Further Information. Dr. Bob Cohen, Department of Computer Science, University of Newcastle, Callaghan, NSW 2308, Australia. Ph: +61 049 21 5291. Fax: +61 049 21 6929. E-Mail: isaac95@cs.newcastle.edu.au. 10TH INTERNATIONAL CONFERENCE ON FUNDAMENTALS OF COMPUTATION THEORY (FCT'95) August 22-25, 1995, Dresden, Germany * Further Information. The WWW page contains the FCT'95 program (invited lectures, accepted papers, invited talks of the minisymposium on specification of time-critical systems) the registration form and accommodation reservation form. One can get a full version of the announcement also be sending e-mail to fct95@tcs.inf.tu-dresden.de. * Deadlines. Deadline for early reservation: June 30, 1995. 2ND WORKSHOP ON LOGIC, LANGUAGE, INFORMATION AND COMPUTATION July 26-28, 1995, Recife, Brazil * Topics. All areas related to logic, language, information and computation, including: pure logical systems, proof theory, model theory, type theory, category theory, constructive mathematics, lambda and combinatorial calculi, program logic and program semantics, nonclassical logics, nonmonotonic logic, logic and language, discourse representation, logic and AI, automated deduction, foundations of logic programming, logic and computation, and logic engineering. * Invited speakers. M Abadi, C Alchourron, A Avron, N Belnap, J van Benthem, P Freyd, D Gabbay, I Hodkinson, P Lincoln, V Pratt. * Programme committee. W A Carnielli, M Costa, V de Paiva, R de Queiroz, A Haeberer, T Pequeno, L C Pereira, A M Sette, P Veloso (Chair, PUC, Rio). * Submissions. Two-page abstracts (preferably by e-mail to wollic95@di.ufpe.br) must be RECEIVED by JUNE 1ST, 1995 by the Chair of the Organising Committee. Authors will be notified of acceptance by July 1st, 1995. WoLLIC '95 is sponsored by the Interest Group in Pure and Applied Logics (IGPL) and The European Association for Logic, Language and Information (FoLLI). Abstracts from members of the IGPL will be published in the Bulletin of the IGPL (ISSN 0945-9103) as part of the meeting report. Selected contributed papers will be invited for submission to a special issue of the Bulletin. * Location. Recife is the capital of the sun belt coast in the northeast of Brazil, just 8 degrees below Equator, bathed by 250+ days of sun/year (ie Caribbean-like climate). City population is around 2.5 million. Recife is over 450 years old, has a number of interesting architectural samples of Portuguese colonial times (esp. XVII and XVIII centuries), and is neighbour to picturesque Olinda, whose architectural heritage is protected by UNESCO. * Further Information. Ruy de Queiroz, Departamento de Informatica, Universidade Federal de Pernambuco (UFPE), Caixa Postal 7851, Recife, PE 50732-970, Brazil, e-mail: wollic95@di.ufpe.br, tel: +55 81 271 8430, fax +55 81 271 4925. NEW TEXTBOOK * Title. How To Prove It -- A Structured Approach. * Author. Daniel J. Velleman, Amherst College. * Summary. This textbook will prepare readers to make the transition from solving problems to proving theorems by teaching them the techniques needed to read and write proofs. The book begins with the basic concepts of logic and set theory. These concepts are used as the basis for a step-by-step breakdown of the most important techniques used in constructing proofs. The author shows how complex proofs are built up from these smaller steps, using detailed "scratchwork" sections to expose the machinery of proofs about the natural numbers, relations, functions, and infinite sets. Numerous exercises give readers the opportunity to construct proofs. * Ordering Information. Cambridge University Press. 1994. 319 pp. 0-521-44116-1, hardback, $49.95. 0-521-44663-5, paperback, $19.95. To order this book, click here, or e-mail to orders@cup.org.