HYPATIA ELECTRONIC LIBRARY * Hypatia is a directory of research workers in computer science and mathematics, and a library of their papers. It is not a web crawler but a resource for and about our research community, containing only relevant information, over which authors have full control. * Hypatia has been implemented by Mark Dawson, who set up and ran the popular mirrored archive at theory.dc.ic.ac.uk, adding many new features such as search facilities. The database has been enlarged and corrected, and users can now contribute data interactively. It now also contains email/postal addresses, Web pointers and bibliographies. * Hypatia would like to encourage each author to compile a BibTeX database of his/her own papers. Draft personal bibliographies are provided, for authors to edit and complete, and there is a guide to help them do this. * Hypatia is at Queen Mary and Westfield College in London's East End. * Hypatia invites you to come and visit! Contact: firstname.lastname@example.org. CALL FOR NOMINATIONS: CADE-13 WOODY BLEDSOE STUDENT TRAVEL AWARD * Award. The board of trustees of the Conference on Automated Deduction Inc. (CADE) have created an award in honor of the memory of Woody Bledsoe for his contributions to mathematics, artificial intelligence, and automated theorem proving, and for his dedication to students. The award is intended to cover most of the expense for one student working in the field of automated deduction to attend CADE-13, which will be held at Rutgers University, U.S.A., July 30 through August 3, 1996 (see http://www.research.att.com/lics/floc/cade13/). The winner will receive $350 (US) for local expenses and up to $650 for transportation expenses, and the CADE registration fee will be waived. Preference will be given to students who will be playing an active role in the conference and to students who do not have alternative funding. * Nominations. Nominations which should include a recommendation of up to 300 words from the student's supervisor, should be sent by e-mail (preferred) to email@example.com or by ordinary mail to William McCune, MCS-221, Argonne National Laboratory, Argonne IL 60439, U.S.A. Nominations must arrive no later than May 15, and the winner will be notified by June 1. The award will be presented at CADE-13; in case the winner cannot attend, the trustees may transfer the award to another nominee. 3RD INT'L CONF ON TYPED LAMBDA-CALCULUS AND APPLICATIONS (TLCA'97) April 2-4, 1997, Nancy, France * Topics. Type systems for lambda calculi. Proof theory of type systems. Semantics of type systems. Typed lambda calculi. Proof verification via type systems. Type systems of programming languages. Typed term rewriting systems. * Program Committee. H. Barendregt, C. Boehm, M. Dezani, G. Dowek, R. Hindley (Chair), F. Honsell, P. Lescanne, A. Pitts, G. Plotkin, P. Scott, J. Smith, M. Takahashi, V. Tannen, J. Tiuryn, * Submissions. Roger Hindley, Mathematics Department, University of Wales Swansea, Swansea SA2 8PP, U.K. E-mail: firstname.lastname@example.org. Fax: (+)-44-1792-295843. Electronic submission is preferred (Postscript files only), although hard copy (6 copies) is also acceptable at the cost of some delay in communication. Papers should not exceed 15 standard A4 or U.S. quarto pages. Deadline for submissions: August 30, 1996. * Further Information. P. de Groote, P. Lescanne, INRIA Lorraine, 615 rue du Jardin Botanique, B.P. 101, 54602 Villers-les-Nancy Cedex, FRANCE. E-mail: Philippe.de.Groote@loria.fr INT'L CONF ON FORMAL AND APPLIED PRACTICAL REASONING (FAPR'96) June 3-7, 1996, Bonn, Germany * Preliminary Program and Registration Information. Avaliable on web page. * Contact. Professor Dov Gabbay, Dept of Computing, 180 Queen's Gate, London SW7 2BZ; Tel ++44 171 5948205; Fax ++44 171 5948201. 21ST INT'L SYM: MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE (MFCS'96) September 2 - 6, 1996, Cracow, Poland * Topics. Algorithms and data structures, automata and formal languages, complexity and computability, concurrency theory, data bases and knowledge-based systems, declarative programming, formal specifications and programd evelopment, models of computation, parallel and distributed computing, semantics and logics of programs, theoretical issues in artificial intelligence, type theory, VLSI systems. * Invited Speakers. E. Clarke, V. Diekert, A. Gibbons, P. Mosses, D. Peled, J. Remmel, D. Sannella P.S. Thiagarajan, J. Tiuryn, V. Uspensky. * Further Information. Wojciech Penczek, MFCS'96 Program Chair, Institute of Computer Science, Polish Academy of Sciences, ul. Ordona 21, 01-237 Warsaw, Poland. Tel: +48 22 36 28 41. Fax: +48 22 37 65 64. E--mail: email@example.com. BRICS AUTUMN SCHOOL IN VERIFICATION October 28, 1996, duration 1 week, Aarhus, Denmark * Theme. Theorem Proving and Model Checking. * Further Information. att. Autumn School, BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, Bldg. 540, DK-8000 Aarhus C, Denmark. CADE'96 TUTORIAL: EQUALITY REASONING IN SEQUENT-BASED CALCULI April 22, 1996, Rutgers U., New Jersey, USA * Lecturers. Anatoli Degtyarev, Andrei Voronkov (Uppsala University). * FLoC. This tutorial will be held as a part of CADE, which is itself embedded in the 1996 Federated Logic Conference. For further information on FLOC/CADE (including conference site, transport, etc) see the FLoC homepage. * Summary. The techniques of equality reasoning presented in the tutorial is applicable to all known sequent-based methods of automated deduction, including the tableau method, the connection method, model elimination and the inverse method. We are going to illustrate main results and ideas on the tableau method and on the inverse method (as a typical non-local top-down and a typical local bottom-up search methods in sequent calculi). * Topics. Early history. Methods of proof-search in sequent calculi. Theorem proving using simultaneous rigid e-unification. The decidable cases of simultaneous rigid e-unification. Tableau calculi with rigid paramodulation/superposition. Can incomplete procedures for rigid e-unification be used for adding equality to the tableau method? A bottom-up approach to equality reasoning in sequent-based calculi. Equality reasoning in non-classical logics. POSITION AVAILABLE: UPPSALA UNIVERSITY * Position. Senior lectureship in computing science (ADB), at the Department of Computing Science, Dno 2006/96. Date of commencement as soon as possible after September 1, 1996. * Duties. Research in Computing Science within the following of the ongoing research projects in ADB at the department: 1) methodologies for developing and constructing complex information systems= , 2) high level constraint programming for resource allocation problems, 3) inductive logic programming and 4) logic programming methodology. Supervision of PhD students within these research projects. Teaching at the department's undergraduate, graduate and PhD programmes. Ability to teach in either English or Swedish is required. * Further Information. Professor Ake Hansson (Ake.Hansson@csd.uu.se), phone: +46 18 181042 or Associate Professor Andreas Hamfelt (Andreas.Hamfelt@csd.uu.se), phone +46 18 181037, fax +46 18 521217. * Deadline. May 20, 1996. CADE-13 WORKSHOP: PROOF SEARCH IN TYPE-THEORETIC LANGUAGES July 30, 1996, Rutgers University, New Brunswick, USA * Update. Extended submission deadline: May 19, 1996. [First announcement: Newsletter 33.] * Organization/Program Chair. D. Galmiche, CRIN-CNRS, UHP Nancy I, Batiment LORIA, 54506 Vandoeuvre-les-Nancy, France. Phone: +33 83 59 20 15. Fax: +33 83 41 30 79. email: Didier.Galmiche@loria.fr. 6TH INTL WKSHP: LOGIC PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR'96) Stockholm, Sweden, August 28-30, 1996 * Update. Second Call for Papers. [First CFP: Newsletter 33.] * Deadline. May 17, 1996 for submission of extended abstracts. * Programme Chair. John Gallagher, University of Bristol, UK; phone: +44 (0)117 9287959; fax: +44 (0)117 9288128; E-mail: firstname.lastname@example.org. LOGICAL FOUNDATIONS OF MATHEMATICS, COMPUTER SCIENCE AND PHYSICS -- KURT GOEDEL'S LEGACY (GOEDEL'96) August 25-29, 1996, Brno, Czech Republic * Update. Program and registration form available. [First anncuncemnent: Newsletter 31.] * Contacts. Programme committee chairman: Petr Hajek, Institute of Computer Science, Academy of Sciences of the Czech Republic, Pod vodarenskou vezi 2, CZ-182 07 Prague, Czech Republic; e-mail: email@example.com; telephone: +42-2-66053760, +42-2-6884244; fax: +42-2-8585789. Organization: Jiri Zlatuska, Faculty of Informatics, Masaryk University, Botanicka 68a, CZ-602 00 Brno, Czech Republic; e-mail: firstname.lastname@example.org; telephone: +42-5-41213125, +42-5-41211646, +42-5-41213219; fax: +42-5-41212747.