June 1997 - Categories - categories.org.au

functions Omega->Omega
by Paul Taylor 15 Jul '97

15 Jul '97

Richard Wood mentioned an observation about functions Omega->Omega in a topos. In the more abstract situation of a classifier Sigma for some subclass of monos (closed under isomorphisms, composition and pullback along arbitrary maps, and such that the characteristic function of a subobject, where it exists, is unique), the following formula holds: for any function f:Sigma x X -> X and predicate a:X -> Sigma f(a) & a = f(true) & a In fact, along with Sigma being a semilattice, this is necessary and sufficient for Sigma and its powers to form a full subcategory of some category in which Sigma is a classifier. I wonder whether anyone has noticed this formula before? In my construction, the Frobenius law for an existential quantifier is derivable from it. It is also reminiscent of the Berry order in stable domain theory, but I can see no substantial connection. It is easily provable in higher order logic: either way, assume a, so a=true. Curiously, Phoa's Principle (in synthetic domain theory) is the conjunction of the higher order equation above its lattice dual f(a) \/ a = f(false) \/ a and all functions f:Sigma->Sigma are monotone. For the continuation of this story, go to Vancouver ... Paul

4 3

Query
by categories 02 Jul '97

02 Jul '97

---------- Forwarded message ---------- Date: Thu, 26 Jun 1997 13:57:18 +0300 (IDT) From: ZIPPIE Gonczarowski <zippie(a)actcom.co.il> To: cat-dist(a)mta.ca Dear Colleagues, I am applying tools of category theory to research in artificial perception and cognition. A basic category is proposed where every perception is an object and morphisms capture the flow between perceptions. Natural transformations capture paths to more cognitive perceptions. An Anonymous referee remarked that my category is `very closely related to comma categories'. Can anybody refer me to written material that introduces comma categories? Also, please let me know if you are aware of other research that applies categorical tools to research in artificial perception and cognition. Thanks Zippie e-mail zippie(a)actcom.co.il Dr. Zippora Arzi-Gonczarowski Typographics, Ltd. 46 Hehalutz St. Jerusalem 96222, Israel

4 3

algebraic logic via arrows
by Zinovy Diskin 30 Jun '97

30 Jun '97

I'd be grateful for comments on the following question motivated by a problem in categorizing algebraic logic a la Tarski. Let C be a complete category with a factorization system (E,M). Given an object A\in C, let us call a pair (m,e) with m\in M, cod(m)=A and e\in E, dom(e)=A, {\it compatible}, m~e, if the square * --m--> A | | e' e | | v v *--m'--> A/e is pull-back (where (e',m') factorizes m;e ). In SET with the standard surjection-injection factorization, m~e iff for all a,b\in A, a\in A_m and e(a)=e(b) entail b\in A_m where A_m is the subset of A corresponding to m. Now let (e_i, i\in I) be a family of congruences compatible with some m:*--->A, e_i ~ m for all i\in I. The question is what properties of (C,E,M) are required to provide sup(e_i, i\in I) ~ m ? (the collection CongA of e:A-->*, e\in E is a meet-complete semilattice due to products, sup is join-via-meets in this lattice). If C is a category of finitary algebras over SET with the standard epi-mono factorization, then sup(e_i) ~ m always holds due to the finitary deduction property of taking sup in the congruence lattice: (a,b)\in sup(e_i) iff there exists a finite subfamily e_1,...,e_k and c_0,...,c_k \in A s.t. a=c_0, b=c_k and e_j(c_{j-1}) =e_j(c_j) for all j=1,...,k . Zinovy Diskin

2 1

AMAST '97 - Call for TOOL AND SYSTEM DEMOS
by Richard Buckland 30 Jun '97

30 Jun '97

-------------------------------------------------------------------- Call for TOOL AND SYSTEM DEMONSTRATIONS Sixth International AMAST Conference AMAST '97, December 13-17, 1997, Sydney, Australia. -------------------------------------------------------------------- We invite demonstrations of software tools and systems. Goals: TOOL and SYSTEM DEMONSTRATIONS The major goal of the AMAST Conferences is to put software development technology on a firm, mathematical foundation. An important aspect of this long term goal is to circulate information about the experience of actual developments, and to encourage the development of and dissemination of information about software tools and development support systems. Accordingly we invite submissions of demonstrations in the following two categories: 1. Tools and Engines to Support formal software development 2. Examples of systems developed using algebraic methodologies -------------------------------------------------------------------- Demonstrations 1. TOOLS AND ENGINES TO SUPPORT FORMAL SOFTWARE DEVELOPMENT An essential component of mathematically founded software development is computational support. Following the successful trend established in the 1995 and 1996 meetings AMAST'97 will include sessions to demonstrate systems with relevance to algebraic or logical methodologies of software development. These sessions have proved popular with attendees in the past as they provide an opportunity for the wide range of researchers and practitioners attending the conference to discover and to learn more about tools and computational engines to support their work. The topics of interest include, but are not limited to, the following: - Software development environments - Support for correct software development - System support for reuse - Tools for prototyping - Validation and verification - Computer algebra systems - Theorem proving systems - Engines and computational support for the above - Systems supporting the education of students and/or practitioners in relevant topics 2. EXAMPLES OF SYSTEMS DEVELOPED USING ALGEBRAIC METHODOLOGIES Topics of interest include, but are not limited to, the following: - System demonstrations showing the improved effectiveness of software developed on a mathematical basis. - Case studies. - Unsuccessful system developments. - Reports on current commercial and industrial practice. -------------------------------------------------------------------- Submissions We invite submissions of tool and system demonstrations. Prospective demonstrators should submit electronically in one or both of the following formats: 1. A paper of high quality of between two and five pages in LNCS style. Submissions in this category should be of theoretical merit and report on previously unpublished work. 2. An abstract of one to two pages providing a description of the tool or system to be demonstrated and containing pointers to further information, preferably available electronically. It is anticipated that the abstracts will be published at the rear of the proceedings in the form of a reference for practitioners, and additionally as an on-line reference on the world wide web. Please see details at http://www.cs.mq.edu.au/amast97 under "submission" which explain how to get a paper number, and then submit a fully self-contained postscript file via ftp (preferably derived from LaTeX with the LNCS style on a standard UNIX system). If for any reason it is impossible to submit electronically authors may send six paper copies of their submission to the Tools and Demos address below. All papers will be refereed and will be judged based on their significance, technical merit, and relevance to the conference. As in the past, we expect the proceedings to be published by Springer-Verlag in their Lecture Notes in Computer Science Series. Papers and abstracts should be received by July 7, 1997. -------------------------------------------------------------------- General AMAST Goals The major goal of the AMAST Conferences is to put software development technology on a firm, mathematical foundation. Particular emphasis is given to algebraic and logical foundations of software technology. An eventual goal is to establish algebraic and logical methodologies as practically viable and attractive alternatives to the prevailing approaches to software engineering. Previous meetings of AMAST were held in Iowa (1989 and 1991), Twente, Holland (1993), Montreal (1995) and Munich (1996). During these meetings, AMAST has attracted an international spread of researchers and practitioners interested in software technology, programming methodology and their algebraic and logical foundations. In addition, the first day of each conference has been dedicated to Mathematics Education for Software Engineers. The sixth AMAST International Conference will be held at Macquarie University, Sydney, Australia, from December 13 to December 17, 1997. -------------------------------------------------------------------- Further Information Address for non-electronic submissions and inquiries: Richard Buckland AMAST'97 Tools and Demos School of Computer Science and Engineering University of New South Wales Sydney, 2052, Australia Phone: ++61 (0)2 9698 7975 Fax: ++61 (0)2 9385 5995 For further information on the conference: http://www.cs.mq.edu.au/amast97 amast97(a)mpce.mq.edu.au -------------------------------------------------------------------- AMAST General Chair: Maurice Nivat (France) Programme Chair: Michael Johnson (Australia) -------------------------------------------------------------------- Programme Committee V.S. Alagar (Canada), Egidio Astesiano (Italy), Didier Begay (France), Richard Buckland (Australia), John Cannon (Australia), Kokichi Futatsugi (Japan), Armando Haeberer (Brazil), Paola Inverardi (Italy), Michael Johnson (Australia), Rocco De Nicola (Italy), Anton Nijholt (Netherlands), Fernando Orejas (Spain), Mehmet Orgun (Australia), John Plaice (Canada) John Potter (Microsoft Research Institute), R. Ramanujam (India), Charles Rattray (Great Britain), Teodor Rus (USA), T. Sakabe (Japan), Giuseppe Scollo (Netherlands), R.K. Shyamasundar (India), Andrzej Tarlecki (Poland), R.F.C Walters (Australia), Martin Wirsing (Germany). -------------------------------------------------------------------- Tool and System Demos Committee Richard Buckland (University of New South Wales) Ken Robinson (University of New South Wales) Jon Tidswell (Microsoft Research Institute) -------------------------------------------------------------------- Important Dates for Tool and System Demonstrations Submission of Demo Proposals: July 12, 1997 Author notification of outcome: August 12, 1997 Camera ready copy received by: September 1, 1997 Education Day: December 13, 1997 Conference Days: December 14-17, 1997 [This announcement is available on the AMAST'97 WWW site, at URL: http://www.cs.mq.edu.au/amast97/demo-cfp.html ] ---------------------------------------------------------------- Richard Buckland School of Computer Science and Engineering The University of New South Wales

1 0

Timetable for Billfest
by Michael Barr 29 Jun '97

29 Jun '97

Below (in latex, followed by ascii) is what is hopefully the final schedule for the Billfest. Amazingly, every speaker got a title and abstract to the AMS by the 26th. I should also mention that Beno Eckmann will be in Montreal from Sept 21-28. He will talk in the category seminar on Sept. 23 and we are trying to arrange a colloquium for Sept. 25. Michael \documentstyle[12pt]{article} \textwidth 6.3in \oddsidemargin -.1in \pagestyle{empty} \begin{document} \begin{tabular}{|r(a){--}r|l|p{3.4in}|}\hline \multicolumn4{|c|}{Friday, September 26\vrule height 15pt depth 5pt width 0pt}\\ \hline \multicolumn2{|c|}{} && \\[-10pt]\hline 8:45 & 9:30 &Andr\'e Joyal & The theory of $h$-categories \\ \hline 9:40 & 10:10 &Marta Bunge &Functions vs Distributions on Grothendieck toposes\\ \hline 10:20 & 10:50 &Jonathon Funk &Complete Spreads in Topos Theory\\ \hline \multicolumn2{|c|}{} && \\[-12pt]\hline 2:30 & 3:15 &Pierre Cartier & Computation and visualization: a new philosophy of categories \\ \hline 3:25 & 3:55 &Phil Mulry & Remarks on Categorical Fixed Points \\ \hline 4:05 & 4:35 &Jim Otto & From NNO to Complexity \\ \hline 4:45 & 5:15 &Robert Par\'e & On the Cardinality of Functors \\ \hline \multicolumn4{|c|}{Saturday, September 27\vrule height 15pt depth 5pt width 0pt}\\ \hline \multicolumn2{|c|}{} && \\[-10pt]\hline 8:45 & 9:30 &Bill Lawvere & Toposes of Laws of Motion\\ \hline 9:40 & 10:10 &Walter Noll &Conceptual Mathematics, Categories, Functors, and Tensors \\ \hline 10:20 & 10:50 &Anders Kock & Geometric Construction of the Levi-Civita Parallelism \\ \hline \multicolumn2{|c|}{} && \\[-12pt]\hline 2:30 & 3:15 &Peter Gabriel & Categories and Representation Theory\\ \hline 3:25 & 3:55 &Alex Heller & Semistabilization and infinite loop-spaces \\ \hline 4:05 & 4:35 &Kimmo Rosenthal& Multirelations and power quantales \\ \hline 4:45 & 5:15 &Fred Linton& Triples vs. Theories---one last time\\ \hline \multicolumn4{|c|}{Sunday, September 28\vrule height 15pt depth 5pt width 0pt}\\ \hline \multicolumn2{|c|}{} && \\[-10pt]\hline 8:45 & 9:30 &Mikhail Kapranov & Dg-thickenings of classifying spaces \\ \hline 9:40 & 10:10 &Ross Street & The Petit Topos of Globular Sets\\ \hline 10:20 & 10:50 &Todd Trimble & Opetopes and bar constructions \\ \hline \multicolumn2{|c|}{} && \\[-12pt]\hline 2:30 & 3:15 &Steve Schanuel & Objective number theory \\ \hline 3:25 & 3:55 &Aurelio Carboni & Syntactic characterizations of various classes of locally presentable categories \\ \hline 4:05 & 4:35 &Jim Lambek &What is the category of sets---A tribute to Bill Lawvere \\ \hline 4:45 & 5:15 &Claudio Hermida&Higher-dimensional multicategories \\ \hline \end{tabular} \end{document} |=======================================================================| | Friday, September 26 | |=======================================================================| |=======================================================================| | 8:45- 9:30| Andr\'e Joyal | The theory of h-categories | |------------|---------------------|------------------------------------| | 9:40-10:10| Marta Bunge | Functions vs Distributions | | | | on Grothendieck toposes | |------------|---------------------|------------------------------------| | 10:20-10:50| Jonathon Funk | Complete Spreads in Topos Theory | |============|=====================|====================================| | 2:30- 3:15| Pierre Cartier | Computation and visualization: | | | | a new philosophy of categories | |------------|---------------------|------------------------------------| | 3:25- 3:55| Phil Mulry | Remarks on Categorical Fixed Points| |------------|---------------------|------------------------------------| | 4:05- 4:35| Jim Otto | From NNO to Complexity | |------------|---------------------|------------------------------------| | 4:45- 5:15| Robert Par\'e | On the Cardinality of Functors | |=======================================================================| | | | | |=======================================================================| | Saturday, September 27 | |=======================================================================| |=======================================================================| | 8:45- 9:30| Bill Lawvere | Toposes of Laws of Motion | |------------|---------------------|------------------------------------| | 9:40-10:10| Walter Noll | Conceptual Mathematics, Categories,| | | | Functors, and Tensors | |------------|---------------------|------------------------------------| | 10:20-10:50| Anders Kock | Geometric Construction of | | | | the Levi-Civita Parallelism | |============|=====================|====================================| | 2:30- 3:15| Peter Gabriel |Categories and Representation Theory| |------------|---------------------|------------------------------------| | 3:25- 3:55| Alex Heller | Semistabilization and | | | | infinite loop-spaces | |------------|---------------------|------------------------------------| | 4:05- 4:35| Kimmo Rosenthal | Multirelations and power quantales | |------------|---------------------|------------------------------------| | 4:45- 5:15| Fred Linton |Triples vs. Theories--one last time | |=======================================================================| | | | | |=======================================================================| | Sunday, September 28 | |=======================================================================| |=======================================================================| | 8:45- 9:30| Mikhail Kapranov |Dg-thickenings of classifying spaces| |------------|---------------------|------------------------------------| | 9:40-10:10| Ross Street | The Petit Topos of Globular Sets | |------------|---------------------|------------------------------------| | 10:20-10:50| Todd Trimble | Opetopes and bar constructions | |============|=====================|====================================| | 2:30- 3:15| Steve Schanuel | Objective number theory | |------------|---------------------|------------------------------------| | 3:25- 3:55| Aurelio Carboni | Syntactic characterizations of | | | | various classes of locally | | | | presentable categories | |------------|---------------------|------------------------------------| | 4:05- 4:35| Jim Lambek | What is the category of sets-- | | | | A tribute to Bill Lawvere | |------------|---------------------|------------------------------------| | 4:45- 5:15| Claudio Hermida | Higher-dimensional multicategories | |=======================================================================|

1 0

PSSL65 - Preliminary Announcement
by Carsten Butz 28 Jun '97

28 Jun '97

--------------------------------------------------------------------------- Preliminary announcement: 65th Peripatetic Seminar on Sheaves and Logic (PSSL) Dear colleagues, The next Peripatetic Seminar on Sheaves and Logic will be held in Aarhus (Denmark) over the weekend of 1-2 November 1997. We welcome talks on category theory, sheaves, logic, and related areas. The first announcement, including information about accommodation and how to get to Aarhus, will be sent out later during the summer on this category mailing list. We will maintain as well a WWW-page including (hopefully) relevant information for the seminar, although this is only in addition to the standard procedures. The URL is http://www.brics.dk/~butz/PSSL65/pssl65.html Also, we would like to mention that Birmingham has plans to organise the next PSSL (spring 1998) (contacts Neil Ghani, Neil.Ghani(a)cs.bham.ac.uk or Valeria DePaiva, V.DePaiva(a)cs.bham.ac.uk) Another one will probably take place in Utrecht in May 1998 (contact Ieke Moerdijk, moerdijk(a)math.ruu.nl) Best regards, Carsten Butz and Anders Kock ------------------------------------------ Carsten Butz BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 8000 Erhus C Denmark butz(a)brics.dk http://www.brics.dk/~butz ------------------------------------------

1 0

2nd CFP - Computing: The Australiasian Theory Symposium (CATS98)
by lxue＠cs.uwa.edu.au 27 Jun '97

27 Jun '97

CALL FOR PAPERS CATS'98 - Computing: The Australasian Theory Symposium University of Western Australia Perth, Western Australia 2-3 February, 1998 CATS'98 will be held at the University of Western Australia as part of the Australasian Computer Science Week (ACSW98) which also includes: . the Australasian Computer Science Conference (ACSC'98) . the Australasian Database Conference (ADC'98) . the Australasian Computer Architecture Conference (ACAC'98) Following on from CATS'94 in Sydney, CATS'96 in Melbourne, and CATS'97 in Sydney, CATS'98 aims at providing a forum for researchers in theoretical computer science. Typical, but not exclusive, topics of interest include: - Algorithms and data structure - Category theory - Complexity - Computational algebra, biology, geometry, logic, and number theory - Concurrency - Distributed and parallel computing - Formal semantics, specification, synthesis, and verification Original research papers are solicited. Submissions to CATS'98 this year will be again conducted electronically, and should be sent in standard Postscript format to cats98(a)cs.uwa.edu.au by the submission deadline. Authors unable to access e-mail may send 4 hard copies of their papers to the program committee chair: Xuemin Lin -- CATS'98 Department of Computer Science University of Western Australia Crawley, Western Australia 6907 Australia E-mail: cats98(a)cs.uwa.edu.au http://www.cs.uwa.edu.au:80/~lxue/CATS98/index.html In both cases, confirmation of receipt will be given, in the case of a postscript submission, once the file has been successfully printed. Submissions should include an abstract, 3-6 key words, and the fax number and e-mail address of the corresponding author. The contribution of the paper should be clearly explained in both general and technical terms, and authors should make every effort to ensure the technical content of their papers is understandable by a broad audience. The paper (an extended abstract or full paper) should not exceed 15 A4 pages using 11 point or larger font. Submission of a paper should be regarded as an undertaking that, should the paper be accepted, at least one of the authors will attend the conference to present the work. Papers will be judged on originality, significance, correctness, and clarity. Accepted papers will be published in the proceedings of the Symposium, which will appear in the DMTCS series of Springer-Verlag. ========================================= INVITED SPEAKERS: Ming Li (University of Waterloo, Canada) Takeshi Tokuyama (IBM, Japan) ========================================= IMPORTANT DATES: Submission Deadline: Friday 15 August 1997. This is a hard deadline; submissions postmarked after this date will be returned. Author Notification: Friday 24 October 1997. Final Version: Friday 14 November 1997. Acceptance of papers for the conference will be conditional upon the registration of at least one of the authors by 21 November 1997. ========================================= GENERAL CHAIR: James Harland RMIT PROGRAM COMMITTEE CHAIR: Xuemin Lin UWA LOCAL CHAIR: Chi-Ping Tsang UWA STEERING COMMITTEE: John Crossley Monash University Peter Eades University of Newcastle James Harland RMIT Michael Johnson Macquarie University John Staples University of Queensland Harald Sondergaard University of Melbourne PROGRAM COMITTEE: Cristian Calude University of Auckland Hossam Elgindy University of Newcastle Matthew Hennessy University of Sussex Xuemin Lin University of Western Australia Bruce Maggs Carnegie-Mellon University Martin Odersky University of South Australia Hong Shen Griffith University Harald Sondergaard University of Melbourne Antonios Symvonis University of Sydney Tadao Takaoka University of Canterbury Ron van der Meyden University of Technology, Sydney Lusheng Wang City University of Hong Kong Sue Whitesides McGill University David Wolfram Australian National University ===================================== ADDRESS FOR ALL PAPER SUBMISSION CORRESPONDENCE Xuemin Lin -- CATS'98 Department of Computer Science University of Western Australia Crawley, Western Australia 6907 Australia Telephone: +61 9 380 3449 Facsimile: +61 9 380 1089 E-mail: cats98(a)cs.uwa.edu.au ===================================== ADDRESS FOR CORRESPONDENCE, OTHER THAN PAPER SUBMISSION, RELATED TO ANY CONFERENCE FORMING PART OF THE AUSTRALIAN COMPUTER SCIENCE WEEK ACSW'98 Information Department of Computer Science The University of Western Australia Crawley, Western Australia, 6907 Telephone: +61 9 380 2533 Email: acsw98info(a)cs.uwa.edu.au ORGANISING COMMITTEE CHAIR Chris McDonald Department of Computer Science The University of Western Australia Crawley, Western Australia, 6907 Email: chris(a)cs.uwa.edu.au ACSW'98 Hosts: Department of Computer Science, The University of Western Australia Department of Computer Science, Curtin University of Technology Department of Computer Science, Edith Cowan University Computer Science Programme, Murdoch University

1 0

REMINDER: MATHFIT Summer School and Workshop
by M.Z.Kwiatkowska＠cs.bham.ac.uk 26 Jun '97

26 Jun '97

Dear Colleagues, We enclose a reminder of two events to be held in Birmingham this September. Please note that the deadline for early registration and applications for grants is ***30th June***. Please forward to anyone interested. Best wishes, Achim and Marta. ------------------------------------------------------------------------- SUMMER SCHOOL and WORKSHOP on NEW PARADIGMS FOR COMPUTATION ON CLASSICAL SPACES Birmingham, 8-10 September 1997 and 11-13 September 1997 The two events are centered around recent developments in the theory of continuous domains as applied to classical problems in Mathematics and Semantics. These developments are based on ground-breaking work by Abbas Edalat who, using earlier work by Jimmie Lawson, Claire Jones and Gordon Plotkin, showed in the early 90's how a classical (locally compact) space could be embedded as the set of maximal points in a domain. This led to a new theory of integration with applications in the theory of Iterated Function Systems, Neural Networks, Statistical Physics, and Fractal Geometry. More recently, Abbas Edalat and Martin Escardo have made substantial progress on the question of exact real number computation. The Summer School is intended to teach the mathematical background of the theory enabling participants to fully take part in the following Workshop. A small number of grants for the Summer School are available for PhD students. Further information can be found at http://www.cs.bham.ac.uk/~axj/comprox.html

1 0

pushouts in toposes
by Cesc Rossello 23 Jun '97

23 Jun '97

Dear categorists A PhD student of mine, Merce Llabres, and I we have got involved in proving some properties of pushouts on toposes, similar (but somehow dual) to those known for pullbacks. We are worried by the fact that perhaps somebody else has already proved many of the results we are interested in. So, before struggling to prove some probably well-known things, we would really appreciate some pointers to literature on the topic. For instance: Assume you have a family of pushouts in a topos Ai ---> Bi | | v f v A------> B (all squares have the same bottom arrow f) with vertical arrows monic, and assume the pullbacks of (Ai -->A)_i and (Bi---> B)_i exist, say A0 and B0, and consider the obvious square A0 ---> B0 | | v f v A------> B It is a pushout square when the family of squares is finite, and for arbitrary families in all complete toposes we have tried (sets, hypergraphs, total unary algebras, unary partial algebras with closed homomorphisms,...). Moreover, a proof (for complete toposes) can probably be derived from the techniques in the paper by Kawahara in TCS vol 77 (1990). But, has somebody already proved (or disproved) such a result? Thanks in advance Cesc Rossello

3 3

CSL'97: Programme and Call for Participation
by Uffe Henrik Engberg 21 Jun '97

21 Jun '97

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Programme and Call for Participation CSL'97 The 1997 Annual Conference on Computer Science Logic Aarhus, Denmark, 25-29 August, 1997 Organized by BRICS, Department of Computer Science, University of Aarhus Sponsored by BRICS, the Danish National Research Foundation and the Danish National Research Council -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- The 1997 Annual Conference on Computer Science Logic, CSL'97, will be held at the Computer Science Department, University of Aarhus, Denmark, 25 - 29 August, 1997, preceded by Tutorials, 23 - 24 August, 1997. The conference includes invited talks by the following speakers: - Samuel R. Buss, San Diego - Hubert Comon, Paris - Thierry Coquand, Gothenburg - Martin Hyland, Cambridge - Neil Immerman, Amherst - Nils Klarlund, Murray Hill - Yiannis N. Moschovakis, Los Angeles - Leszek Pacholski, Wroclaw The tutorials include a three series of lectures on the theme of Games in Computer Science Logic. The tutorials speakers are: - Samson Abramsky, Edinburgh - E. Allen Emerson, Austin - Wolfgang Thomas, Kiel - Igor Walukiewicz, Warsaw Preliminary proceedings will be available at the conference, and final proceedings will be published in Springer Lecture Notes in Computer Science, Springer Verlag. Participants will receive copies of both. Besides the scientific program, the conference offers a nice social programme including a conference dinner and an excursion visiting the Museum of Prehistory at Moesgaard and the Old Town of Aarhus. Amongst the attractions of Moesgaard are its collections from the Viking Age, and the Grauballe man, one of the only complete preserved bog bodies from the Iron age. A limited number of student grants covering accommodation, conference fee including refreshments, lunches, excursion, conference dinner and conference material, are available. Information on registering, student grants, travel etc., can be found after the conference and tutorials programme below or by visiting: http://www.brics.dk/CSL97 =========================================================================== CSL'97 Conference Programme =========================================================================== MONDAY, AUGUST 25 08:00-09:15 Registration 09:15-09:30 Welcome 09:30-10:30 Neil Immerman (invited speaker): Descriptive Complexity and Model Checking 10:30-11:00 Break 11:00-11:30 L. Staiger: Disjunctive omega-Words and Monadic Second-Order Arithmetic 11:30-12:00 D. Pardo, A. Rabinovich, B.A. Trakhtenbrot: On Synchronous Circuits over Continuous Time 12:00-12:30 A. Arnold, D. Janin: A Note on the Satisfiability Problem in Fixpoint Calculi 12:30-14:00 Lunch 14:00-15:00 Samuel R. Buss (invited speaker): Resolution, The Pigeonhole Principle and Proof Complexity 15:00-15:30 M. L. Bonet, N. Galesi: Linear Lower Bounds and Simulations in Frege Systems with Substitutions 15:30-16:00 Break 16:00-16:30 T. Coquand, H. Persson: A Proof-Theoretical Investigation of Zantema's Problem 16:30-17:00 E. Pezzoli: On the Computational Complexity of Type 2 Functionals 17:00-17:30 P. J. Voda: A Simple Ordinal Recursive Normalization of Goedel's T 17:45- EACSL Business Meeting TUESDAY, AUGUST 26 09:00-10:00 Thierry Coquand (invited speaker): Formal Topology and Inductive Definitions 10:00-10:30 M. Hollenberg: Equational Axioms of Test Algebra 10:30-11:00 Break 11:00-11:30 T. Brauener, V. de Paiva: A Dependency Formulation for Linear Logic 11:30-12:00 C. Faggian: Classical Proofs via Basic Logic 12:00-12:30 P. Baillot, V. Danos, T. Ehrhard, L. Regnier: Timeless Games 12:30-14:00 Lunch 14:00-15:00 Nils Klarlund (invited speaker): Mona & Fido: The Logic/Automaton Connection in Practice 15:00-15:30 O. Kupferman, R.P. Kurshan, M. Yannakakis: Existence of Reduction Hierarchies 15:30-16:00 Break 16:00-16:30 M. Grohe: Inversion of the L^k-invariants is Hard 16:30-17:00 A. Durand, R. Fagin, B. Loescher: Spectra with only Unary Function Symbols 17:00-17:30 F. Olive: A Conjunctive Logical Characterization of Nondeterministic Linear Time 17:30-18:00 T. Schwentick: Padding and the Expressive Power of Existential Second-Order Logics WEDNESDAY, AUGUST 27 09:00-10:00 Yiannis N. Moschovakis (invited speaker): Concurrent Recursion 10:00-10:30 R. Backofen, P. Clote: Evolution as a Computational Engine 10:30-11:00 Break 11:00-11:30 I. Schiering: A Hierarchical Approach to Graph Automata and Monadic Second-Order Logic over Graphs 11:30-12:00 N. Schweikardt: The Monadic Quantifier Alternation Hierarchy over Grids and Pictures 12:00-12:30 A. Ayari, D. Basin, A. Podelski: Lisa: A Specification Language Based on WS2S 13:30- Excursion THURSDAY, AUGUST 28 09:00-10:00 Hubert Comon (invited speaker): Higher-Order Matching and Tree Automata 10:00-10:30 F. Kamarredine, R. Bloo, R. Nederpelt: An Approximation of Reductional Equivalence 10:30-11:00 Break 11:00-11:30 A. Barber, P. Gardner, M. Hasegawa, G. Plotkin: From Action Calculi to Linear Logic 11:30-12:00 P. Ruet, F. Fages: Concurrent Constraint Programming and Mixed Non-Commutative Linear Logic 12:00-12:30 M. Hofmann: A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion 12:30-14:00 Lunch 14:00-15:00 Martin Hyland (invited speaker): Constructing Categories of Abstract Games 15:00-15:30 J. Power: Categories with Algebraic Structure 15:30-16:00 Break 16:00-16:30 S. Abramsky, G. McCusker: Call-by-Value Games 16:30-17:00 R. Heckmann, M. Huth: A Duality Theory for Quantitative Semantics 17:00-17:30 T. Hartonas, M. Hennessy: Full Abstractness for a Functional/Concurrent Language with Higher-Order Value-Passing 19:00- Conference Dinner FRIDAY, AUGUST 29 09:00-10:00 Leszek Pacholski (invited speaker): Complexity of Type Inference 10:00-10:30 G. Davydov, I. Davydova: Applications of Unsatisfiability 10:30-11:00 Break 11:00-11:30 P. A. Bonatti, N. Olivetti: A Sequent Calculus for Circumscription 11:30-12:00 J. Hudelmaier: Bicomplete Calculi for Intuitionistic Propositional Logic 12:00-12:30 S. Brass, J. Dix, I. Niemelae, T. C. Przymusinski: A Comparison of the Static and the Disjunctive Well-founded Semantics 12:30-14:00 Lunch End of Conference =========================================================================== CSL'97 Tutorials Programme =========================================================================== SATURDAY, AUGUST 23 09:00-09:15 Welcome 09:15-10:45 Samson Abramsky, Univ. of Edinburgh: Game Semantics 10:45-11:15 Break 11:15-12:15 Wolfgang Thomas, Univ. of Kiel: Determinacy, the Rabin Tree Theorem and its extensions 12:15-14:00 Lunch 14:00-15:00 Wolfgang Thomas: Determinacy, the Rabin Tree Theorem and its extensions 15:00-15:30 Break 15:30-17:00 Samson Abramsky: Game Semantics SUNDAY, AUGUST 24 09:15-10:45 E. Allen Emerson, Univ. of Texas at Austin: Games, mu-calculus, and program verification 10:45-11:15 Break 11:15-12:15 Igor Walukiewicz, Univ. of Warsaw: Determinacy, the Rabin Tree Theorem and its extensions 12:15-14:00 Lunch 14:00-15:00 Igor Walukiewicz: Determinacy, the Rabin Tree Theorem and its extensions 15:00-15:30 Break 15:30-17:00 E. Allen Emerson: Games, mu-calculus, and program verification Tutorial Abstracts Samson Abramsky: Game Semantics for Programming Languages Abstract These lectures will give an introduction to game semantics and its applications to modelling programming languages. The mathematical structure of categories of games will be described, and it will be shown how they can be used to model a range of computational features in a precise way. E. Allen Emerson: Games, mu-calculus, and Program Verification Abstract Temporal logics are often used to verify concurrent programs using such techniques as model checking. We describe some intimate connections between such temporal logics, the related fixpoint logic known as the mu-calculus, and infinite games. Applications include improved nonemptiness algorithms for tree automata, mu-calculus characterizations of winning strategies in memoryless games, and an automata-theoretic characterization of the complexity of model checking in the mu-calculus. Wolfgang Thomas, Igor Walukiewicz: Determinacy, the Rabin Tree Theorem and its Extensions Abstract We present a self-contained proof of Rabin's Tree Theorem (decidability of the monadic theory of two successors). The proof uses memoryless determinacy of infinite games. We also show some extensions of the theorem to tree-like infinite graphs and discuss connections with fixed point calculi. =========================================================================== Further Information =========================================================================== How to Register ================ To get more detailed information on CSL'97, including information on registering, please visit: http://www.brics.dk/CSL97 We encourage you to register via this www page, but alternatively you may send an email to csl97(a)brics.dk including your surface mail address requesting a copy of the registration form to be forwarded. Notice that the deadline for early registration (DKK 2000) has been extended to July 11. Please also note that there is a reduced student registration fee (DKK 600). Registration Fees Particip. paid before July 11: DKK 2000 Particip. paid after July 11: DKK 2500 Student registration: DKK 600 Tutorials, paid before July 11: DKK 300 Tutorials, paid after July 11: DKK 400 The registration fees cover refreshments, lunches, excursion, banquet and conference material. See registration form for payment. If payment is made by credit card, the registration form must be signed and mailed or faxed to the Convention Bureau. All correspondence concerning registration and accommodation (payment, reservation, cancellation, etc.) should be sent to CSL'97 Aarhus Convention Bureau Raadhuset DK-8000 Aarhus C Denmark Telephone: +45 8612 1177 Telefax: +45 8612 0807 e-mail: aarhconv(a)inet.uni-c.dk Please give phone and/or telefax numbers on all inquiries to the Convention Bureau. Accompanying Persons ================== Please register accompanying persons on the registration form. Tickets for lunches, excursion and conference dinner may be purchased at the registra- tion desk. Grants ================== A limited number of student grants to attend the Conference and/or the Tutorials are available. The grants will cover local expenses (accom- modation at the nearby Youth Hostel and conference fee, including lunches and coffees during the conference, excursion and conference dinner). They will not cover travel expenses. The deadline for application is July 1, 1997. To apply, you fill out an application form available from the above mentioned www page, and return it with a short description of your research activity and a letter of recommendation from your supervisor or from the head of the department to Prof. Mogens Nielsen, CSL'97 Department of Computer Science University of Aarhus Ny Munkegade, Building 540 DK-8000 Aarhus C Denmark Inquiries ================== Organisational inquiries about the conference can be sent to: CSL97(a)brics.dk Local Organization ================== BRICS, Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C Denmark Telephone: +45 8942 3360 Telefax: +45 8942 3255 e-mail: csl97(a)brics.dk http://www.brics.dk/CSL97 Organizing Committee ================== Mogens Nielsen (chair) Gian Luca Cattani Uffe Engberg Karen K. Moeller Program Committee ================== K. Compton (Ann Arbor) J. Flum (Freiburg) F. Honsell (Udine) J. W. Klop (Amsterdam) V. W. Marek (Lexington) M. Nielsen (Aarhus, Vice-chair) P. Pudlak (Prague) E. Robinson (QMW, London) A. Tarlecki (Warsaw), W. Thomas (Kiel, Chair), I. Walukiewicz (Warsaw). Travel information ================== By air Aarhus Airport/Tirstrup is connected with Copenhagen International Airport through 19 daily departures on weekdays, 7-8 departures on Saturdays and Sundays. Flying time is 35 minutes. Aarhus Airport, located 40 km north of the city, offers direct international flights to Oslo, Stockholm, Gothenburg, London Heathrow and Amsterdam. Billund Airport, located 100 km south of Aarhus, has direct international flight connections to Amsterdam, Brussels, Paris, Nice, Frankfurt, London, Birmingham, Manchester, Riga, Oslo, Bergen, Stavanger, Stockholm and Berlin. By train/car From Southern and Central Europe, the train/car connections are via Hamburg/-Flensburg. Travel time from Hamburg to Aarhus is approximately five hours. >>From Eastern European countries train connections to Aarhus go via Poland and Copenhagen. Aarhus has an hourly service to and from Copenhagen and several daily connections to Sweden, Germany and the rest of Europe. Travel time Copenhagen-Aarhus is 3 hrs. 15 min. Accommodation ============= Aarhus Convention Bureau has made preliminary hotel reservations for the CSL'97 participants. Please use the registration form to book rooms. The hotels have been divided into three categories according to standard or comfort. The organizers cannot guarantee accommodation to participants who do not book in advance. Payment has to be made directly to the hotel upon departure. Social Program ============== Get-together: Get-together parties will be held on Friday, August 22 and Sunday, August 24, 7:00-10:00 pm at the conference venue. Beer and soft drinks will be served. Excursion: Wednesday, August 27, 1997 Programme 13:30 Departure from the conference site to the Museum of Prehistory at Moesgaard, a culture-historical museum which specializes in prehistoric archaeology and ethnography. The collections are from the Danish prehistory ranging from the Paleolithic Age to the end of the Viking Age. One of the major attractions is the Grauballe man - the only completely preserved bog body from the Iron Age (1st century BC). An ethnographical special exhibition about mountain people of the Hindu Kush is also on show at Moesgaard. On the museum grounds a replica of a stave church from the Viking Age is being erected this summer. The building is 9.5 m long and almost 5 m wide and is a reconstruction of a church found during excavation in Hoerning Church near Randers. The church is built to the north of the Hedeby house just behind the museum. Not since the Viking Age has a stave church been built in Denmark. The public is invited to follow the reconstruction. Weather permitting, we will take a prehistoric walk through fields and woods passing reconstructions of Iron Age houses, places of cult, and dolmens from the Stone Age. Refreshments will be served on the beach. 16:00 Buses will return to the centre of Aarhus, more precisely to The Old Town, an open-air museum with more than 75 half-timbered houses, rebuilt along cobbled streets and fitted out with all the workshops and furnishings of a Danish market town, reflecting life from 1600 down to our grand- parents' time. A meal in the Old Town restaurant, Simonsen's Garden, will finish the excursion. Conference Dinner: The conference dinner will be held on the evening of Thursday, August 28, starting at 7 pm in the canteen at the conference venue.

1 0