March 2001 - Categories - categories.org.au

Looking for adjoints
by Jean-Pierre Marquis 05 Apr '01

05 Apr '01

I would like to have a large pool of examples of adjoint functors in as many different fields of mathematics as possible. I am looking for the "nicest", in whatever sense you can think of this expression (e.g. unexpected, their existence is equivalent to a classical theorem, etc), cases in various fields. References or examples anyone? (Besides the standard ones found in Mac Lane, etc.) Thank you, Jean-Pierre Marquis

6 5

Co-operation with ASRIOS-Georgia
by Irakli Tskhvedadze 01 Apr '01

01 Apr '01

Dear Sir/Madam , Georgian Association of System Reforms and Informatization of Organizational Structures (ASRIOS) intends to find partners, carrying out Mathematical Structures in Computer Science, on close cooperation based on conceptual project ÂResearch to the Development of Dynamic Database Structure based on Mathematical ModelsÂ with possible funding support. ASRIOS conducts development of methodology of construction of information complexes on the basis of their unification based on Categorial Analysis, Petri Nets, Mathematical Lattice etc. If you take an interest in the given proposal, your recommendations for further interaction will be desirable. To learn more about ASRIOS activity, please visit web-site http://www.asrios.ge Thank you in advance, Sincerely, Irakli Tskhvedadze Vice-President of the Association of System Reforms and Informatization of Organizational Structures **************************************************** Association of System Reforms and Informatization of Organizational Structures(ASRIOS) Address: Georgia, 380071 Tbilisi, Gamsachurdia ave.10, apt.1 Web: http://www.asrios.ge E-mail: asrios(a)ip.osgf.ge asrios(a)parliament.ge Tel: +995 32 389710 +995 32 397926 *********************************************************

1 0

TACS 2001 -- extended deadline
by Benjamin C. Pierce 31 Mar '01

31 Mar '01

In response to a large number of requests, the submission deadline for TACS has been extended to April 15th. Authors intending to submit during this grace period are requested to email the title and abstract of their paper before the original deadline (April 1st) to bcpierce(a)cis.upenn.edu. Call For Papers Fourth International Symposium on Theoretical Aspects of Computer Science (TACS 2001) October 29-31, 2001 Tohoku University, Sendai, Japan http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ The TACS Symposium will focus on the theoretical foundations of programming and their applications. The topics of interest include... Theoretical aspects of the design, semantics, analysis, and implementation of programming languages and systems; logics of programs; calculi and models of concurrency and parallel computation; theories of mobile computation and system security; categories and types in computer science; formalisms, methods, and systems for program specification, verification, synthesis, and optimization; constructive, linear, and modal logics in computer science. The scientific program will consist of invited lectures, contributed talks, and demo sessions. A proceedings containing the full papers of the invited and contributed talks will be published by Springer-Verlag as a volume of Lecture Notes in Computer Science. IMPORTANT DATES Submission deadline: April 15, 2001 Notification to authors: June 20, 2001 Deadline for final versions: July 23, 2001 INVITED SPEAKERS Luca Cardelli Microsoft Research Daniel Jackson Massachusetts Institute of Technology Christine Paulin-Mohring Universite Paris Sud & INRIA Andrew Pitts University of Cambridge Jon Riecke Lucent Technologies Kazunori Ueda Waseda University CONFERENCE CHAIR: Takayasu Ito Tohoku University PROGRAM CO-CHAIRS: Naoki Kobayashi Tokyo Institute of Technology kobayasi(a)cs.titech.ac.jp Benjamin Pierce University of Pennsylvania bcpierce(a)cis.upenn.edu PROGRAM COMMITTEE: Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann Edinburgh University Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark Edinburgh University Makoto Tatsuta Kyoto University SUBMISSION INFORMATION Authors are invited to submit full papers (up to 6000 words, including figures and bibliographies). Papers must be unpublished and not submitted for publication elsewhere. Submissions should be in Postscript or PDF format, on A4 or US letter pages. They must be printable on common printers and viewable with ghostview or acroread. The first page of each submission should include the email address, telephone, and fax numbers of the corresponding author. Accepted papers must be presented at the symposium, and the final manuscript must be prepared in the LNCS format. All submissions should be made electronically through the TACS submission page http://saul.cis.upenn.edu:8086/.

1 0

jobs: Open positions at IT-C
by rms 27 Mar '01

27 Mar '01

Regarding open positions at The IT-University of Copenhagen, Via the following URL you will find a detailed description of 13 positions as Associate or Assistant Professor currently open at The IT-University of Copenhagen. http://www.it-c.dk/pub_uk/db_363.html Kind Regards Personnel Department/ The IT-University of Copenhagen

1 0

PhD studentships at the LFCS, U. of Edinburgh
by Paul Jackson 27 Mar '01

27 Mar '01

[This announcement has been sent to the categories mail list since much research at the LFCS makes use of category theory. Please pass it on to interested students and colleagues at your university or research institute. Apologies if you receive multiple copies] PhD positions available for October 2001 Laboratory for Foundations of Computer Science Division of Informatics, University of Edinburgh Applications are open for students to take up PhD places at Edinburgh in October 2001. Supporting funds are available for postgraduates of any nationality. The Laboratory for Foundations of Computer Science is one of the world's leading centres of research into theoretical computer science and its application. An important part of this is its active community of research students, currently over 20 strong. LFCS runs a 3-year PhD programme; this includes a series of taught courses which provide a broad background in the theory of computation, and prepare students to do their own research work. All students are directly supervised by an academic staff member. The Laboratory and the Division fund some studentships of their own, open to applicants of any nationality. UK students can also apply for one of several grants awarded to the Division by the EPSRC. For more information, including details of how to apply, please consult our web site. http://www.lfcs.informatics.ed.ac.uk/research/students.html

1 0

A. Carboni - eaddress
by aurelio.carboni＠uninsubria.it 24 Mar '01

24 Mar '01

>>From now on my e-mail address that should be used is aurelio.carboni(a)uninsubria.it at my official institution, which is Universita' dell'Insubria Dipartimento di Scienze CC, FF e MM Via Valleggio 11 22100 COMO (IT). Thanks, Aurelio.

1 0

preprint: The logic of linear functors
by Robert A.G. Seely 21 Mar '01

21 Mar '01

We wish to announce the availability of the following paper, at the URL given below. The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely It has been commonplace to base logics and type theories on categorical doctrines; with this paper we propose a more general paradigm, suggesting that logics and type theories may be based on functorial doctrines. This paradigm is very general - in particular, it subsumes all of usual categorical logic and type theory as degenerate cases. So as to be able to make precise claims, we illustrate this idea with a special case, developing the logic of linear functors with sufficient detail to see that this one doctrine is general enough to deal with basic linear modal logic and with the Abrusci-Ruet mixed non-commutative linear logic. We emphasise the case where the logic is based on a single functor, but it will be clear that one could also base it on a family of functors, which would allow one to deal with process logic as considered by Hennessy and Milner. The paper's abstract is given in full below. The paper may be found at http://www.math.mcgill.ca/rags/linear/lfl.ps.gz> or go to R.A.G. Seely's home page http://www.math.mcgill.ca/rags/ and click on the appropriate link. ......................................................... The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely ABSTRACT: This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics which contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the "noncommutative logic" of Abrusci and Ruet, a variant of linear logic which has both commutative and noncommutative connectives. Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasize the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality. There have been several individual attempts to develop logics with distinct but related subsystems of connectives, such as the Abrusci--Ruet noncommutative logic and the bunch logic of O'Hearn and Pym; generally these are presented in terms of "bunching" the formulas in the sequents of the logics via different "punctuation". The present functor logic, by contrast, uses a system of "formula blocks", which represent the functorial action and which give finer control over what logical features may be displayed. By displaying a family of functor logics, we illustrate how different logical systems can be developed along these lines, logics which are primarily distinguished by the degree to which they permit nesting of formula blocks. Our examples will include a basic logic where there is essentially no nesting, a system of linear modal logic, which allows nesting, but has only one system of connectives, and the Abrusci--Ruet logic, where nesting is virtually unrestricted and there are two subsystems of connectives. We finish by showing how to translate between the ``bunch'' style of logic and our ``formula block'' or functor logic using the Abrusci--Ruet noncommutative logic as an example. ================== R.A.G. Seely <rags(a)math.mcgill.ca> <http://www.math.mcgill.ca/rags>

1 0

IJCAR 2001 - Deadlines reminder + List of accepted papers
by Peter Baumgartner 20 Mar '01

20 Mar '01

------------------------------------------------------------ IJCAR 2001 The International Joint Conference on Automated Reasoning http://www.dii.unisi.it/~ijcar/ ------------------------------------------------------------ Contents: 1) About IJCAR 2) Deadlines reminder 3) List of accepted Research Papers 4) List of accepted System Descriptions 1) About IJCAR -------------- The International Joint Conference on Automated Reasoning (IJCAR) is the fusion of three major conferences in Automated Reasoning: CADE (The International Conference on Automated Deduction), TABLEAUX (The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods) and FTP (The International Workshop on First-Order Theorem Proving). These three events will join for the first time at the IJCAR conference in Siena in June 2001. 2) Deadlines reminder --------------------- The submission deadline for research papers and system descriptions has passed. However, submission of short papers and submission to workshops is still open. Short papers submission deadline : April 2, 2001 Workshop submission deadlines: Theory and Application of Quantified Boolean Formulas : March 24, 2001 Verification : March 25, 2001 Future directions in Automated Reasoning : March 29, 2001 Mechanized Reasoning about Languages with Variable Bindings : March 30, 2001 Precise Modelling and Deduction for OO-Software Development : March 31, 2001 Automation of Proof by Mathematical Induction : March 31, 2001 Strategies in Automated Deduction (STRATEGIES 2001) : March 31, 2001 Proof Transformations, Proof Presentations and Complexity of Proofs (PTP-01) : March 31, 2001 Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics : April 1, 2001 Unification (UNIF-2001) : April 15, 2001 For details please visit the IJCAR web page given above. 3) List of accepted Research Papers ----------------------------------- (88 submitted, 37 accepted) Ulrike Sattler, Moshe Y. Vardi The Hybrid mu-Calculus Carsten Lutz NExpTime-complete Description Logics with Concrete Domains R. Pliuskevicius Deduction-based Decision Procedure for a Clausal Miniscoped Fragment of FTL Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev A tableau calculus for temporal description logic: the constant domain case Juergen Giesl, Deepak Kapur Decidable Classes of Inductive Theorems Arnon Avron, Iddo Lev Canonical Propositional Gentzen-Type Systems Aart Middeldorp, Seitaro Yuuki Approximating Dependency Graphs using Tree Automata Techniques Haarslev, Volker, MÃ¶ller, Ralf, Turhan, Anni-Yasmin Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics Bernard Boigelot, SÃ©bastien Jodogne, Pierre Wolper On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables Haarslev, V., Moeller, R., Wessel, M. The Description Logic ALCNHR Extended with Concrete Domains: A Practically Motivated Approach Gilles Audemard, Laurent Henocque The eXtended Least Number Heuristic Nicolas Peltier A general method for using schematizations in automated deduction Franz Baader, Stephan Tobies The Inverse Method Implements the Automata Approach for Modal Satisfiability Marco Benedetti Conditional Pure Literal Graphs CERRITO Serenella, CIALDEA-MAYER Marta Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-Rigid Designation Bernhard Beckert, Steffen Schlager A Sequent Calculus for First-order Dynamic Logic with Trace Modalities Pablo Armelin, David Pym Bunched Logic Programming (Extended Abstract)) W. Reif, G. Schellhorn, A. Thums Flaw Detection in Formal Specification Stefan Szeider NP-Completeness of Refutability by Literal-Once Resolution Xavier Urbain Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems Sylvie Doutre, Jerome Mengin Preferred Extensions of Argumentation Frameworks: Query Answering and Computation Reiner Haehnle, Neil V. Murray, Erik Rosenthal Ordered Resolution vs. Connection Graph Resolution Andrea Formisano, Eugenio G. Omodeo, Marco Temperini Instructing equational set-reasoning with Otter Martin Giese Incremental Closure of Free Variable Tableaux Hans de Nivelle, Ian Pratt-Hartmann A Resolution-Based Decision Procedure for the Two-Variable fragment with Equality Marko Luther More On Implicit Syntax Kewen Wang A Top-down Procedure for Disjunctive Well-founded Semantics Brigitte Pientka Termination and Reduction Checking for Higher-Order Logic Programs Enrico Giunchiglia, Massimo Maratea, Armando Tacchella, Davide Zambonin Evaluating search heuristics and optimization techniques in propositional satisfiability JÃ¼rgen Stuber A Model-based Completeness Proof of Extended Narrowing And Resolution Joshua S. Hodas, Naoyuki Tamura LolliCoP -- A Linear Logic Implementation of a Lean Connection-Method TheoremProver for First-Order Classical Logic Uwe Egly, Stephan Schmitt Deriving Modular Programs from Short Proofs Christopher Lynch, Barbara Morawska Decidability and Complexity of Finitely Closable Linear Equational Theories Uwe Waldmann Superposition and Chaining for Totally Ordered Divisible Abelian Groups(Extended Abstract) Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov On the Evaluation of Indexing Techniques for Theorem Proving Harald Ganzinger, David McAllester Bottum-up deduction with deletion Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Context trees 4) List of accepted System Descriptions --------------------------------------- (24 submitted, 19 accepted) Maria Paola Bonacina Combination of distributed search and multi-search in Peers-mcd.d Dominique PASTRE Muscadet 2.3: A Knowledge-based Theorem Prover Based on Natural Deduction Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Alexey Nogin JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants Michael Beeson A Second-order Theorem Prover applied to Circumscription Peter F. Patel-Schneider, Roberto Sebastiani A System and Methodology for Generating Random Modal Formulae Haarslev, V., Moeller, R. RACE System Description C. Anger, K. Konczak, Th. Linke NoMoRe: A System for NonMonotonic Reasoning with logic Programs under Answer Set Semantic Jens Happe The ModProf Theorem Prover Stephan Schulz System Abstract: E 0.61 Alessandro Armando, Luca Compagna, Silvio Ranise System Description: RDL---Rewrite and Decision procedure Laboratory Kahlil Hodgson, John Slaney Development of a Semantically Guided Theorem Prover Armin Fiedler P.rex: An Interactive Proof Explainer Reinhold Letz, Gernot Stenz DCTP -- A Disconnection Calculus Theorem Prover -- System Abstract D. Larchey-Wendling, D. Mery, D. Galmiche STRIP: Structural sharing for efficient proof-search Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella QuBE: A system for deciding Quantified Boolean Formulas Satisfiability Joerg Luecke Hilberticus - a Tool Deciding an Elementary Sublanguage of Set Theory Farinas del Cerro, Luis, Fauthoux, David, Gasquet, Olivier, Herzig, Andreas, Longin, Dominique, Massacci, Fabio Lotrec: The Generic Tableau Prover for Modal and Description Logics JÃ¼rgen Avenhaus, Bernd LÃ¶chner CCE: Testing Ground Joinability Alexandre Riazanov, Andrei Voronkov Vampire 1.1 (system description) -- Peter Baumgartner Tel. (Giessen): +49 641 99-32160 Mail: peter(a)uni-koblenz.de Tel. (Koblenz): +49 261 287-2777 WWW: http://www.informatik.uni-giessen.de/staff/baumgart/

1 0

LAST CFP: FORMAL STRUCTURES IN COMPUTER SCIENCE
by Yuri Velinov 19 Mar '01

19 Mar '01

LAST CALL FOR PAPERS FORMAL STRUCTURES IN COMPUTER SCIENCE Organized by Y. Velinov, University of Natal Invited Session of the SCI'2001 Conference The Fifth World Multi-Conference on Systemics, Cybernetics and Informatics, Orlando, Florida, USA, July 22--25, 2001 Professor Nagib Callaos, General Chair URL http://www.iiis.org/sci ------------------------- TOPICS OF THE INVITED SESSION: A rich variety of formal models are currently in use in every field of the contemporary information technology. New formal structures are frequently introduced to model real world situations. Old, sometimes almost forgotten, are revived finding new applications. The aim of the present session is, instead of concentrating on a particular approach, to get together researchers from different areas to share ideas, approaches and their practical efficiency. The scope of the session includes set-theoretical, relational, logical or categorical structures. More specific areas like Petri nets or Automata theory are also welcome. SUBMISSION ------------ Potential authors are asked to inform for their intention to submit a paper as soon as possible by sending a short abstract to yuri(a)cs.unp.ac.za. Potential authors are expected to send the draft of their paper for reviewing before 12 April 2001 in PS (possibly zipped) or PDF format to yuri(a)cs.unp.ac.za. Instructions for preparing a paper for the session can be found at the conference site. The invited sessions will be published by IIIS (International Institute of Informatics and Systemics) as books with multiple authors. IMPORTANT DATES : ----------------- April, 12, 2001. Deadline for submitting paper drafts. April, 30, 2001. Deadline for acceptations. May, 20, 2001. Deadline for sending the camera-ready papers.

1 0

Call for papers GETCO 2001
by Philippe Gaucher 17 Mar '01

17 Mar '01

3rd workshop on Geometric and Topological Methods in Concurrency GETCO 2001 hosted by Concur 2001, , and Aalborg University Venue: Aalborg University, Denmark Conference dates: CONCUR: August 21-24, 2001 GETCO: August 25, 2001 Call for papers Scope of the workshop The main mathematical disciplines that have been used in computer science are discrete mathematics (especially, graph theory and ordered structures), logics (mostly proof theory for all kinds of logics, classical, intuitionistic, modal etc.) and category theory (cartesian closed categories, topoi etc.). General Topology has also been used for instance in denotational semantics, with relations to ordered structures in particular. Recently, ideas and notions from mainstream "geometric" topology and algebraic topology have entered the scene in Concurrency Theory and Distributed Systems Theory (some of them based on older ideas). They have been applied in particular to problems dealing with coordination of multi-processor and distributed systems (see the historical note ). Among those are techniques borrowed from algebraic and geometric topology: Simplicial techniques have led to new theoretical bounds for coordination problems. Higher dimensional automata have been modelled as cubical complexes with a partial order reflecting the time flows, and their homotopy properties allow to reason about a system's global behaviour. The first workshop on the subject Geometric and Topological Methods in Concurrency Theory has been held in Aalborg, Denmark, in June 1999. GETCO 2000 was organised as a workshop affiliated with CONCUR 2000 at Penn State University.The recent volumes 10 of Math. Struct. in Comp. Science and 39, issue 2, of Electr. Notes Theor. Comp. Science have been devoted to this area. The 3rd workshop in this series will be organised as a satellite to CONCUR 2001 at Aalborg University (Aug.21 - Aug.24). It aims at bringing together researchers from both the mathematical (geometry, topology, algebraic topology etc.) and computer scientific side (concurrency theorists, semanticians, researchers in distributed systems etc.) with an active interest in these or related developments. Topics include (but are not limited to) Semantics, Concurrency Theory, Model-checking, Abstract Interpretation, Fault-tolerant Protocols for Distributed Systems, Geometrical/Topological models, Applications of algebraic topology, Category theory etc. Paper submission The deadline for submission to the workshop is May 20, 2001 (midnight). Submissions may be of two forms: * Short abstracts: up to 4 pages, in format A4, typeset 11 points * Full papers: up to 12 pages, in format A4, typeset 11 points (excluding bibliography and technical appendices) Both forms of submission should include a separate page with the following informations: title, author(s), corresponding author, contact information and a 12-15 lines summary. Simultaneous submission to other conferences or journals is only allowed for short abstracts. Electronic submission is strongly encouraged. The paper or abstract should be sent by e-mail in the form of a postscript file to both the addresses raussen(a)math.auc.dk and goubault(a)aigle.saclay.cea.fr. The accompanying page should be sent in a separate email message. If surface mail has to be used, then 3 copies of the paper/abstract should be sent to: Martin Raussen, Dept. of Mathematical Sciences, Aalborg University, Fredrik Bajersvej 7G, DK-9220 Aalborg Ãst, Denmark. Publication Accepted papers will be made available in the BRICS Notes series. For full publication -- only full papers -- first contacts have been taken with Electronic Notes in Theoretical Computer Science. Acceptance of papers will be decided upon after the workshop. Registration The registration for GETCO'2001 is made through the registration for Concur'2001 with no extra-charge. Programme Committee (to be completed): * Patrick Cousot, Ecole Normale Superieure, Paris, France * Lisbeth Fajstrup, Aalborg University, Denmark * Eric Goubault, Commissariat Ã l'Energie Atomique, France * Jeremy Gunawardena, Hewlett-Packard BRIMS, England * Martin Raussen, Aalborg University, Denmark * Vladimiro Sassone, Catania University, Italy Important Dates * Call for Papers: March 13, 2001 * Deadline for submission: May 20, 2001 * Notification of acceptance: July 1, 2001 * Final version due: July 29, 2001 * CONCUR: August 21-August 24, 2001 * GETCO: August 25, 2001 Local Organization * Lisbeth Fajstrup, Aalborg University, Denmark * Eric Goubault, Commissariat Ã l'Energie Atomique, France * Martin Raussen, Aalborg University, Denmark Contact http://www.math.auc.dk/~raussen/GETCO/getco.html Martin Raussen Department of Mathematics Aalborg University Fredrik Bajersvej 7G DK-9220 Aalborg Ãst Denmark Phone: (+45) 96 35 88 55 Fax: (+45) 98 15 81 29 Email: raussen(a)math.auc.dk

1 0