Return-Path: To: Greg Restall Cc: linear@cs.stanford.edu Subject: Re: Papers available by Public ftp In-Reply-To: <9403281716.AA16320@Ghoti.Stanford.EDU> Date: Mon, 28 Mar 94 13:19:40 PST From: pratt@CS.Stanford.EDU Sender: lincoln@cs.stanford.edu --text follows this line-- Date: Mon, 28 Mar 1994 15:04:37 +1000 From: Greg Restall The directory contains a file README with short descriptions of the works in the directory. They include papers on substructural logics, With regard to your "A Useful Substructural Logic" in that directory, it is worth mentioning that this logic supports an equational definition of transitive closure. See my paper @InProceedings( Pr90b, Author="Pratt, V.R.", Title="Action Logic and Pure Induction", Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478", Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120", Address="Amsterdam, NL", Month=Sep, Year=1990) making this point, abstract appended, paper available by anonymous ftp as boole.stanford.edu:/pub/jelia.tex. At a talk at a 1992 conference: @InProceedings( Pr92c, Author="Pratt, V.R.", Title="A Roadmap of Some Two-Dimensional Logics", Booktitle="Logic and Information Flow", Editor="Van Eijck, J. and Visser, A.", Year="1994") (belatedly published only this year due to unplanned change of publisher by the organizers) I identified a number of RA-like logics. Your Peirce monoids appear on my chart as the class RES of residuated monoids, while their expansion with transitive closure is ACT (for action algebras). This paper is twod.tex on Boole. Key to any equational definition of transitive closure is the ability to express induction, which requires some form of antimonotonicity. With residuated or Peirce monoids, antimonotonicity is supplied by residuation (implication). An alternative source of antimonotonicity is Boolean negation, which I used much earlier to define transitive closure equationally in @InProceedings( Pr79c, Author="Pratt, V.R.", Title="Models of program logics", Booktitle="20th Symposium on foundations of Computer Science", Address="San Juan", Month=Oct, Year=1979) and @InProceedings( Pr80b, Author="Pratt, V.R.", Title="Dynamic algebras and the nature of induction", Booktitle="12th ACM Symposium on Theory of Computation", Address="Los Angeles", Month=Apr, Year=1980) Vaughan Pratt ============= Abstract: In Floyd-Hoare logic programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a -> b (HAD a THEN b) and postimplication b <- a (b IF-EVER a). Unlike REG, ACT is finitely based, makes a* reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a -> a)* = a -> a. Return-Path: <@Sunburn.Stanford.EDU:Jean.Marc.Andreoli@xerox.fr> Date: Tue, 29 Mar 1994 09:37:23 --100 From: Jean.Marc.Andreoli@xerox.fr (Jean Marc Andreoli) To: linear@cs.stanford.edu Subject: CFP, ECOOP'94 workshop (W4) on Logical Foundations of OOP X-Sun-Charset: US-ASCII Content-Length: 3793 Sender: lincoln@cs.stanford.edu --text follows this line-- ---------------------------------------------------------------------- Call for participation One day workshop on Logical Foundations of Object Oriented Programming in connection with ECOOP'94 4 - 8 July 1994 Bologna, Italy The aim of this workshop is to investigate the relation between logic, computing and object oriented programming. Both the declarative and computational aspects of logic have long been exploited in the context of object-oriented programming. For instance, researchers have investigated the use of static type- and effect-inferencing mechanisms, and the use of Dijkstra-Hoare-style assertional systems for reasoning about state changes produced by method invocations. Considerable work has been done in extending basic declarative computational formalisms (e.g. lambda calculus) that support the essence of OOP. On the computational side, novel OOP techniques have emerged from the use of "agent-oriented" (concurrent) programming languages based on the computational interpretation of fragments of various logics. Conversely, some of the fundamental insights of OOP concern the structuring of large (computational) formal descriptions so as to minimize change in the face of evolution. These insights are equally applicable when the formal systems are also logical, as happens for example, in constructing large domain theories of phenomena of interest. Recent developments in substructural approaches to logic (e.g. linear logic) and rewriting logic offer the promise of considerably expanding the repertoire of logical techniques that can be brought to bear in the design, execution and analysis of OO systems. These developments internalize a fundamental notion of localized state-change within logic. A primary objective of this workshop will be to investigate the applicability and usefulness of these techniques to the design of real-world object-oriented computational systems. The workshop will consist of short presentations as well as informal discussions. We expect to establish a state-of-the-art in the use of logic for Object Oriented Programming, as well as to contribute to a better understanding between researchers in this area. Topics of interest include but are not limited to the following: - Logic based models for Object Oriented Programming - Logic and change - Use of logic in object-oriented domain modeling and analysis - Declarative object-oriented real-time systems - Abstraction, Encapsulation, and information hiding in logic - Knowledge-structuring mechanisms in logic (inheritance, overriding...) - Process-oriented mechanisms in logic (communication, synchronization...) Last but not least, descriptions of applications developed on logic based object-oriented environments are welcome. Organizers: Jean-Marc Andreoli (Rank-Xerox, Grenoble, France) and Vijay Saraswat (Xerox, Palo-Alto, California) Please send a position paper (e-mail if possible, latex prefered) to Jean-Marc Andreoli | Tel: +33 76 61 50 80 Rank Xerox Research Center | Switchboard: +33 76 61 50 50 6 Chemin de Maupertuis | Fax: +33 76 61 50 99 38240 Meylan (France) | E-mail: Jean.Marc.Andreoli@xerox.fr Specify whether you wish to make a presentation (in that case, send a title and 2-3-line abstract). Presentations are limited to 15 minutes and will be selected and scheduled by the organizers. Submission due: 13 May, 1994 Date of the workshop: 4 July, 1994 IMPORTANT: The participation to the workshop is free, but each workshop participant must have registered for the main ECOOP conference. ---------------------------------------------------------------------- Return-Path: <@Sunburn.Stanford.EDU:joerg@leibniz.informatik.uni-tuebingen.de> Date: Wed, 30 Mar 94 12:25:56 +0200 From: joerg@leibniz.informatik.uni-tuebingen.de (Joerg Hudelmaier) To: linear@cs.stanford.edu Subject: papers available Sender: lincoln@cs.stanford.edu --text follows this line-- A number of recent papers related to linear logic are available by anonymous ftp from ftp.informatik.uni-tuebingen.de: 1) File /pub/LS/lamlog.{ps,dvi}.Z: Classical Lambek Logic by J. Hudelmaier and P. Schroeder-Heister. A paper about proof theoretical properties of the two sided version of classical noncommutative linear logic. In particular we formulate a cut free yet complete sequent calculus for this logic. 2) File /pub/LS/hier.ps.Z: On a hierarchy of fragments of intuitionistic propositional logic by J. Hudelmaier. We give a simple syntactic definition of a hierarchy H of sets of so called CD-sequents such that intuitionistic provability of the sequents in the stages of H is hard for successive stages of the polynomial hierarchy. Moreover provability for the set of all CD-sequents is PSPACE complete. One corollary says that the CD- sequents provide a polynomial normal form for intuitionistic propositional logic. Another corollary is 3) File /pub/LS/comp.ps.Z: On the complexity of commutative and noncommutative linear logic by J. Hudelmaier. Here we show that the fragment of both commutative and noncommutative linear logic based on (one) implication and additive conjunction is PSPACE complete. 4) File /pub/LS/modal.ps.Z: On a contraction free sequent calculus for the modal logic S4 by J. Hudelmaier. We formulate a sequent calculus for S4 in which deductions of sequents are bounded in length by the length of the endsequent. The calculus is much more complicated than similar calculi for intuitionistic propositional logic. But it may be possible to use this calculus for an embedding of S4 into linear logic without modalities in a manner similar to what has been done for intuitionistic implication. 5) File /pub/LS/KTS4.ps.Z: Improved decision procedures for the modal logics K,T, and S4 by J. Hudelmaier. Using methods developped in 4) we arrive at decision procedures of space complexity n log n, n log n, n*n log n for the logics K, T, and S4 respectively. Joerg Hudelmaier Return-Path: <@Sunburn.Stanford.EDU:rossi@di.unipi.it> Organization: Dipartimento di Informatica - Universita' di Pisa - Italy From: Francesca Rossi Subject: ilps94 call for workshop proposal (text+latex) Date: Wed, 30 Mar 1994 18:00:20 +0100 (METDST) X-Mailer: ELM [version 2.4 PL22] Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 5323 To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Call For Workshop Proposals - ILPS'94 INTERNATIONAL LOGIC PROGRAMMING SYMPOSIUM Sponsored by the Association for Logic Programming Post-Conference Workshops Ithaca, New York, USA November 13 -- 19, 1994 The 1994 International Logic Programming Symposium will be held November 13-19, 1994, in Ithaca, New York, USA. Up to six post-conference workshops are planned for November 18-19. Researchers from all areas of logic programming are invited to submit proposals. To encourage active participation and exchange of ideas, the workshops will be kept small, preferably under 40 participants. The format of the workshop will be determined by the organizer(s) proposing the workshop, but ample time must be allowed for general discussion. Workshops can vary in length, but the optimal duration will be half a day or a full day. Having two or three co-organizers for a workshop is strongly advised. Workshops are particularly appropriate for specialized subcommunities of researchers for whom a larger workshop or conference is not yet justified. Proposals for workshops should be about two pages in length, and should contain: o A description of the workshop, identifying specific technical issues that will be addressed. o A discussion of the timeliness and relevance of the workshop. o The name, postal address, phone and fax numbers, and email address of the workshop organizer(s) and identification of the principal contact person. o A proposed schedule for organizing the workshop, a preliminary agenda, and the indication of the length of the workshop. Proposals should be submitted no later than May 16, 1994. Organizers will be notified no later than June 16, 1994. Workshop organizers will be responsible for: o Producing a "Call for Participation" in the workshop and posting it via various electronic lists and/or other means. o Reviewing requests to participate in the workshop and selecting participants. o Scheduling workshop activities. Please submit proposals and inquiries (hardcopy or e-mail) to: Howard Blair School of Computer and Information Science Syracuse University Syracuse, New York 13244-4100 USA\ Phone: 315-443-3565 FAX: 315-443-1122 E-mail: blair@top.cis.syr.edu Return-Path: <@Sunburn.Stanford.EDU,@ICINECA.CINECA.IT:HONSELL@UDUNIV.CINECA.IT> Date: Wed, 30 MAR 94 18:44 N From: HONSELL@UDUNIV.CINECA.IT Reply-To: HONSELL@UDUNIV.CINECA.IT Comments: GMAIL V1.3, DECnet, 21 Mar 1989 Subject: School Announcement To: LINEAR@CS.STANFORD.EDU X-Original-To: linear@cs.stanford.edu, HONSELL Sender: lincoln@cs.stanford.edu --text follows this line-- PRELIMINARY ANNOUNCEMENT ADVANCED SCHOOL ON TYPED LAMBDA CALCULUS AND FUNCTIONAL PROGRAMMING September 19 - September 30, 1994 CISM, Palazzo del Torso, Piazza Garibaldi, 18 - UDINE Udine (ITALY) The Advanced School is organized under the auspices of the Italian Chapter of EATCS (European Association for Theoretical Computer Science) and UNESCO. It is supported also by the University of Udine and the CNR. Formal Methods for specifying, modularizing, verifying, and reusing large programs and systems, as well as principled languages, which allow to apply rapidly such methods, are greatly needed in Computer Science. Typed Lambda Calculus has been recently understood as a central node in a conceptual network which links various fields of Logic to Computer Science. It has made possible to transfer fruitfully ideas and techniques from Category Theory, Proof Theory, Type Theory to Computer Science. Based on formally solid and conceptually disciplined logical grounds, Typed Lambda Calculus allows for the development of a mathematically clear style of programming as well as for the design of flexible logical tools and methods for Computer Science. In recent years, Typed Lambda Calculus has been impressively used also as a metalanguage for defining formal systems for reasoning about Programs and as a logical framework for designing interactive proof assistants} for computer aided formal reasoning. The School will offer 5 series of (approx.8-10) introductory and advanced lectures on the connections between Typed Lambda Calculus and Category Theory, Proof Theory, and Type Theory, and on the, more recent, applications of Typed Lambda Calculus, such as the design of Typed Functional Languages, General Proof Assistants, and Program Logics. SCHOOL DIRECTORS M. DEZANI CIANCAGLINI (Torino) FURIO HONSELL (Udine) LIST OF SPEAKERS JEAN-YVES GIRARD (Marseilles) Proof Theoretic Foundations GERARD HUET (INRIA Rocquencourt) Advanced Typed Functional Languages: Theorem Proving in Coq JOHN MITCHELL (Stanford) Type Systems and Programming Languages EUGENIO MOGGI (Genova) Meta-languages and Applications S. RONCHI DELLA ROCCA (Torino) Basic Lambda Calculus The School is intended primarily for young researchers and PhD students in Computer Science and Mathematics. During the School, participants will be able to attend also informal talks and discussions of open problems. PhD students may ask to sit for an examination at the School. It will consist of a Seminar on a topic agreed upon by the Directors and the Speakers. There will be demonstrations, and participants will have the opportunity to use a computer environment. To apply, participants should fill the form (to be publicized shortly) and return it together with a recommandation letter to: Advanced School Secretariat: Professor F.Honsell Universita' di Udine, Dipartimento di Matematica e Informatica via Zanon, 6, 33100 UDINE - ITALY Tel: 39-432-272220 Fax: 39-432-510755 The DEADLINE for application is July 31st 1994. Further information can be obtained via email under the address: scuola@dimi.uniud.it FEES and SCHOLARSHIPS The participation fee is 650.000 Italian Liras. There is a limited number of scholarships available for people who cannot obtain funding for their travel, participation fee and living expenses from their institutions. A request for full or partial support should be enclosed with the applications. Return-Path: <@Sunburn.Stanford.EDU:felty@research.att.com> Date: Wed, 6 Apr 94 19:53 EDT From: felty@research.att.com (Amy Felty) To: linear@cs.stanford.edu Subject: LICS'94 Program and Registration Sender: lincoln@cs.stanford.edu --text follows this line-- [This announcement is being sent to email lists. Our apologies for multiple copies.] LOGIC IN COMPUTER SCIENCE (LICS) ******************************** Ninth Annual IEEE Symposium July 3-7, 1994, Paris, France ADVANCE REGISTRATION AND PROGRAM INFORMATION ============================================ [This information is available on the world-wide web at http://www.research.att.com/lics/ Postscript, dvi, latex and plain text versions of the conference brochure are available via anonymous ftp from research.att.com in directory /dist/lics.] CONFERENCE OFFICE. ================= Please address registration form and inquiries to LICS'94 Secretariat Claudie Thenault INRIA-Rocquencourt Relations Exterieures Domaine de Voluceau BP 105 78153 Le Chesnay Cedex FRANCE Phone: 33 (1) 39 63 56 75 Fax: 33 (1) 39 63 56 38 E-mail: symposia@inria.fr REGISTRATION ============ The registration form should be sent to the conference office. Registration without payment (or purchase order) enclosed will not be considered. For early registration, payment must be received by June 5. Fees will be returned in full for any written cancellation received before June 24. No refund will be made after this date. A table of registration fees can be found on the registration form. The member rate applies to members of ACM, IEEE, EATCS and INRIA, members of the organizing and program committees and authors of accepted papers. The student rate applies to full time students; a copy of the registrant's 1993-94 student card should be included with the registration form. The registration fee includes conference participation, a copy of the proceedings, coffee breaks and an invitation to the welcome reception. There is a separate charge for the banquet. Payment must be in French currency, and can be made by bank cheque, postal cheque, or foreign draft made payable to "Agent Comptable de l'INRIA", by bank transfer to Tresorerie Generale des Yvelines, Versailles, account number 10071-78000-00044009 15389, by postal transfer to CCP Paris---30041-00001-09099 45 B 020-31, or by institutional purchase order. We have applied for permission to allow registration by credit card, and hope to have confirmation of this possibility by May 1. Participants wishing to use this facility should contact our office at that time, preferably by email addressed to symposia@inria.fr. Bank transfers should specify registrant's name and "Conference reference LICS94". ACCOMMODATION ============= Reservations can be made through the Wagonlit Travel Agency. The accommodation form should be sent with deposit before June 1 to: Wagonlit Travel Departement Congres & Evenements 50 Rue de Londres 75008 Paris FRANCE Tel: 33 (1) 44 90 33 10 Fax: 33 (1) 44 90 33 15 There are two categories of hotels available, as well as inexpensive student lodging (no age limit) in an international center in Clichy (north Paris). Paris is very popular in the summer, so reservations should be made as soon as possible. A deposit is compulsory for hotel reservations, and student lodging must be entirely prepaid. Payment must be in French currency, and can be made by bank cheque, Eurocheque, or foreign draft made payable to "Wagonlit Travel", by bank transfer to the account 00021935201/61 B.N.P. Paris Saint Lazare, bank code 30004, branch code 0819, "Wagonlit Travel---code comptable 04/670", or by credit card. Hotel deposits will be forwarded to the hotel less 60FF for reservation fees. The participant's bank charges must be added to the amount transferred. For cancellations made before June 1, payments will be refunded less 60FF for fees; no refunds will be made after June 1. LOCATION ======== The Conference is being hosted by the Conservatoire National des Arts et Metiers (CNAM) and will be part of its Bicentennial celebration. CNAM is a well-known engineering school where professionals are taught by professionals. It houses the famous Musee National Des Arts et Techniques, and is located at 292 Rue Saint Martin in the old center of Paris, on the right bank of the river Seine. It is walking distance from Les Halles, the Centre National d'Art et de Culture Georges-Pompidou (Beaubourg), the Hotel de Ville (City Hall) and the cathedral Notre-Dame de Paris. The nearest Metro station is Arts et Metiers. Paris normally enjoys pleasant summer weather in early July. Days are warm, but nights may be cool. For general information on Paris, contact the Paris Tourist Information Office, 127 Champs Elysees, 75008 Paris, phone number 33 (1) 49 52 53 54. RECEPTIONS ========== A Welcome Reception will be held on Sunday evening (17:00-19:00) in a gallery of CNAM. The Conference Banquet will be held in the palace housing the Senate, the upper chamber of the French Parliament. The palace was built in the beginning of the 17th century for Marie de Medicis, widow of King Henry IV. It is located in the well-known Jardins du Luxembourg. To reserve a place at the banquet, the appropriate column on the registration form must be marked; a banquet reservation on site will not be possible. LOCAL ARRANGEMENTS ================== Lunches are at the participants' own expense. Participants may eat in cafes and restaurants in CNAM's vicinity. Telephone messages will be delivered to participants during breaks. Access to email will be possible from CNAM. The organizers cannot be held liable to conference participants for injury, damage or loss of their personal property. It is suggested that participants make their own insurance arrangements. REGISTRATION DESK ================= A registration and information desk located at the conference site will operate on Sunday, July 3, from 15:00 to 18:00, and on the remaining conference days from 8:00 to 18:00. TRAVEL ====== Paris has two airports, Roissy-Charles de Gaulle, 30km north of Paris, and Orly, 20km south of Paris. A frequent Air France bus service goes from Roissy to Place Charles de Gaulle-Etoile or Porte Maillot in central Paris (the cost is about 48FF); from Orly the bus goes to Invalides and stops on demand at Montparnasse (32FF). There is also train service. From Roissy, the RER B line goes to Gare du Nord or Chatelet; from Orly, the Orlyval goes to Antony where there is a connection to the RER B (32FF). A taxi from Orly to central Paris costs about 150FF; from Roissy, 200FF. The Metro offers a convenient way to get around the city. Each trip (with unlimited transfers) costs one ticket. Tickets can be bought individually, but a carnet of 10 is more practical. RER lines to the suburbs connect with the Metro and cost more. Both Metro and RER tickets can be purchased from ticket booths or machines. A 40-45% discount may be obtained from AIR INTER for French domestic blue and white flights, depending on the days of departure. A voucher can be requested on the registration form. Participants requiring a visa for entry into France are strongly advised to make their application in their home countries at least two months prior to departure date. LICS'94 REGISTRATION FORM ************************* Last Name __________________________________________________ First Name _________________________________________________ Affiliation ________________________________________________ Street Address _____________________________________________ _______________________________________________________ City _______________________________________________________ State/Zip __________________________________________________ Country ____________________________________________________ Phone(s) ___________________________________________________ Fax ________________________________________________________ E-mail _____________________________________________________ REGISTRATION RATES. The fees below are in French currency and include 18.6% VAT. Please circle the applicable fees. through June 5 from June 6 Regular 2200 2600 Member 1700 2100 Student 1000 1200 Banquet 300 300 Total Fee ___________________________________________________ Rate justification __________________________________________ Full-time student at ________________________________________ I need an AIR INTER discount form: Yes / No Payment (circle one): Cheque (Bank/Foreign Draft) / Purchase Order / Bank Transfer (include copy) LICS'94 ACCOMMODATION FORM ************************** to be returned before Jun 1 Last Name __________________________________________________ First Name _________________________________________________ Company ____________________________________________________ Street Address _____________________________________________ _______________________________________________________ City _______________________________________________________ State/Zip __________________________________________________ Country ____________________________________________________ Phone(s) ___________________________________________________ Fax ________________________________________________________ 1A. HOTEL. Please reserve: *...twin bed room shared by 2 persons *...single room in a hotel of ________ stars, for ________ nights, from _________________ to _________________(a.m.). Average rates in French currency, per room and per night, room only, taxes and service included: Category Single/Twin Deposit 2** 385/500 460 3*** 550/700 760 1B. YOUTH HOSTEL. Please reserve: *...bed in a twin bed room, bathroom and toilets outside the room, compulsory stay of 4 nights (July 3 to 7, 1994), continental breakfast included, full prepayment compulsory, fixed rate per person 4 nights: 600FF. 2. PAYMENT. Deposit/prepayment of ____________ FF Circle one: Visa / Eurocard / Mastercard / Cheque (Bank/Euro/Foreign Draft) / Bank Transfer (include copy) Credit card # __________________________ Exp. __________ Signature _____________________________ Date ___________ CONFERENCE PROGRAM ****************** SUNDAY, July 3 ============== REGISTRATION (15:00-18:00) WELCOME RECEPTION (17:00-19:00) MONDAY, July 4 ============== REGISTRATION (8:00-9:00) OPENING ADDRESSES (9:00-9:25) INVITED LECTURE I (9:25-10:25) Chair: Robert Constable (Cornell) Rod Burstall (Edinburgh), Lambda-terms, proofs and refinement SESSION 1: FINITE MODEL THEORY (10:50-12:30) Chair: Daniel Leivant (Indiana) 10:50 McColm's Conjecture, Yuri Gurevich (Michigan), Neil Immerman (U Mass) & Saharon Shelah (Hebrew U & Rutgers) 11:15 The expressive power of finitely many generalized quantifiers, Anuj Dawar (Swansea) & Lauri Hella (Helsinki) 11:40 Generalized quantifiers for simple properties, Martin Otto (RWTH Aachen) 12:05 How to define a linear order on finite models, Lauri Hella (Helsinki), Phokion Kolaitis (UC Santa Cruz), & Kerkk Luosto (Helsinki) LUNCH (12:30-14:00) SESSION 2: CONCURRENCY (14:00-15:15) Chair: Vaughan Pratt (Stanford) 14:00 Finitary fairness, Rajeev Alur (Bell Labs) & Thomas Henzinger (Cornell) 14:25 Bisimulation is not (first-order) equationally axiomatisable, Peter Sewell (Edinburgh) 14:50 Foundations of timed concurrent constraint programming, Vijay Saraswat (Xerox PARC), Radha Jagadeesan (Loyola) & Vineet Gupta (Stanford) SESSION 3: SEMANTICS I (15:40-16:55) Chair: Achim Jung (Darmstadt) 15:40 A fully abstract semantics for concurrent graph reduction, Alan Jeffrey (Sussex) 16:05 An axiomatization of computationally adequate domain-theoretic models of FPC, Marcelo Fiore & Gordon Plotkin (Edinburgh) 16:30 On strong stability and higher-order sequentiality, Loic Colson & Thomas Ehrhard (Marne-la-Vallee) SESSION 4: DOMAIN THEORY (17:10-18:00) Chair: Carl Gunter (U Penn) 17:10 Linear types, approximation and topology, Michael Huth, Achim Jung & Klaus Keimel (Darmstadt) 17:35 Domain theory and integration, Abbas Edalat (Imperial Coll.) BUSINESS MEETING (20:00) TUESDAY, July 5 =============== TUTORIAL I (8:30-9:45) Chair: Moshe Vardi (Rice) Ed Clarke (CMU), Model Checking SESSION 5: CONSTRAINTS (10:00-10:50) Chair: Harald Ganzinger (MPI Saarbrucken) 10:00 Negative set constraints with equality: an easy proof of decidability, Witold Charatonik (Wroclaw) & Leszek Pacholski (Polish Academy of Sciences) 10:25 Systems of set constraints with negative constraints are NEXPTIME-complete, Kjartan Stefansson (Cornell) SESSION 6: MODAL AND TEMPORAL LOGICS I (11:15-12:30) Chair: Dexter Kozen (Cornell) 11:15 A compositional proof system for the modal mu-calculus, Hendrik Reif Andersen (TU Denmark), Colin Stirling (Edinburgh) & Glynn Winskel (Aarhus) 11:40 On the parallel complexity of model-checking in the modal mu-calculus, Shipei Zhang, Oleg Sokolsky & Scott Smolka (SUNY Stony Brook) 12:05 Complexity transfer for modal logic, Edith Hemaspaandra (Le Moyne) LUNCH (12:30-14:00) SESSION 7: TYPES I (14:00-15:15) Chair: Paris Kanellakis (Brown) 14:00 Typability and type-checking in the second-order lambda-calculus are equivalent and undecidable, J.B. Wells (Boston U) 14:25 Efficient inference of object types, Jens Palsberg (Northeastern) 14:50 Type inference and extensionality, Adolfo Piperno (Roma) & Simona Ronchi della Rocca (Torino) SESSION 8: CONSTRUCTIVE MATHEMATICS (15:40-16:55) Chair: Daniel Leivant (Indiana) 15:40 A groupoid model refutes uniqueness of identity types, Martin Hofmann (Edinburgh) & Thomas Streicher (LMU Muenchen) 16:05 A non-elementary speed-up in proof length by structural clause form transformation, Matthias Baaz, Christian Fermueller & Alexander Leitsch (TU Wien) 16:30 Upper and lower bounds for tree-like cutting planes proofs, Russell Impagliazzo (UC San Diego), Toniann Pitassi (UC San Diego) & Alasdair Urquhart (Toronto) SESSION 9: COMPLEXITY AND DATABASES (17:10-18:00) Chair: David McAllester (MIT) 17:10 The power of reflective relational machines, Serge Abiteboul (INRIA), Christos Papadimitriou (UC San Diego) & Victor Vianu (UC San Diego) 17:35 A syntactic characterization of NP-completeness, J. Antonio Medina & Neil Immerman (U Mass) EVENING LECTURE (19:30-20:30) Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS) Corrado Boehm (Roma), An algebraic view of the lambda-calculus WEDNESDAY, July 6 ================= TUTORIAL II (8:30-9:45) Chair: Samson Abramsky (Imperial Coll.) Gerard Berry (CMA), The semantics of synchronous concurrent languages SESSION 10: LOGIC PROGRAMMING (10:00-10:50) Chair: Krzysztof Apt (CWI) 10:00 The declarative semantics of the Prolog selection rule, Robert Staerk (U Muenchen) 10:25 Semantics of meta-logic in an algebra of programs, Antonio Brogi & Franco Turini (Pisa) SESSION 11: LINEAR LOGIC (11:15-12:30) Chair: Samson Abramsky (Imperial Coll.) 11:15 A multiple-conclusion meta-logic, Dale Miller (U Penn) 11:40 Proof search in first-order linear logic and other cut-free sequent calculi, Patrick Lincoln & N. Shankar (SRI) 12:05 Linear logic, totality and full completeness, Ralph Loader (Oxford) LUNCH (12:30-14:00) SESSION 12: TYPES II (14:00-15:15) Chair: Frank Pfenning (CMU) 14:00 The emptiness problem for intersection types, Pawel Urzyczyn (Warsaw) 14:25 Subtyping and parametricity, Gordon Plotkin (Edinburgh), Martin Abadi (DEC SRC) & Luca Cardelli (DEC SRC) 14:50 On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study, Herman Geuvers (Nijmegen) & Benjamin Werner (Cornell & INRIA) SESSION 13: SEMANTICS II (15:40-16:55) Chair: Prakash Panangaden (McGill) 15:40 A semantics of object types, Martin Abadi & Luca Cardelli (DEC SRC) 16:05 Passivity and independence, Uday Reddy (Illinois) 16:30 A general semantics for evaluation logic, Eugenio Moggi (Genova) SESSION 14: CATEGORY THEORY (17:10-18:00) Chair: Glynn Winskel (Aarhus) 17:10 Reflexive graphs and parametric polymorphism, Edmund Robinson (Sussex) & Giuseppe Rosolini (Genova) 17:35 Categories, allegories and circuit design, Carolyn Brown (Sussex) & Graham Hutton (Chalmers) BANQUET THURSDAY, July 7 ================ INVITED LECTURE II (9:00-10:00) Chair: Gerard Huet (INRIA) Henk Barendregt (Nijmegen), Results and problems related to proof-checking SESSION 15: REWRITING (10:00-10:50) Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS) 10:00 Rewrite techniques for transitive relations, Leo Bachmair & Harald Ganzinger, (Max-Planck-Institut) 10:25 Normalised rewriting and normalised completion, Claude Marche (CNRS & INRIA) SESSION 16: LAMBDA-CALCULUS (11:15-12:30) Chair: Jean-Jacques Levy (INRIA) 11:15 Modularity of strong normalization and confluence in the algebraic lambda-cube, Franco Barbanera (Torino), Maribel Fernandez (Paris Sud & CNRS), & Herman Geuvers (Nijmegen) 11:40 Cyclic lambda graph rewriting Zena Ariola (U Oregon) & Jan Willem Klop (CWI) 12:05 Paths in the lambda-calculus, Andrea Asperti (Bologna), Vincent Danos (CNRS & Paris 7), Cosimo Laneve (INRIA & CMA), & Laurent Regnier (CNRS) LUNCH (12:30-14:00) SESSION 17: MODAL AND TEMPORAL LOGIC II (14:00-15:15) Chair: Colin Stirling (Edinburgh) 14:00 A trace based extension of linear time temporal logic, P.S. Thiagarajan (SPIC Madras) 14:25 Axioms for knowledge and time in distributed systems with perfect recall, Ron van der Meyden (NTT Tokyo) 14:50 Compositional verification of real-time systems, Edward Chang (Stanford), Zohar Manna (Stanford), & Amir Pnueli (Weizmann Institute) SESSION 18: LOGIC IN ARTIFICIAL INTELLIGENCE (15:40-16:55) Chair: Peter Schroeder-Heister (Tuebingen) 15:40 Logical bilattices and inconsistent data, Ofer Arieli & Arnon Avron (Tel Aviv) 16:05 A modal logic for subjective default reasoning, Shai Ben-David & Rachel Ben-Eliyahu (Technion) 16:30 Language completeness of the Lambek calculus, Mati Pentus (Moscow State) SESSION 19: AUTOMATED DEDUCTION} (17:10-18:00) Chair: Gerard Huet (INRIA) 17:10 Rigid E-unifiability is NEXPTIME-complete, Jean Goubault (Bull) 17:35 Higher-order narrowing, Christian Prehofer (TU Muenchen) END OF CONFERENCE CONFERENCE ORGANIZATION *********************** LICS General Chair: Robert L. Constable 1994 Conference Co-chairs: Gerard Huet & Jean-Pierre Jouannaud 1994 Program Chair: Samson Abramsky Publicity Co-chairs: Amy Felty & Douglas Howe 1994 Local Arrangements: A. Theis-Viemont & C. Thenault PROGRAM COMMITTEE: ================== S. Abramsky, K. Apt, H. Ganzinger, C. Gunter, A. Jung, P. Kannelakis, D. Kozen, D. Leivant, J.-J. Levy, D. McAllester, P. Panangaden, F. Pfenning, V. Pratt, P. Schroeder-Heister, C. Stirling, G. Winskel. ORGANIZING COMMITTEE: ===================== M. Abadi, S. Abramsky, S. Artemov, A. Borodin, A. Bundy, S. Buss, E. Clarke, R. Constable (Chair), A. Felty, U. Goltz, Y. Gurevich, S. Hayashi, D. Howe, G. Huet, J.-P. Jouannaud, D. Kapur, C. Kirchner, P. Kolaitis, R. Kosaraju, D. Kozen, D. Leivant, A.R. Meyer, D. Miller, J. Mitchell, Y. Moschovakis, M. Okada, P. Panangaden, A. Pitts, G. Plotkin, J. Remmel, S. Ronchi della Rocca, G. Rozenberg, A. Scedrov, D. Scott, J. Tiuryn, M.Y. Vardi. Return-Path: <@Sunburn.Stanford.EDU:psh@hume.Informatik.Uni-Tuebingen.De> Date: Mon, 11 Apr 94 17:46:58 +0200 From: psh@hume.Informatik.Uni-Tuebingen.De (Peter Schroeder-Heister) To: linear@cs.stanford.edu Subject: Substructural Logics Sender: lincoln@cs.stanford.edu --text follows this line-- A collection of papers originating from a conference held 1990 at the University of T\"ubingen is now available. Kosta Do\{v}sen & Peter Schroeder-Heister (Eds.), Substructural Logics. Oxford University Press 1993. ISBN 0-19-853777-8. UK-Price: GBP 40.00, US-Price: approx. USD 60.00. (On cover and title page of the printed edition the editors are listed in non-alphabetical order. This is due to an error by the publisher. It does not express any rank order.) Contents: Preface A Historical Introduction to Substructural Logics K. Do\v{s}en Life in the Undistributed Middle N. Belnap Theorems in Classical Logic are Instances of Theorems in Condensed BCI Logic M.W. Bunder Partial Gaggles Applied to Logics with Restricted Structural Rules J.M. Dunn A General Theory of Structured Consequence Relations D.M. Gabbay Decidability and Interpolation for a First-Order Relevance Logic A. Kron Logic without Structural Rules (Another Look at Cut Elimination) J. Lambek >From Categorial Grammar to Bilinear Logic J. Lambek The Semantics of Entailment 0 R.K. Meyer and E.D. Mares Semantics for Substructural Logics H. Ono The Semantics of Pretopologies G. Sambin Lambda-Terms with Functional Symbols and Decidability in Certain Closed Categories S. V. Soloviev Tutorial on Linear Logic A.S. Troelstra The Landscape of Deduction J. van Benthem Index The preface and the first page of each chapter are contained in the file /pub/LS/substruc.ps.Z which can be ftp'ed from ftp.informatik.uni-tuebingen.de. Return-Path: <@Sunburn.Stanford.EDU:felty@research.att.com> Date: Thu, 14 Apr 94 16:56 EDT From: felty@research.att.com (Amy Felty) To: linear@cs.stanford.edu Subject: LICS'94 registration and ASL members Sender: lincoln@cs.stanford.edu --text follows this line-- LOGIC IN COMPUTER SCIENCE ******************************** Ninth Annual IEEE Symposium July 3-7, 1994, Paris, France Please note the following correction to the LICS'94 registration information: the member rate also applies to members of the Association for Symbolic Logic. [Complete program and registration information is available on the world-wide web at http://www.research.att.com/lics/ Postscript, dvi, latex and plain text versions of the conference brochure are available via anonymous ftp from research.att.com in directory /dist/lics.] Return-Path: <@Sunburn.Stanford.EDU:farwer@rzdspc2.informatik.uni-hamburg.de> X-Sender: farwer@rzdspc2.informatik.uni-hamburg.de (Unverified) Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Wed, 20 Apr 1994 08:19:44 +0100 To: linear@cs.stanford.edu From: farwer@rzdspc2.informatik.uni-hamburg.de Subject: PhD theme Sender: lincoln@cs.stanford.edu --text follows this line-- I have so far taken a broad interest in Linear Logic, but have not yet found out in which direction to do do any further work. This is probably due to the lack of interest among colleages and therfore the impossiility of apt on site discussions. As I am still determined to do further work on Linear Logic I have two questions: 1) What are the main fields of interest to researchers (i.e *you*) at the moment? 2) Do you have any suggestions as to which topics (open problems) I could focus on for my PhD? Any help and suggestions are gratefully accepted. Thanks in advance. Berndt ---------------------------------------------------------------------------- Berndt Farwer Universit"at Hamburg \\\\\ \\\\\\\ FB Informatik \\ \\ \\ farwer@informatik.uni-hamburg.de Diplomand TGI \\\\\ \\\\ phone (++44)+40-54715-244 Vogt-K"olln-Str. 30 \\ \\ \\ fax (++44)+40-54715-246 D-22301 Hamburg \\\\\ \\ Germany Return-Path: <@Sunburn.Stanford.EDU:lincoln@csl.sri.com> Date: Wed, 20 Apr 94 10:24:14 -0700 From: Pat Lincoln To: linear@cs.stanford.edu Subject: WWW Sender: lincoln@cs.stanford.edu --text follows this line-- I have built a small www server for linear logic: http://www.csl.sri.com/linear/sri-csl-ll.html This contains two implementations of a par symbol for TeX, a picture from last year's workshop, archives of old messages to the linear mailing list, and pointers to ftp directories containing papers previously announced on the linear mailing list. Also reachable from there in http://www.csl.sri.com/history.html is a picture of the original mouse (developed at SRI in the 1960's) and other items of computing history. Although ftp is a slower and uglier interface than mosaic, the linear information is available through anonymous ftp to: ftp.csl.sri.com in directory /pub/linear. pdl.