From cat-dist@mta.ca Thu Feb 1 10:11:13 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA11766; Thu, 1 Feb 1996 10:11:12 -0400 Date: Thu, 1 Feb 1996 10:10:10 -0400 (AST) From: categories To: categories Subject: Associate Professor Positions at Italian Universities Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 1 Feb 1996 08:45:54 +0100 From: Eugenio Moggi A competition for associate professor positions has been advertised by MURST (Italian Ministery for University and Research), the deadline for application is the 30th Aprile 1996. Full details are available in italian from the MURST server (http://sirio.cineca.it/murst-diu/), these include: - text of the ads published on the GU (Offical Gazet), - positions available (e.g. 68+49 in comp. sci., 174 in math. disciplines) - sample application (for italian and foreigners) Eugenio Moggi -- From cat-dist@mta.ca Thu Feb 1 16:02:53 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09013; Thu, 1 Feb 1996 16:02:53 -0400 Date: Thu, 1 Feb 1996 15:59:38 -0400 (AST) From: categories To: categories Subject: Conference Announcement ICFP w/ FLIC Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 1 Feb 1996 13:29:14 -0600 (CST) From: Matthias Felleisen ======================================================================== Preliminary Program 1996 ACM SIGPLAN International Conference on Functional Programming and Functional Languages in the Introductory Computing Curriculum Philadelphia, Pennsylvania, USA May 24-26, 1996 (see also http://www.cs.indiana.edu/icfp96/program.html) ======================================================================== The ACM SIGPLAN International Conference on Functional Programming (ICFP) is a new annual conference combining the established LISP and Functional Programming (LFP) and Functional Programming and Computer Architecture (FPCA) conferences. The conference is sponsored by ACM SIGPLAN in association with IFIP WG 2.8 and will take place in Philadelphia, Pennsylvania as part of the Federated Computing Research Conference (FCRC '96). A workshop on Functional Languages in the Introductory Computing Curriculum (FLIC) will be held on the morning of May 24 in connection with ICFP. ======================================================================== ==== Functional Languages in the Introductory Computing Curriculum ===== ======================================================================== (see also http://www.cs.rice.edu/~matthias/FLIC/FLICp.html) Keynote Lecture: 9:15 Friday Programming as a Medium for Teaching Gerald J. Sussman (MIT) and Daniel P. Friedman (Indiana University) ------------------------------------------------------------------------ Session FLIC 1: 10:05-11:05 Friday Chair: Matthias Felleisen (Rice University) Teaching Computation Theory Of and With Scheme Albert Meyer (MIT) Scheme in Pre-College Classrooms Ian Ferguson and Terry Kaufman (Schemer's Inc.) ------------------------------------------------------------------------ Session FLIC 2: 11:20-12:50 Friday Chair: Christopher Haynes (Indiana University) Programming Languages and Techniques Carl Gunter (University of Pennsylvania) CAML at ENS Guy Cousineau (Ecole Normale Superieure) An FP-based Series of Undergraduate Lectures using Gofer S. Doaitse Swierstra (University of Utrecht) ======================================================================== ========== International Conference on Functional Programming ========== ======================================================================== Session 1: 2:00-3:30 Friday Chair: Olivier Danvy (Aarhus University) Let-floating: moving bindings to give faster programs Simon Peyton Jones, Will Partain, and Andre Santos (University of Glasgow) A reflection on call-by-value Amr Sabry (University of Oregon) and Philip Wadler (University of Glasgow) Functional back-ends within the lambda-sigma-calculus Therese Hardin (LITP and INRIA Rocquencourt), Luc Maranget (INRIA Rocquencourt), and Bruno Pagano (LITP and INRIA Rocquencourt) ------------------------------------------------------------------------ Session 2: 4:00-5:30 Friday Chair: Olin Shivers (MIT) Lag, drag, void and use -- heap profiling and space-efficient compilation revisited Niklas Rojemo and Colin Runciman (University of York) Static and dynamic partitioning of pointers as links and threads David S. Wise and Joshua Walgenbach (Indiana University) Storage use analysis and its applications Manuel Serrano (University of Montreal & INRIA Rocquencourt) and Marc Feeley (University of Montreal) ------------------------------------------------------------------------ Plenary Invited Speaker: 8:00-9:00 Saturday Computing is Interaction Robin Milner (Cambridge) ------------------------------------------------------------------------ Session 3: 9:30-10:30 Saturday Chair: Paul Hudak (Yale University) The role of lazy evaluation in amortized data structures Chris Okasaki (Carnegie Mellon University) Deriving structural hylomorphisms from recursive definitions Zhenjiang Hu, Hideya Iwasaki, and Masato Takeichi (University of Tokyo) ------------------------------------------------------------------------ Session 4: 11:00-12:30 Saturday Chair: John Launchbury (Oregon Graduate Institute) Analysis and caching of dependencies Martin Abadi (Digital Systems Research Center), Butler Lampson (Microsoft), and Jean-Jacques Levy (INRIA Rocquencourt) Optimality and inefficiency: What isn't a cost model of the lambda calculus? Julia L. Lawall (IRISA) and Harry G. Mairson (Brandeis University) Inductive, coinductive, and pointed types Brian T. Howard (Kansas State University) ------------------------------------------------------------------------ Session 5: 2:00-3:30 Saturday Chair: Didier Remy (INRIA) A new look to pattern matching in abstract data types Pedro Palao Gostanza, Ricardo Pena, and Manuel Nunez (Universidad Complutense de Madrid) Simplifying subtyping constraints Francois Pottier (ENS Paris & INRIA Rocquencourt) Complexity of kernel Fun subtype checking Giorgio Ghelli (Universita di Pisa) ------------------------------------------------------------------------ Session 6: 4:00-5:30 Saturday Chair: Matthias Felleisen (Rice University) The semantics of Scheme with future Luc Moreau (University of Southampton) First-class synchronization barriers Franklyn Turbak (Wellesley College) pHluid: The design of a parallel functional language implementation Cormac Flanagan (Rice University) and Rishiyur S. Nikhil (Digital Equipment Corporation) ------------------------------------------------------------------------ Plenary Invited Speaker: 8:00-9:00 Sunday The case for wireless overlay networks Randy Katz (UC Berkeley) ------------------------------------------------------------------------ Session 7: 9:30-10:30 Sunday Chair: Peter Lee (Carnegie Mellon University) Cogen in six lines Peter Thiemann (Universitat Tubingen) A probabilistic approach to the problem of automatic selection of data representations Tyng-Ruey Chuang and Wen L. Hwang (Academia Sinica, Taiwan) ------------------------------------------------------------------------ Session 8: 11:00-12:30 Sunday Chair: John Reppy (AT&T Research) A theory of weak bisimulation for core CML William Ferreira, Matthew Hennessy, and Alan Jeffrey (University of Sussex) A provable time and space efficient implementation of NESL Guy E. Blelloch and John Greiner (Carnegie Mellon University) Synchronous Kahn networks Paul Caspi (VERIMAG) and Marc Pouzet (McGill University) ------------------------------------------------------------------------ Session 9: 2:00-3:30 Sunday Chair: Andrew Wright (NEC Research) Enriching the lambda calculus with contexts: toward a theory of incremental program construction Shinn-Der Lee and Daniel P. Friedman (Indiana University) Sharing code through first-class environments Christian Queinnec (Ecole Polytechnique & INRIA Rocquencourt) and David DeRoure (University of Southampton) Mixin modules Dominic Duggan and Constantinos Sourelis (University of Waterloo) ======================================================================== General Chair: Robert Harper (Carnegie Mellon University) Program Chair: R. Kent Dybvig (Indiana University) Program Committee: Luca Cardelli (Digital SRC) Peter Lee (CMU) Olivier Danvy (Aarhus Univ.) Atsushi Ohori (Kyoto Univ.) Matthias Felleisen (Rice Univ.) Didier Remy (INRIA) Richard Gabriel (ParcPlace) John Reppy (AT&T Bell Labs.) Paul Hudak (Yale Univ.) Olin Shivers (MIT) John Launchbury (Oregon Grad. Inst.) Andrew Wright (NEC Research) FLIC Organizers: Matthias Felleisen (Rice University) Christopher Haynes (Indiana University) ======================================================================== From cat-dist@mta.ca Fri Feb 2 14:57:31 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09526; Fri, 2 Feb 1996 14:57:30 -0400 Date: Fri, 2 Feb 1996 14:55:46 -0400 (AST) From: categories To: categories Subject: Preprints Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 2 Feb 1996 10:29:02 +0100 From: Marco Grandis The following two preprints will soon be available. A "hard" copy will be sent on request. With best regards, Marco Grandis Dipartimento di Matematica Universita' di Genova Via Dodecaneso 35 16146 Genova, Italy (E-mail: grandis@dima.unige.it) *** 1. M. Grandis, Categorically algebraic foundations for homotopical algebra, Dip. Mat. Univ. Genova, Preprint 293 (1996). Abstract. We investigate a structure for an abstract cylinder endofunctor I which produces a good basis for homotopical algebra. It essentially consists of the usual operations (faces, degeneracies, connections, symmetries, composition) together with a transformation I^2 -> I^2, which we call lens collapse after its realisation in the standard topological case. This structure, if somewhat heavy, has the interest of being "categorically algebraic", i.e. based on operations on functors. Consequently, it can be naturally lifted from a category A to its categories of diagrams A^S and its slice categories A\X, A/X. Further, the dual structure, based on a cocylinder (or path) endofunctor P can be lifted to the category of A-valued sheaves on a site, whenever P preserves limits, and to the category of internal monoids in A, with respect to any monoidal structure of A consistent with P. 2. M. Grandis, On the homotopy structure of strongly homotopy associative differential algebras, Dip. Mat. Univ. Genova, Preprint 294 (1996). Abstract. We study here the homotopy structure of Shad, the category of strongly homotopy associative d-algebras (shad-algebras for short), also called A_infinity-algebras and introduced by Stasheff ([St], 1963) for the study of the singular complex of the loop-space of a pointed topological space. Shad extends the category Da of associative differential (graded) algebras, by allowing for a homotopy relaxation of objects and morphisms, up to systems of homotopies of arbitrary degree. The better known category Dash of associative differential algebras and strongly homotopy multiplicative maps (Stasheff-Halperin [StH], Munkholm [Mu1-4]), having strict objects (the ones of Da) and lax morphisms (the ones of Shad) is intermediate between them. A crucial advantage of Shad over its subcategories Dash and Da is the homotopy invariance property proved by Gugenheim - Stasheff [GuS]. In order to study shad-homotopies of any order and their operations, the usual cocylinder functor of d-algebras is here extended to Shad, where we construct the vertical composition and reversion of homotopies (also existing in Dash, but not in Da) and homotopy pullbacks (which exist in Da, but not in Dash). Shad acquires thus a laxified version of the homotopy structure studied by the author in previous works; the main results therein, developing homotopical algebra from the Puppe sequence to stabilisation and triangulated structures, can very likely be extended to the new axioms, so to be available for Shad. From cat-dist@mta.ca Fri Feb 2 14:57:31 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09095; Fri, 2 Feb 1996 14:57:31 -0400 Date: Fri, 2 Feb 1996 14:56:29 -0400 (AST) From: categories To: categories Subject: Lectureship in Computer Science Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 2 Feb 96 09:33:44 GMT From: Roy L. Crole LEICESTER UNIVERSITY, UK, DEPARTMENT OF MATHEMATICS & COMPUTER SCIENCE Lectureship in Computer Science Applications are invited for a Lectureship in Computer Science in the Department of Mathematics and Computer Science. This post is tenable from 1 October 1996 or as soon as possible thereafter. The Department of Mathematics and Computer Science is divided into four groups: Pure Mathematics, Applied Mathematics, Computer Science and Statistics. The Computer Science Group has recently appointed three new lecturers, and will consist of nine members of staff when Iain A. Stewart takes up his appointment as Professor of Computer Science in March 1996. This lectureship is intended to strengthen the group with regard to both teaching and research. The group aims to expand even further in the near future. The Computer Science Group is firmly research oriented and current research interests include: artificial intelligence and expert systems; categorical logic; complexity theory; concurrency theory; fault-tolerant, real-time and dependable systems; finite model theory; formal languages and automata theory; formal methods for software development and programming language design; information systems; software engineering; type theory. The successful applicant will be ambitious, able to develop their own research within a multi-faceted environment, and have a strong research record and potential. There is no restriction regarding the area of research, and applicants with expertise in any area of Computer Science, and not just those listed above, are welcomed. The new lecturer will be required to teach at undergraduate and postgraduate level, and to perform administrative duties as directed by the Head of Department. There will be ample scope for a person of energy, drive and ambition to assume a rewarding role in a young and dynamic department. Initial salary, dependent upon qualifications and experience, will be on the Lecturer Grade A scale 15,154 to 19,848 p.a. Candidates who are interested in the lectureship are invited, if they so wish, to contact Professor Iain Stewart (telephone +44 (0)1792 295397, e-mail i.a.stewart@swansea.ac.uk) or Dr Rick Thomas (telephone +44 (0)116 252 3411, email rmt@mcs.le.ac.uk), who would be pleased to discuss the lectureship further. Information is also available on the WWW [http://www.mcs.le.ac.uk]. Further particulars and application forms are available from the Personnel and Planning Office (Academic Appointments), University of Leicester, University Road, LEICESTER, LE1 7RH, United Kingdom. Telephone +44 (0)116 252 2758. The closing date for applications is 29th March 1996. Please quote reference A5058. From cat-dist@mta.ca Tue Feb 6 21:39:41 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA11155; Tue, 6 Feb 1996 21:39:40 -0400 Date: Tue, 6 Feb 1996 21:35:08 -0400 (AST) From: categories To: categories Subject: Seminar in Honour of Max Kelly Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 7 Feb 1996 11:14:48 +1100 From: Ross Street SEMINAR IN HONOUR OF MAX KELLY There will be a two day seminar at the University of Sydney to honour Max Kelly on the occasion of his retirement. The dates are 12-13 March 1996. I am pleased to announce that George Janelidze, Peter Johnstone, Andre Joyal, and a number of Sydney and Macquarie University category theorists, have accepted invitations to lecture. On Tuesday 12 March, there will be a dinner held at the Art Gallery on the 5th Floor of the Wentworth Building at Sydney University. Please let Sonia Morr ( or 61-2-351-5809) know if you would like to attend. The charge is $40 per person. Bob Walters and I would be very happy to hear from other interested mathematicians who are able to attend the seminar. Sincerely, Ross From cat-dist@mta.ca Tue Feb 6 21:40:00 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA10011; Tue, 6 Feb 1996 21:39:59 -0400 Date: Tue, 6 Feb 1996 21:36:17 -0400 (AST) From: categories To: categories Subject: vanishing of derived functors of inverse limit Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 6 Feb 1996 20:08:27 -0500 (EST) From: Dan Christensen Dear category theorists, I have been working on a problem in stable homotopy theory that led to a question about the vanishing of the higher derived functors of the inverse limit functor. I was wondering if anyone on this list can answer it. Let G be any abelian group and let {G_\alpha} be the filtered diagram of all the finitely generated subgroups of G. Apply a contravariant additive functor T : Ab --> Ab to the diagram to produce {T G_\alpha}. Is it always true that lim^i T G_\alpha is zero for i at least 2? If G is countable, then this is true, and if T takes finitely generated groups to finitely generated groups, then it is true. But is it true in general? I should say that I have certain examples of T that I care about, namely TA = [HA,HB]_k (k and B fixed), the abelian group of maps from HA, the Eilenberg-Mac Lane spectrum with group A in dimension 0, to \Sigma^k HB, the E-M spectrum with group B in dimension k. However, I was hoping that it would be enough to use the abstract information we have. For example, the shape of the inverse system is "Noetherian" in a certain sense (because it comes from a diagram of finitely generated subgroups of a group) and while the objects in the diagram need not be finitely generated, they are finite sums of abelian groups chosen from a countable list. Thanks for any help or references you can provide. I have looked through several things written by Roos, Jensen and others and nothing answers the question either positively or negatively. Dan Christensen jdchrist@mit.edu From cat-dist@mta.ca Wed Feb 7 09:39:13 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA23708; Wed, 7 Feb 1996 09:39:13 -0400 Date: Wed, 7 Feb 1996 09:38:07 -0400 (AST) From: categories To: categories Subject: The Kelly Dinner Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 7 Feb 1996 12:30:35 +1100 From: Ross Street A REQUEST FOR CONTRIBUTIONS As previously announced, there will be a Seminar for Max Kelly on 12-13 March. On the Tuesday night there will be a dinner at which some words will be spoken. Because so many category theorists will be unable to attend the seminar and dinner, I decided to ask those of you who know Max personally, or have been influenced by his mathematical research, to send me some thoughts about Max that I can share with the people at the dinner. I have in mind between a few sentences and two paragraphs in length. Max is very proud of his international contacts and friends so I think this would be a very fitting tribute to him. Please send your contributions to me at . I look forward to hearing from you, if possible, before the end of February. Kind regards, Ross PS We are trying to avoid having this message sent to Max. From cat-dist@mta.ca Wed Feb 7 10:24:00 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA01331; Wed, 7 Feb 1996 10:23:59 -0400 Date: Wed, 7 Feb 1996 10:23:13 -0400 (AST) From: categories To: categories Subject: 3rd WoLLIC'96 - third call Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 7 Feb 96 11:10:38 EST From: Ruy de Queiroz PLEASE POST ** PLEASE POST ** PLEASE POST ** PLEASE POST ** PLEASE POST Third Call for Contributions 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil The `3rd Workshop on Logic, Language, Information and Computation' (WoLLIC'96) will be held in Salvador, Bahia (Brazil), from the 8th to the 10th May 1996. Contributions are invited in the form of two-page (600 words) abstracts in 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 artificial intelligence, automated deduction, foundations of logic programming, logic and computation, and logic engineering. There will be a number of guest speakers, including: Andreas Blass (Ann Arbor), Nachum Dershowitz (Urbana-Champaign), J. Michael Dunn (Indiana), Peter G"ardenfors (Lund), Jeroen Groenendijk (Amsterdam), Wilfrid Hodges (London), Roger Maddux (Ames, Iowa), Andrew Pitts (Cambridge), Amir Pnueli (Rehovot), Michael Smyth (London). WoLLIC'96 is part of a larger biennial event in computer science being held in the campus of the Federal University of Bahia from the 6th to the 10th of May 1996: the `6th SEMINFO' (6th Informatics Week). The 6th SEMINFO will involve parallel sessions, tutorials, mini-courses, as well as the XI Brazilian Conference on Mathematical Logic (EBL'96), and a Workshop on Distributed Systems (WoSiD'96). Submission: Two-page abstracts, preferably by e-mail to *** wollic96@di.ufpe.br *** must be RECEIVED by MARCH 8th, 1996 by the Chair of the Organising Committee. Authors will be notified of acceptance by April 8th, 1996. The 3rd WoLLIC'96 is under the official auspices of the Interest Group in Pure and Applied Logics (IGPL) and The European Association for Logic, Language and Information (FoLLI). Abstracts will be published in the Journal of the IGPL (ISSN 0945-9103) (up to now produced and distributed by Imperial College, London, and Max-Planck-Institut, Saarbruecken, but soon to be distributed by Oxford University Press) as part of the meeting report. Selected contributed papers will be invited for submission (in full version) to a special issue of the Journal (http://www.mpi-sb.mpg.de/igpl/Journal). The location: Salvador, Capital of the Bahia state, the first European settlement of Portuguese America and the first Capital of Brazil, is where all the most important colonial buildings were constructed: churches, convents, palaces, forts and many other monuments. Part of the city historical center has been safekept by UNESCO since 1985. Five hundred years of blending Native American, Portuguese, and African influences have left a rich culture to its people, which can be felt on its music, food, and mysticism. Salvador is located on the northeastern coast of Brazil and the sun shines year round with the average temperature of 25 degrees Celsius. It is surrounded by palm trees and beaches with warm water. City population is around 2.5 million and life style is quite relaxed. Programme Committee: W. A. Carnielli (UNICAMP, Campinas), M. Costa (EMBRAPA, Brasilia), V. de Paiva (Cambridge Univ., UK), R. de Queiroz (UFPE, Recife), A. Haeberer (PUC, Rio), T. Pequeno (UFC, Fortaleza), L. C. Pereira (PUC, Rio), K. Segerberg (Uppsala Univ., Sweden), A. M. Sette (UNICAMP, Campinas), P. Veloso (PUC, Rio). Organising Committee: H. Benatti (UFPE), L. S. Baptista (UFPE), A. Duran (UFBA), T. Monteiro (UFPE), A. G. de Oliveira (UFBA), N. Riccio (UFBA). For further information, contact the Chair of Organising Committee: R. de Queiroz, Departamento de Informatica, Universidade Federal de Pernambuco (UFPE) em Recife, Caixa Postal 7851, Recife, PE 50732-970, Brazil, e-mail: ruy@di.ufpe.br, tel.: +55 81 271 8430, fax: +55 81 271 8438. (Co-Chair: T. Pequeno, LIA, UFC, tarcisio@lia.ufc.br, fax +55 85 288 9845) Web homepage: http://www.di.ufpe.br/simposios/wollic.html -------------------------------------------------------------------------------- 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96) May 8-10, 1996 Salvador (Bahia), Brazil TITLE AND ABSTRACT OF INVITED TALKS -------------------------------------------------------------------------------- Some Semantical Aspects of Linear Logic Andreas Blass I plan to discuss some of the semantics that have been proposed for Girard's linear logic, including different forms of game semantics, de Paiva's Dialectica-like semantics, and perhaps others. I shall describe how these semantics are related to each other, to the intuitions that underlie linear logic, and to some other parts of mathematics. -------------------------------------------------------------------------------- Trees, Ordinals, and Termination Nachum Dershowitz Trees are a natural representation for countable ordinals. We describe natural well-founded orderings of finite binary trees, finite ordered (plane-planted) trees, rational binary trees (finite or infinite binary trees with only finitely many different subtrees), and "supertrees" (trees whose nodes may themselves be supertrees). We relate these orderings to existing ordinal notations, and illustrate their use in various colorful termination problems. -------------------------------------------------------------------------------- Proof Theory and Semantics for Structurally Free Logics J. Michael Dunn This work is joint with R. K. Meyer. The idea is to provide a semantics and proof theory for combinatory logic, extended by a "residual" (implication). The semantics is a variation on the ternary relational (Meyer-Routley) semantics for relevance logic, as extended by Meyer-Routley, and more recently others for the (fusion-implication) fragment of the relevance logic B+ (closely related to the non-associative Lambek calculus). The proof-theory extends some semi-published work of Meyer in the 1970's (following a suggestion of Belnap), wherein Gentzen's structural rules for the intuitionistic implication calculus were replacewith explicit introduction of a combinator licensing the combinatorial manipulations. This is extended so as to make combinators "first-class objects," and a cut theorem can still be proven. This is called "structurally free logic" in analogy with "logic freed of existential presppositions." In this original "free logic," existence presuppositions are made explicit, just as in "combinatorially free logic" combinatorial moves are made explicit by adding the combinators that license them as explicit premisses in the antecedent of the sequent. This allows various logics to be translated into the combinatorially free logic. It also expands the meaning of "substructural logics" beyond the usual ones obtained by considering various subsets of Gentzen's structural rules (plus say associativity). There will also be results about adding other connectives (conjunction and disjunction), with or without distribution. -------------------------------------------------------------------------------- TBA Peter G"ardenfors -------------------------------------------------------------------------------- Update Semantics Meets Discourse Jeroen Groenendijk In update semantics the meaning of a sentence is identified with its potential to change the information state of an agent. In the recursive semantic definition, truth conditions are replaced by update effects. Central notions are not truth and validity, but consistency, support, and coherence. Although update semantics is advertized as addressing itself to the interpretation of discourse, rather than being limited to single sentences, it usually goes no further than interpreting sequences of utterances of a single agent. In the present talk I will study the interpretation of multi-agent discourse. The object language we investigate is the language of modal predicate logic. We concentrate on the role of (epistemic) modalities in discourse, and on anaphoric relations (binding of variables) across utterances of different speakers. The aim is to characterize notions of logical consistency and coherence of multi-agent discourse. The paper reports on joint work with Martin Stokhof and Frank Veltman. -------------------------------------------------------------------------------- TBA Wilfrid Hodges -------------------------------------------------------------------------------- TBA Roger Maddux -------------------------------------------------------------------------------- TBA Andrew Pitts -------------------------------------------------------------------------------- Verifying Timed and Hybrid Systems Amir Pnueli The talk presents new computational models for real-time and hybrid systems. For timed systems we propose a model called A Clocked Transition System (CTSS). The CTSS model is a development of our previous Timed Transition model, where some of the changes are inspired by the model of Timed Automata. The new models lead to a simpler style of temporal specification and verification, requiring no extension of the temporal language. We present verification rules for proving safety properties (including time-bounded response properties) of clocked transition systems, and separate rules for proving (time-unbounded) response properties. To justify the need for time-unbounded resopnse rules, we present a characteristic example of a timed system which terminates but no apriori bound on its termination time can be given All rules are associated with verification diagrams. The verification of RESPONSE properties requires adjustments of the proof rules developed for untimed systems, reflecting the fact that progress in the real time systems is ensured by the progress of time and not by fairness. The style of the verification rules is very close to the verification style of untimed systems which allows the (re)use of verification methods and tools, developed for untimed reactive systems, for proving properties of real-time systems. We conclude with the presentation of a branching-time based approach for verifying that an arbitrary given CTSS is Non-Zeno. This is joint work with Y. Kesten and Z. Manna. -------------------------------------------------------------------------------- TBA Michael Smyth -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- \documentstyle[a4]{article} \renewcommand{\thepage}{} \begin{document} \begin{center} {\large\bf 3rd Workshop on Logic, Language, Information and Computation (WoLLIC'96)}\\[1.0ex] {\large May 8--10, 1996}\\[.8ex] {\large Salvador (Bahia), Brazil}\\[1.0ex] \end{center} \bigskip \noindent The {\bf 3rd Workshop on Logic, Language, Information and Computation} ({\bf WoLLIC'96}) will be held in Salvador, Bahia (Brazil), from the 8th to the 10th May 1996. Contributions are invited in the form of two-page (600 words) abstracts in 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 artificial intelligence, automated deduction, foundations of logic programming, logic and computation, and logic engineering.\\ There will be a number of guest speakers, including:\\ Andreas Blass (Ann Arbor), Nachum Dershowitz (Urbana-Champaign), J.\ Michael Dunn (Indiana), Peter G\"ardenfors (Lund), Jeroen Groenendijk (Amsterdam), Wilfrid Hodges (London), Roger Maddux (Ames, Iowa), Andrew Pitts (Cambridge), Amir Pnueli (Rehovot), Michael Smyth (London)\\ {\bf WoLLIC'96} is part of a larger biennial event in computer science being held in the campus of the Federal University of Bahia from the 6th to the 10th of May 1996: the {\bf 6th SEMINFO} (6th Informatics Week). The {\bf 6th SEMINFO} will involve parallel sessions, tutorials, mini-courses, as well as the {\bf XI Brazilian Conference on Mathematical Logic} ({\bf EBL'96}), and a {\bf Workshop on Distributed Systems} ({\bf WoSiD'96}).\\ {\bf Submission}: Two-page abstracts, preferably by e-mail to ***~wollic96@di.ufpe.br~*** must be RECEIVED by MARCH 8th, 1996 by the Chair of the Organising Committee. Authors will be notified of acceptance by April 8th, 1996. The {\bf 3rd WoLLIC'96} is officially sponsored by the Interest Group in Pure and Applied Logics (IGPL) and The European Association for Logic, Language and Information (FoLLI). The {\bf EBL'96} is the annual meeting of Brazilian Logic Society. Abstracts will be published in the Journal of the IGPL (ISSN 0945-9103) (up to now produced and distributed by Imperial College, London, and Max-Planck-Institut, Saarbr\"ucken, but soon to be distributed by Oxford University Press) as part of the meeting report. Selected contributed papers will be invited for submission (in full version) to a special issue of the Journal (http://www.mpi-sb.mpg.de/igpl/Journal).\\ {\bf The location}: Salvador, Capital of the Bahia state, the first European settlement of Portuguese America and the first Capital of Brazil, is where all the most important colonial buildings were constructed: churches, convents, palaces, forts and many other monuments. Part of the city historical center has been safekept by UNESCO since 1985. Five hundred years of blending Native American, Portuguese, and African influences have left a rich culture to its people, which can be felt on its music, food, and mysticism. Salvador is located on the northeastern coast of Brazil and the sun shines year round with the average temperature of 25 degrees Celsius. It is surrounded by palm trees and beaches with warm water. City population is around 2.5 million and life style is quite relaxed.\\ {\bf Programme Committee}: W.\ A.\ Carnielli (UNICAMP, Campinas), M.\ Costa (EMBRAPA, Brasilia), V.\ de Paiva (Cambridge Univ., UK), R.\ de Queiroz (UFPE, Recife), A.\ Haeberer (PUC, Rio), T.\ Pequeno (UFC, Fortaleza), L.\ C.\ Pereira (PUC, Rio), K.\ Segerberg (Uppsala Univ., Sweden), A.\ M.\ Sette (UNICAMP, Campinas), P.\ Veloso (PUC, Rio).\\ {\bf Organising Committee}: H.\ Benatti (UFPE), L.\ S.\ Baptista (UFPE), A.\ Duran (UFBA), T.\ Monteiro (UFPE), A.\ G.\ de Oliveira (UFBA), N.\ Riccio (UFBA).\\ For further information, contact the Chair of Organising Committee: R.\ de Queiroz, Departamento de Inform\'atica, Universidade Federal de Pernambuco (UFPE) em Recife, Caixa Postal 7851, Recife, PE 50732-970, Brazil, e-mail: ruy@di.ufpe.br, tel: +55~81~271~8430, fax +55~81~271~8438. (Co-Chair: T.\ Pequeno, LIA, UFC, tarcisio@lia1.ufc.br, fax +55~85~288~9845)\\ Web homepage: http://www.di.ufpe.br/simposios/wollic.html \end{document} From cat-dist@mta.ca Tue Feb 13 09:01:41 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA32492; Tue, 13 Feb 1996 09:01:41 -0400 Date: Tue, 13 Feb 1996 09:00:06 -0400 (AST) From: categories To: categories Subject: H-Day Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 13 Feb 1996 07:31:11 -0500 From: Peter Freyd I remember the time when the only people who could pronounce the word "functor" without either a sneer or an apologetic little snort were a few homological algebraists. The first exception I knew was Paul Halmos. Among other things, he became the single best salesman for my first book. All of which is a preamble for my forwarding of the following: Date: Mon, 12 Feb 1996 16:49:29 -0600 From: gillman@MAIL.UTEXAS.EDU (Leonard Gillman) Subject: Halmos = 80 As you may know, Paul will celebrate his 80th birthday on Sunday March 3rd. I am organizing an email blitz for the occasion, the idea being to deluge the old gent on that day with electronic birthday greetings from near and far. You are invited to join the fun. Halmos's address is phalmos@scuacc.scu.edu We are all allowed to add any other mathematicians (or nonmathematicians) we think of. Duplications are inevitable in any case, but that is no problem. I suggest notifying people at least a week in advance of H-Day. People without access to email on a Sunday should wait until Monday the 4th to send their greetings. Len ================== ================== Leonard Gillman 1606 The High Road gillman@mail.utexas.edu Austin TX 78746-2236 Fax 512-327-2274 (new) Tel 512-327-2277 From cat-dist@mta.ca Tue Feb 13 09:02:03 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA31972; Tue, 13 Feb 1996 09:02:03 -0400 Date: Tue, 13 Feb 1996 09:01:08 -0400 (AST) From: categories To: categories Subject: CAAP/ESOP/CC Programme-Registration Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 13 Feb 1996 13:44:10 +0100 From: Helene Kirchner CALL FOR PARTICIPATION European Symposium on Programming (ESOP'96) 22--24 April Colloquium on Trees in Algebra and Programming (CAAP'96) 22--24 April International Conference on Compiler Construction (CC'96) 24--26 April Linkvping Sweden April 1996 In cooperation with IFIP Note: Early registration deadline - March 15 CAAP/ESOP/CC PROGRAMME ======================= Sunday April 21 --------------- 17.00 - 21.00 REGISTRATION AND RECEPTION (at Frimurarehotellet) Monday April 22 --------------- 09.00 - 10.00 CA1 Invited speaker: S. Abramsky Semantics of interaction 10.00 - 10.30 E1 F. Bueno, D. Cabeza, M. Hermenegildo, G. Puebla Global Analysis of Standard Prolog Programs CA2 A. Bottreau, Y. Mitivier The Kronecker product and local computations in graphs 10.30 - 11.00 COFFEE BREAK 11.00 - 11.30 E2 H. Seidl Integer Constraints to Stop Deforestation CA3 M. Madonia, S. Varricchio Iterative pairs and multitape automata 11.30 - 12.00 E3 T. Jensen, I. Mackie Flow Analysis in the Geometry of Interaction CA4 A. Boudet, H. Comon Diophantine Equations, Presburger Arithmetic and Finite Automata 12.00 - 12.30 E4 R. Giacobazzi, F. Ranzato Compositional Optimization of Disjunctive Abstract Interpretations CA5 A. K|hnemann A pumping Lemma for Output Languages of Macro Tree Transducers 12.30 - 14.00 LUNCH 14.00 - 15.00 E5 C.B. Jones Some Practical Problems and their Influence on Semantics 15.00 - 15.30 E6 F. Maraninchi, N. Halbwachs Compositional Semantics of Non-deterministic Synchronous Languages CA6 D. Merlini, R. Sprugnoli, M.C. Verri The area determined by underdiagonal lattice paths 15.30 - 16.00 COFFEE BREAK 16.00 - 16.30 E7 R. Barbuti, P. Mancarella A Multiple-valued Logical Semantics for Prolog CA7 Y. Takayama Extraction of Concurrent Processes from Higher Dimensional Automata 16.30 - 17.00 E8 M. Alpuente, M. Falaschi, G. Vidal Narrowing-driven Partial Evaluation of Functional Logic Programs CA8 R. Kaivola Axiomatising Extended Computation Tree Logic 17.00 - 17.30 E9 D. Bechet Removing Value Encoding using Alternative Values in Partial Evaluation of Strongly-Typed Languages CA9 M. Lenisa Final Semantics for a Higher Order Concurrent Language Tuesday April 23 ---------------- 09.00 - 10.00 CA10 F. Pfenning The practice of logical framework 10.00 - 10.30 E10 E. Goubault Durations for Truly-concurrent Transitions CA11 L. Bachmair, T. Chen, C.R. Ramakrishnan, I.V. Ramakrishnan Subsumption Algorithms Based on Search Trees 10.30 - 11.00 COFFEE BREAK 11.00 - 11.30 E11 K. Stxlen Assumption/Commitment Rules for Data-flow Networks - with an Emphasis on Completeness CA12 M. Fernandez, I. Mackie Interaction Nets and Term Rewriting Systems 11.30 - 12.00 E12 S. Melzer, J. Esparza Checking System Properties via Integer Programming CA13 B. Lisper Computing in Unpredictable Environments: Semantics, Reduction Strategies, and Program Transformations 12.00 - 12.30 E13 U. Montanari, M. Pistore, D. Yankelevich Efficient Minimization up to Location Equivalence CA14 J. Glauert, Z. Khasidashvili Relative Normalization in Deterministic Residual Structures 12.30 - 14.00 LUNCH 14.00 - 14.30 E14 G. Smith, D. Volpano Towards an ML-style Polymorphic Type System for C CA15 T. Arts Termination by absence of infinite chains of dependency pairs 14.30 - 15.00 E15 P. Fradet, R. Gaugne, D. Le Mitayer Static Detection of Pointer Errors: an Axiomatisation and a Checking Algorithm CA16 B. Gramlich Confluence without Termination via Parallel Critical Pairs 15.00 - 15.30 E16 E. Rohwedder, F. Pfenning Mode and Termination Checking for Higher-Order Logic Programs CA17 E.A. Cichon, H. Touzet An Ordinal Calculus for Proving Termination in Term Rewriting 15.30 - 16.00 COFFEE BREAK 16.00 - 16.30 E17 J. Palsberg, B. Patt-Shamir, K. Lieberherr A New Approach to Compiling Adaptive Programs CA18 M. Bidoit, A. Tarlecki Behavioural satisfaction and equivalence in concrete model categories 16.30 - 17.00 E18 S. Liang, P. Hudak Modular Denotational Semantics for Compiler Construction CA19 A. Cheng, M. Nielsen Open Maps, Behavioural Equivalences, and Congruences 17.00 - 17.30 E19 E. Rose Linear Time Hierarchies for a Functional Language Machine Model CA20 A. Rensink Denotational, Causal and Operational Determinism in Event Structures 17.30 - 18.00 E20 M. Thuni, K. Ehlander Towards an expressive language for PDE solvers 19.00 CONFERENCE DINNER Wednesday April 24 ------------------ 09.00 - 10.00 E21 Invited speaker: S.L. Peyton Jones Compiling Haskell by Transformation 10.00 - 10.30 E22 J. Launchbury, R. Paterson Parametricity and Unboxing with Unpointed Types CC1 G. Riedewald CC conferences - the first decade 10.30 - 11.00 COFFEE BREAK 11.00 - 11.30 E23 J.C. Gonzalez-Moreno, M.T. Hortala-Gonzalez, F.J. Lspez-Fraguas, M. Rodrmguez-Artalejo A Rewriting Logic for Declarative Programming CC2 J. Wang, G.R. Gao Pipelining-Dovetailing: A Transformation to Enhance Software Pipelining Performance for Nested Loops 11.30 - 12.00 E24 J.A. Bergstra, T.B. Dinesh, J. Field, J. Heering A Complete Transformational Toolkit for Compilers CC3 P. Pfahler, G. Piepenbrock A Comparison of Modulo Scheduling Techniques for Software Pipelining 12.00 - 12.30 E25 S. van Bakel, F. Barbanera, M. Fernandez Rewrite Systems with Abstraction and beta-rule: Types, Approximants and Normalization CC4 M.A. Ertl, A. Krall Removing Anti Dependences by Repairing 12.30 - 14.00 LUNCH 14.00 - 14.30 CA21 M.H. Sxrensen Effective Longest and Infinite Reduction Paths in Untyped lambda-Calculi CC5 J. Janssen Controlled Node Splitting 14.30 - 15.00 CA22 G. Boudol, C. Lavatelli Full abstraction for lambda calculus with resources and convergence testing CC6 J.W. Davidson, S. Jinturkar Aggressive loop unrolling in a retargetable, optimizing compiler 15.00 - 15.30 CA23 J. Tiuryn, M. Wand Untyped Lambda-Calculus with Input-Output CC7 C. Verbrugge, P. Co, L.J. Hendren Generalized Constant Propagation: A Study in C 15.30 - 16.00 COFFEE BREAK 16.00 - 16.30 CC8 C. Cifuentes Structuring Decompiled Graphs 16.30 - 17.00 CC9 A. Geser, J. Knoop, G. Luttgen, O. Ruthing, B. Steffen Non-monotone Fixpoint Iterations to resolve Second Order Effects 17.00 - 17.30 CC10 U. Assmann How to Uniformly Specify Program Analysis and Transformation with Graph Rewrite Systems 17.30 - 18.00 CC11 B. Steensgaard Points-to Analysis by Type Inference of Programs with Structures and Unions 19.00 DEMO SESSION AND BUFFET (at the Department of Computer and Information Science) Thursday April 25 ----------------- 09.00 - 10.00 CC12 Invited speaker: W. Waite Compiler Construction: Craftsmanship or Engineering? 10.00 - 10.30 CC13 A. Nymeyer, J-P. Katoen, Y. Westra, H. Alblas Code Generation = A* + BURS 10.30 - 11.00 COFFEE BREAK 11.00 - 11.30 CC14 M. Pettersson A Compiler for Natural Semantics 11.30 - 12.00 CC15 D. Boucher, M. Feeley Abstract compilation: a new implementation paradigm for static analysis 12.00 - 12.30 CC16 D.J. Salomon Using Partial Evaluation in Support of Portability, Reusability, and Maintainability 12.30 - 14.00 LUNCH 14.00 - 14.30 CC17 J-D. Choi, V. Sarkar, E. Schonberg Incremental Computation of Static Single Assignment Form 14.30 - 15.00 CC18 Z. Li, C. Kirkham Efficient Storage Reuse of Aggregates in Single Assignment Languages 15.00 - 15.30 CC19 F. Chow, S. Chan, S-M. Liu, R. Lo, M. Streich Effective Representation of Aliases and Indirect Memory Operations in SSA Form 15.30 - 16.00 COFFEE BREAK 16.00 - 18.00 POSTER SESSION 19.00 CONFERENCE DINNER Friday April 26 --------------- 09.00 - 09.30 CC20 B.M. Kadhim, W.M. Waite Maptool - Supporting Incremental Syntax Development 09.30 - 10.00 CC21 P. McLean, R.N. Horspool A faster Earley Parser 10.00 - 10.30 CC22 T.A. Proebsting, B.R. Whaley One-Pass, Optimal Tree Parsing - With Or Without Trees 10.30 - 11.00 COFFEE BREAK 11.00 - 11.30 CC23 J. Vitek, R.N. Horspool Compact Dispatch Tables for Dynamically Typed Object Oriented Languages 11.30 - 12.00 CC24 J. Bosch Delegating Compiler Objects - An Object-Oriented Approach to Crafting Compilers 12.00 - 12.30 CC25 P. Fritzson, R. Wism|ller, O. Hansen, J. Sala, P. Skov A Parallel Debugger with Support for Distributed Arrays, Multiple Executables, and Dynamic Processes Please see the separate description for the Friday afternoon satellite meetings. Quick Overview -------------- +----------------------------------------------------+ | Mon | Tue | Wed | Thu | Fri | |----------------------------------------------------| 09.00 - | CA1 | CA10 | E21 | CC12 | CC20 | 09.30 - | - " - | - " - | - " - | - " - | CC21 | 10.00 - | E1 CA2 | E10 CA11 | E22 CC1 | CC13 | CC22 | 10.30 - | COFFEE BREAK | 11.00 - | E2 CA3 | E11 CA12 | E23 CC2 | CC14 | CC23 | 11.30 - | E3 CA4 | E12 CA13 | E24 CC3 | CC15 | CC24 | 12.00 - | E4 CA5 | E13 CA14 | E25 CC4 | CC16 | CC25 | 12.30 - | LUNCH |--------+ 14.00 - | E5 | E14 CA15 | CA21 CC5 | CC17 | 14.30 - | - " - | E15 CA16 | CA22 CC6 | CC18 | 15.00 - | E6 CA6 | E16 CA17 | CA23 CC7 | CC19 | 15.30 - | COFFEE BREAK | 16.00 - | E7 CA7 | E17 CA18 | CC8 | POSTER | 16.30 - | E8 CA8 | E18 CA19 | CC9 | | 17.00 - | E9 CA9 | E19 CA20 | CC10 | | 17.30 - | | E20 | CC11 | | 18.00 +-------------------------------------------+ 19.00 | | DINNER | DEMO | DINNER | +-------------------------------------------+ Demonstrations -------------- A number of systems will be demonstrated during the course of the conference. The demonstrations and buffet will take place at the Department of Computer and Information Science. There is still space available and it may be possible to arrange for equipment for the demonstrations. Contact point below. Note that a fee will be charged for commercial exhibitions. CAAP/ESOP/CC'96 attn. Mikael Pettersson Department of Computer and Information Science Linkvping University S-581 83 Linkvping SWEDEN Telephone: +46 13 26 83 Telefax: +46 13 28 44 99 E-mail: mpe@ida.liu.se Venue ----- The CAAP/ESOP/CC conferences will be hosted by Linkvping University in April 1996. Organised by the Programming Environments Laboratory at the Department of Computer and Information Science, the conferences will be held in the Collegium building at the Mjdrdevi Science Park, near the University campus. Accommodation is available at several downtown hotels. Linkvping is the fifth largest city in Sweden and has about 130,000 inhabitants. It is located about 200 kilometres southwest of Stockholm, the capital of Sweden. There are airports in Linkvping and Norrkvping (40 kilometres from Linkvping) with regular flights from Copenhagen and Stockholm. One of the main railways runs from Stockholm through Norrkvping, Linkvping and further to Malmv in the south of Sweden. There are also direct train connections from several European cities. The weather is in general unpredictable. Temperatures in spring can vary between 5 and 150C. You are best advised to bring several layers of clothing which can be put on and taken off as required. Registration ------------ The registration fee covers lunches, coffee breaks, conference dinner(s) and proceedings which are to be published by Springer-Verlag in the Lecture Notes in Computer Science series. Student fees cover lunches and proceedings, but not the conference dinner(s). Extra dinner tickets will be available for purchase at the conference. The registration desk is open on Sunday April 21 from 17 to 21 in the lobby of Frimurarehotellet, Monday April 22 from 8 to 9 in Collegium, and Wednesday April 24 from 8 to 9 in Collegium. The phone number to Collegium is +46 13 20 44 00. Accommodation ------------- We have reserved rooms at a number of downtown hotels. Rooms should be booked before April 1st, after that date no rooms are reserved. Note that you have to contact the hotels yourself for booking accommodation. Booking code and the conference name (or the name of our reference person: Ms. Gunilla Blom) must be given when contacting the hotel for booking. The hotels below have reserved rooms. Prices are per night. Ekoxen Hotell 40 single rooms at SEK 1080 Addr: Klostergatan 68 Booking code FI 651 Tel: +46 13 14 60 70 Fax: +46 13 12 19 03 Frimurarehotellet 75 single rooms at SEK 825 Addr: Sankt Larsgatan 14 Give the conference name Tel: +46 13 12 91 80 Fax: +46 13 13 95 44 Good Evening Hotel 65 single rooms at SEK 555 Addr: Hantverkaregatan 1 Booking code BI 365 Tel: +46 13 12 90 00 Fax: +46 13 13 88 50 Stora Hotellet 80 single rooms at SEK 810 Addr: Stora Torget 9 Booking code BI 364 Tel: +46 13 12 90 00 Fax: +46 13 13 37 69 Linkvpings Vandrarhem 3 single rooms at SEK 390, (youth hostel) 5 double rooms at SEK 470 Addr: Klostergatan 52A (SEK 235/person), 2 flats for 4 Tel: +46 13 14 90 90 persons each at SEK 210/person Fax: +46 13 14 83 00 Give the conference name Satellite meetings ------------------ Workshop on Compiler Techniques for Application Domain Languages and Extensible Language Models. Friday afternoon, April 26. Tentatively 14.00--18.00. Organisers: Jan Bosch (Jan.Bosch@ide.hk-r.se), and Gvrel Hedin (Gorel.Hedin@dna.lth.se). For more information, please contact the organisers or visit http://www.dna.lth.se/Research/CC96-ALEL/about.html The use of functional languages in industry - the Erlang experience, and other cases. Friday afternoon. Contact: Bengt Lennartsson (bln@ida.liu.se). For more information, see the web page below. Workshop on Term Rewriting and Tree Languages. Probably Thursday April 25. Organisers: Dieter Hofbauer (dieter@cs.tu-berlin.de) Sophie Tison (tison@lifl.fr) The workshops aim at providing a discussion forum for the exchange of ideas and experience in these areas. Participants are required to send a short position paper to one of the organisers before April 5th. WWW --- A word-wide-web page containing information about the conferences is reachable by URL: http://www.ida.liu.se/activities/conferences/CAAP-CC-ESOP96/ Administration -------------- Contact point for Conference administration: CAAP/ESOP/CC'96 attn. Ms. Gunilla Blom Department of Computer and Information Science Linkvping University S-581 83 Linkvping SWEDEN Telephone: +46 13 28 22 97 Telefax: +46 13 28 44 99 E-mail: gunli@ida.liu.se Chairpersons ------------ CAAP'96 chair: Hilhne Kirchner E-mail: caap96@loria.fr CC'96 chair: Tibor Gyimothy E-mail: cc96@inf.u-szeged.hu ESOP'96 chair: Hanne Riis Nielson E-mail: esop96@daimi.aau.dk Local arrangements chair: Peter Fritzson E-mail: conf96@ida.liu.se Payment ------- Registration fees should be paid by Eurocheque, cheque or bankdraft (in Swedish crowns drawn on a Swedish bank) or travellers cheques in Swedish crowns. We cannot accept bank transfers, credit cards or cheques drawn on non-Swedish banks or in currencies other than Swedish crowns. All payments must be made in advance, preferably enclosed with the registration form. For Swedish participants, we also have the possibility to send an invoice of the amount. Registration form ----------------- Return this form to: CAAP/ESOP/CC'96 attn. Ms. Gunilla Blom Department of Computer and Information Science Linkvping University S-581 83 Linkvping SWEDEN Telephone: +46 13 28 22 97 Telefax: +46 13 28 44 99 E-mail: gunli@ida.liu.se Name: ----------------------------------------------------------------- Address: ----------------------------------------------------------------- Affiliation: ----------------------------------------------------------------- Telephone: ----------------------------------------------------------------- Telefax: ----------------------------------------------------------------- E-mail: ----------------------------------------------------------------- Dietary restrictions: ----------------------------------------------------------------- Please check the relevant box. Early Late CAAP/ESOP, regular SEK 2450 [ ] SEK 2750 [ ] CAAP/ESOP, student SEK 1500 [ ] SEK 1750 [ ] CC, regular SEK 2200 [ ] SEK 2550 [ ] CC, student SEK 1450 [ ] SEK 1700 [ ] CAAP/ESOP & CC, regular SEK 4000 [ ] SEK 4550 [ ] CAAP/ESOP & CC, student SEK 2450 [ ] SEK 2750 [ ] Payment enclosed: SEK ----------------------------------------------------------------- Early registration forms must be received by 15th March 1996. Student registrations must include proof of status (e.g. copy of identity card or letter from advisor or supervisor). All cancellations received before 9th April 1996 will incur an administration charge of SEK 200. No refunds can be made for cancellations received after this date. From cat-dist@mta.ca Wed Feb 14 15:18:23 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA10223; Wed, 14 Feb 1996 15:18:22 -0400 Date: Wed, 14 Feb 1996 15:16:38 -0400 (AST) From: categories To: categories Subject: Preprint (announcement) Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Wed, 14 Feb 1996 13:12:33 +0100 From: Anders Kock The paper "Frame distributions, and support" by A. Kock and G.E,. Reyes is available by anonymous ftp : ftp://theory.doc.ic.ac.uk/papers/Kock where it appears as distr.ps.Z It is a slightly expanded version of the preprint with the same title, Universite de Montreal DMS No 386, janvier 1996. Abstract: We analyze in terms of constructive frame theory the relationship between support of distributions, regularization of opens, and "frame distributions" (sup lattice maps from a frame to the frame of truth values, as considered recently by Bunge and Funk). From cat-dist@mta.ca Thu Feb 15 11:14:38 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA02311; Thu, 15 Feb 1996 11:14:38 -0400 Date: Thu, 15 Feb 1996 11:13:46 -0400 (AST) From: categories To: categories Subject: Prolongation by zero (preprint) Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 15 Feb 1996 14:26:36 +0100 From: Anders Kock The preprint "Locally closed sublocales and prolongation by zero" is available by anonymous ftp from theory.doc.ic.ac.uk/papers/Kock where it appears as the file: loc-clo.ps (it is about 150 kb). Abstract: We prove that abelian group valued sheaves over a locally closed sublocale admit prolongation by zero, and that the prolongation functor has a right adjoint. The method is by left exact comonads; specifically, it uses a version of Artin-Wraith glueing, where one has to put glue on _both_ the items to be glued. From cat-dist@mta.ca Fri Feb 16 11:39:23 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA04351; Fri, 16 Feb 1996 11:39:22 -0400 Date: Fri, 16 Feb 1996 11:35:42 -0400 (AST) From: categories To: categories Subject: Research Position Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Thu, 15 Feb 1996 14:36:27 +0100 (MET) From: Matthew Hennessy UNIVERSITY OF SUSSEX RESEARCH FELLOW IN THE FOUNDATIONS OF COMPUTING A Research Fellow is required for a 3-year project entitled ``Foundations for the Integration of Concurrent Distributed and Functional Computation'', under the direction of Prof. M. Hennessy and funded by the EPSRC. The aim of the project is to - provide a uniform coherent semantic foundation for concurrent, distributed and functional behaviour; - develop proof methodologies for establishing properties of process descriptions expressed in specification languages using these paradigms; - develop prototypes of supporting verification systems. The project will start on 1/4/96 and salary will be related to the academic 1A scale. A Ph.D. in Computer Science or Mathematics or equivalent experience is required. In addition to normal research duties the successful candidate will be expected to provide some assistance to undergraduate teaching. More details of the project and the conditions of service are available at ftp://ftp.cogs.sussex.ac.uk/pub/users/matthewh/details.ps To apply please submit electronic applications to matthewh@cogs.sussex.ac.uk Applications should include a detailed curriculum vitae, names of three referees with their email addresses. From cat-dist@mta.ca Thu Feb 22 10:12:58 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA07202; Thu, 22 Feb 1996 10:12:58 -0400 Date: Thu, 22 Feb 1996 10:07:57 -0400 (AST) From: categories To: categories Subject: RESEARCH FELLOWSHIP Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 21 Feb 96 10:34:11 GMT From: Zhaohui.Luo@durham.ac.uk Department of Computer Science University of Durham Research Fellowship in Type Theory and its Applications to Theorem Proving Applications are invited for a post-doctoral research fellowship funded under the UK EPSRC research project "Subtyping, inheritance and reuse: developing expressive type theory for formal analysis". The area of work is computer-assisted formal reasoning based on type theory. The project is to develop expressive type theories with subtyping and inheritance mechanisms to support structuring and reuse of formal theories and proofs. The theoretical research results will be incorporated into proof development systems such as Lego and used in application case studies. The research fellowship is for a period of three years and available from May 1996. The appointment will be on the AR1A scale (starting salary from 15,986 to 18,294 pounds per annum, according to experience). Candidates would normally be expected to have a PhD in computer science or mathematics, or equivalent experience. Experience or background in areas such as constructive type theory, type systems for programming languages, formal proof development, or implementation of theorem provers, is considered to be desirable, though not necessary. The successful candidate will be working in an active research group at Durham with interests in both theory and application. He or she is also expected to have a close collaboration with the theorem proving group led by Prof. Rod Burstall at LFCS, Edinburgh (a collaborating partner of the above project) and other related institutions in Europe. Further details of the research project and related information can be found from the WWW page "http://www.dur.ac.uk/~dcs0zl/sir.html". Applications should include a curriculum vitae and names of two referees with their addresses (and email addresses if available). Please send applications or enquiries to Dr Zhaohui Luo Dept of Computer Science The Science Laboratories South Road Durham DH1 3LE, U.K. email: Zhaohui.Luo@durham.ac.uk tel: +44-(0)191-3743657 fax: +44-(0)191-3742560 From cat-dist@mta.ca Thu Feb 22 10:19:10 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA01264; Thu, 22 Feb 1996 10:19:09 -0400 Date: Thu, 22 Feb 1996 10:11:05 -0400 (AST) From: categories To: categories Subject: postdoc ad Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: RO X-Status: Date: Wed, 21 Feb 1996 15:27:56 +0100 From: I. Moerdijk Dear readers of the categories list: A postdoc position as described in the ad below will be available at our department. The description below is somewhat narrow, but I believe that any good candidate with background in algebraic topology will be considered.The starting date is negotiable, and January 1, 1997 could also be a possibility. If you are interested, or if you wish to suggest a candidate, please feel free to approach me directly by e-mail. Ieke Moerdijk. ---------------------------------------------------------- ---------------------------------------------------------- As of September 1996, there will be available a two year post doctoral position at the Mathematical Institute of the University of Utrecht. Holders of a Ph. D. degree in mathematics and those who will obtain such a degree before September 1996 are invited to apply. The positions are tied to a specific NWO (= Dutch Science Foundation) research project in topology, including the theory of foliations, orbifolds, equivariant cohomology, intersection cohomology (of related orbit spaces), C*-algebras and K-theory related to foliations, and related topics. The positions do not involve teaching. Applications should be sent before April 1, 1996, to the attention of the departmental secretary, K. Schoenmaker Mathematical Institute, University of Utrecht, P.O. Box 80.010, 3508 TA Utrecht, The Netherlands. Applications should include the usual items: a c.v., a brief description of past and current research and of the results obtained, a list of publications (if any), the names of mathematicians who will write letters of recommendation, and a research plan. Furthermore, at least two mathematicians must write a letter of recommendation to the address above, with the same deadline. ---------------------------------------------------------- ---------------------------------------------------------- From cat-dist@mta.ca Tue Feb 28 08:44:37 1995 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09552; Tue, 28 Feb 1995 08:44:37 -0400 Date: Tue, 28 Feb 1995 08:44:19 -0400 (AST) From: categories To: categories Subject: Paper available by ftp Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Tue, 27 Feb 1996 14:17:21 -0500 From: Robert A. G. Seely The following paper is available via ftp or WWW browser, at the URLs given after the abstract. Categories for computation in context and unified logic: I by R.F. Blute, J.R.B. Cockett, and R.A.G. Seely Abstract In this paper we introduce the notion of contextual categories. These provide a categorical semantics for the modelling of computation in context, based on the idea of separating logical sequents into two zones, one representing the context over which the computation is occurring, the other the computation itself. The separation into zones is achieved via a bifunctor equipped with a tensorial strength. We show that a category with such a functor can be viewed as having an action on itself. With this interpretation, we obtain a fibration in which the base category consists of contexts, and the reindexing functors are used to change the context. We further observe that this structure also provides a framework for developing categorical semantics for Girard's Unified Logic, a key feature of which is to separate logical sequents into two zones, one in which formulas behave classically and one in which they behave linearly. This separation is analogous to the context/computation separation above, and is handled by our semantics in a similar fashion. Furthermore, our approach allows an analysis of the exponential structure of linear logic using a tensorially strong action as the primitive notion. We demonstrate that from such a structure one can recover a model of the linear storage operator. Finally, we introduce a sequent calculus for the fragment of Unified Logic modeled by contextual categories. We show cut elimination for this fragment, and we introduce a simple notion of proof circuit, which provides a description of free contextual categories. ----------------------------- Available via browser on my home page ftp://triples.math.mcgill.ca/pub/rags/ragstriples.html or directly via ftp ftp://triples.math.mcgill.ca/pub/rags/bang/context1.[ps,dvi].gz (The [X,Y] syntax means you should use either X or Y in the URL, not both and not the "[", "]".) From cat-dist@mta.ca Tue Feb 28 08:44:41 1995 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA09564; Tue, 28 Feb 1995 08:44:41 -0400 Date: Tue, 28 Feb 1995 08:43:29 -0400 (AST) From: categories To: categories Subject: Enrichment and Representation Theorems for Domains. Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Mon, 26 Feb 1996 15:06:26 GMT From: Marcelo Fiore The prepint "Enrichment and Representation Theorems for Categories of Domains and Continuous Functions" is available from http://www.dcs.ed.ac.uk/home/mf files rep.dvi or rep.ps, or by anonymous ftp from ftp.dcs.ed.ac.uk directory pub/mf files rep.dvi or rep.ps. ----------------------------------------------------------------------- Enrichment and Representation Theorems for Categories of Domains and Continuous Functions Synopsis Domain-theoretic categories are axiomatised by means of categorical non-order-theoretic requirements on a cartesian closed category equipped with a commutative monad. We prove an enrichment theorem showing that every axiomatic domain-theoretic category can be endowed with an intensional notion of approximation, the path relation, with respect to which the category Cpo-enriches. Subsequently, we provide a representation theorem of the form: every small domain-theoretic category (with a lifting monad) has a full and faithful representation in a domain-theoretic category of cpos and continuous functions (with a lifting monad) in a suitable intuitionistic set theory. Our analysis suggests more liberal notions of domains. In particular, we present a category where the path order is not omega-complete, but in which the constructions of domain theory (as, for example, the existence of uniform fixed-point operators and the solution of domain equations) are possible. ----------------------------------------------------------------------- From cat-dist@mta.ca Thu Feb 29 23:33:21 1996 Received: from bigmac.mta.ca by mailserv.mta.ca; (5.65/1.1.8.2/09Sep94-0117PM) id AA31358; Thu, 29 Feb 1996 23:33:20 -0400 Date: Thu, 29 Feb 1996 23:31:48 -0400 (AST) From: categories To: categories Subject: The announcement of ALGI3 Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Status: O X-Status: Date: Fri, 01 Mar 1996 04:39:49 +0900 From: AKAMA Youji PLEASE POST ** PLEASE POST ** PLEASE POST ** PLEASE POST ** PLEASE POST Preliminary Call for Participation The Third Seminar on Algebra, Logic, and Geometry in Informatics (ALGI 3) April 3-5, 1996 Keio University, Mita, Tokyo The ALGI (Algebra, Logic, and Geometry in Informatics) seminar is a series of informal peripatetic seminars in Japan (hopefully extending to other areas of Eastern Asia / Oceania) on the interaction between informatics and mathematics. Information about ALGI seminars can be found at "http://www.etl.go.jp:8080/People/yoshiki/ALGI-e.html". For the third meeting, watch "http://nicosia.is.s.u-tokyo.ac.jp/~akama/algi3.html". The third ALGI meeting will be held as one of the post-conference workshops of Linear Logic 96 (held at Keio University, organized by Prof. Mitsu OKADA). The scope of ALGI includes Linear Logic, but is not restricted to it. We expect offers of talks about informal, half-baked works, as well as completed ones. Participants should fill in the registration form below and send it to "akama@is.s.u-tokyo.ac.jp". The details of the meeting will be announced later in the same place. * Date: 3 April afternoon - 5 April. * Place: Keio University, Mita. * Program: To be decided. * Schedule 3 April: From some time in the afternoon. 4 April: From morning, Rest during 1330-1430, for van Dalen symposium being held meantime. 5 April: From morning. * For program/registration/hotel information for Linear Logic 96, see "http://abelard.flet.mita.keio.ac.jp/person/linear96/Linear96.html". The listing of hotels can be found at "http://abelard.flet.mita.keio.ac.jp/person/linear96/hotel.html". * Registration: Please send the registration form to Yohji AKAMA (akama@is.s.u-tokyo.jp). * General inquiry: Yohji AKAMA, Department of Information Science, The University of Tokyo, Hongoh, 7-3-1, Bunkyo-ku,Tokyo, 113, Japan. 03(3812)4177(direct), 03(3812)2111(ext.4097), 03(3818)1073(fax) akama@is.s.u-tokyo.ac.jp ===================================================================== ALGI Registration form Please use the following format: I intend to come to the 3rd meeting of the ALGI seminar. * I intend to give a talk entitled ......... * I will need approximately......minutes Name ....................................... Address .................................... ............................................ Email ..................................... Tel ..................................... Fax ..................................... *Delete if inapplicable Please inform us if you need anything else besides blackboard and OHP Please inform us (in)convenient day of your talk.