February 2010 - Categories - categories.org.au

Research positions
by Maria Manuel Clementino 26 Feb '14

26 Feb '14

5-YEAR RESEARCH POSITIONS The Centre for Mathematics of the University of Coimbra (CMUC) invites applications for five 5-year research positions in all areas of Mathematics. Applicants should have a PhD in Mathematics and at least three years of post-doctoral experience, with an international-level publication record and demonstrated ability to perform independent research. Preference will be given to candidates working in one of the areas in which the members of CMUC are currently active. A very good command of English is required. The appointments will be made for three years, renewable for two more. Successful applicants are expected to develop research within the areas of interest of CMUC. They should also contribute to graduate studies, supervising students from the Department of Mathematics. The basic salary is equivalent to the index 195 of the Portuguese research career (in the order of 42 500 euros a year), in accordance with the Ciência 2008 guidelines http://alfa.fct.mctes.pt/apoios/contratacaodoutorados/edital2008 Benefits include private health insurance and social security. Applicants should send • cover sheet (available from www.mat.uc.pt/cmuc/coversheet.pdf) including names and contact information of three persons who can provide a letter of recommendation • curriculum vitae (publication list included) • a 5-year research proposal (2 pages max), emphasizing their own research goals as pdf files to cmuc(a)mat.uc.pt. The subject of the e-mail message must include the job reference C2008 FCTUC CMUC v15-v19. The deadline for applications is *September 10, 2008.* ------------------------------ More information can be found at www.mat.uc.pt

1 1

separable locale
by Thomas Streicher 17 May '13

17 May '13

Recently rereading Fourman's "Continuous Truth" I came across the term "separable locale" but could nowhere find an explanation. Does it mean a cHa A for which there exists a countable subset B such that ever a in A is the supremum of those b in B with b leq a. This would be the point free account of "second countable", i.e. having a countable basis. Of course, second countable T_) spaces are separable, i.e. have a countable dense set. Is this reading the "usual" one? Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 4

Foundations?
by F W Lawvere 03 Sep '10

03 Sep '10

Down with "Foundations"! Up with algebra! Dear Friends, Presumably I am among those who are being "vilified" as "lovers of categories as foundation". By avoiding any precise definition, such a formulation might appeal to the widespread justified boredom induced by the past hundred years of "foundations as justification". Whenever I used the word "foundation" in my writings over the past forty years, I have explicitly rejected that reactionary use of the term and instead used the definition implicit in the work of my teachers Truesdell and Eilenberg. Namely, an important component of mathematical practice is the careful study of historical and contemporary analysis, geometry, etc. to extract the essential recurring concepts and constructions; making those concepts and constructions (such as homomorphism, functional, adjoint functor, etc.) explicit provides powerful guidance for further unified development of all mathematical subjects, old and new. What is the primary tool for such summing up of the essence of ongoing mathematics? Algebra! Nodal points in the progress of this kind of research occur when, as is the case with the finite number of axioms for the metacategory of categories, all that we know so far can be expressed in a single sort of algebra. I am proud to have participated with Eilenberg, Mac Lane, Freyd, and many others, in bringing about the contemporary awareness of Algebra as Category Theory Had it not been for the century of excessive attention given to the alleged possibility that mathematics is inconsistent, with the accompanying degradation of the F-word, we would still be using it in the sense known to the general public: the search for what is "basic". We, who supposedly know the explicit algebra of homomorphisms, functionals, etc. are long remiss in our duty to find ways to utilize those concepts also in guiding high school calculus. Best wishes, Bill Bibliography: - The Category of Categories as a Foundation for Mathematics, La Jolla conference 1965, Springer (1966) - Adjointness in Foundations, Dialectica, (1969), to be reprinted in TAC - Foundations and Applications: Axiomatization and Education, Bulletin of Symbolic Logic, (2003) vol 9, pp 213-224 - Sets for Mathematics, w/ Bob Rosebrugh, Cambridge Univ. Press, (2003) ************************************************************ F. William Lawvere Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************

2 1

Composing modifications
by David Leduc 03 Mar '10

03 Mar '10

Dear all, I am reading Basic Bicategories by Tom Leinster, and I have basic questions about modifications. 1) Suppose that n, n', m and m' are transformations such that m * n and m' * n' are well defined, where * denotes horizontal (= Godement) composition of transformations. >>From given modifications a:m-->m' and b:n-->n' is there a way to derive a modification from m * n to m' * n' ? 2) There are two ways to compose transformations: vertical and horizontal. What are the ways to compose modifications? Thanks for your help, David [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

abstraction of notation from sets.
by peasthope＠shaw.ca 01 Mar '10

01 Mar '10

When S is a set, the notation "a \epsilon S" is familiar. Is this ever extended to CT? All the texts I recall use natural language such as "A is an object of C". What if a more symbolic notation is required? Thanks, ... Peter E. -- Google "pathology workshop" [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

6 6

Re: abstraction of notation from sets.
by Richard Garner 28 Feb '10

28 Feb '10

> One cannot write "a \in C" to mean that a is an object of > the category C, at least as long as \in is restricted to > its precise set-theoretic meaning. However, in my > experience it is fairly common to write "a \in C" with this > meaning, although perhaps not so common in formal > mathematical writing. > One can refer to this sort of thing perjoratively as an "abuse of > notation," but one can also regard it as a perfectly legitimate part of > informal mathematical language which is not captured by the > set-theoretic encoding. One could also formalize it by regarding the > symbol "\in" as "overloaded" in a precise sense analogous to programming > languages. I think it is more perspicuous to treat this, not as an overloading of \in, but as an "implicit conversion" associated to the notion of category; that is, we allow the forgetful functor Cat->Set to be applied silently in contexts which otherwise would not type-check. In fact the vast majority of "abuses of notation" are of this character, when applied to, for example, any forgetful functor from an Eilenberg-Moore category; the discrete category functor Set->Cat; the Yoneda embedding C -> [C^op, Set]; the forgetful functor from universal cones to their vertex, etc, etc. In principle this becomes problematic as soon as the category generated by all such implicit conversions has non-identity idempotents; in practice, this category is free on a graph and we hope to identify a shortest path between two vertices! Richard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

PhD position in ICT on Formal Verification via SMT available in Trento
by Roberto Sebastiani 27 Feb '10

27 Feb '10

--------------------------------------------------------------------------- [[[ We apologize if you receive multiple copies of this message ]]] --------------------------------------------------------------------------- -------------------------------------------------------------- PLEASE FORWARD THIS EMAIL TO WHOEVER YOU MAY THINK INTERESTED. -------------------------------------------------------------- Posted: February 26, 2010 One Doctoral Student Position in Information and Communication Technologies on the research project "WORD-LEVEL FORMAL VERIFICATION VIA SMT SOLVING" is available at the International Doctorate School in Information and Communication Technologies (http://www.ict.unitn.it/) of the University of Trento, Italy, under the joint supervision of Dr. ALESSANDRO CIMATTI, Embedded Systems Research Unit, FBK-Irst, via Sommarive 18, I-38100 Povo, Trento, Italy http://sra.fbk.eu/people/cimatti/, cimatti[at]fbk[dot]eu Prof. ROBERTO SEBASTIANI Software Engineering & Formal Methods Research Program DISI, University of Trento, via Sommarive 14, I-38100 Povo, Trento, Italy http://disi.unitn.it/~rseba/. rseba[at]disi[dot]unitn[dot]it The research activity will be carried out jointly within the Embedded Systems (ES) Research Unit of the Center for Scientific and Technological Research of the Fondazione Bruno Kessler (FBK), Trento, and the Software Engineering & Formal Methods (SE&FM) Research Program, at Department of Information Engineering and Computer Science (DISI) of University of Trento. The research activity will aim at investigating and developing novel techniques, methodologies and support tools for Satisfiability Modulo Theories (SMT) for the verification of WORD-level circuit designs. This work will be part of the "Word-Level Formal Verification via SMT Solving" (WOLFLING) project, a three-year custom research project supported by SRC/GRC (http://grc.src.org/fr/S200802_Call.asp) in strict collaboration with the Formal Verification Group at Intel, Haifa, Israel. SMT tools will be developed on top of the MathSAT SMT platform (http://mathsat4.disi.unitn.it) and Formal Verification tools will be developed on top of the NuSMV Model Checking platform (http://nusmv.fbk.eu) Both platforms are jointly developed and maintained by ES and SE&FM. The selected candidate will be initially enrolled in a stage and, if he/she passes the selection of the Ph.D. school, he/she will be enrolled as Ph.D. students. Ph.D. courses will start in Autumn 2010, and the thesis must be completed in three or four years. People enrolled in a stage and subsequent Ph.D. courses are expected to move to Trento, and will receive monetary support during both phases of their activity. Candidate Profile ================= The ideal candidate should have an MS or equivalent degree in computer science, mathematics or electronic engineering, and combine solid theoretical background and excellent software development skills. The candidate should be able to work in a collaborative environment, with a strong commitment to reaching research excellence and achieving assigned objectives. Background knowledge and/or previous experience in the following areas (in order of preference), though not strictly mandatory, will be considered very favorably: - Satisfiability Modulo Theory (SMT) - Propositional Satisfiability (SAT) - Embedded Systems Design Languages (e.g. Verilog, VHDL) - Symbolic Model Checking - Automated Reasoning - Constraint Solving and Optimization Applications and Inquiries ========================== Interested candidates should inquire for further information and/or apply by sending email to Prof. Sebastiani (rseba[at]disi[dot]unitn[dot]it) with Dr. Cimatti (cimatti[at]fbk[dot]eu) in CC. Applications should contain a statement of interest, with a Curriculum Vitae, and three reference persons. PDF format is strongly encouraged. Emails will be automatically processed and should have 'PHD ON WOLFLING PROJECT' as subject. Contact Person ============== Prof. ROBERTO SEBASTIANI Software Engineering & Formal Methods Research Program DISI, University of Trento, via Sommarive 14, I-38100 Povo, Trento, Italy http://disi.unitn.it/~rseba/. mailto: rseba[at]disi[dot]unitn[dot]it The Embedded Systems Research Unit at FBK ========================================= The Embedded Systems Unit consists of about 15 persons, including researchers, post-Doc, Ph.D. students, and programmers. The Unit carries out research, tool development and technology transfer in the fields of design and verification of embedded systems. Current research directions include: * Satisfiability Modulo Theory, and its application to the verification of hardware, embedded critical software, and hybrid systems (Verilog, SystemC, C/C++, StateFlow/Simulink). * Formal Requirements Analysis based on techniques for temporal logics (consistency checking, vacuity detection, input determinism, cause-effect analysis, realizability and synthesis). * Formal Safety Analysis, based on the integration of traditional techniques (e.g. Fault-tree analysis, FMEA) with symbolic verification techniques. The Embedded Systems Unit is part of Fondazione Bruno Kessler, formerly Istituto Trentino di Cultura, a public research institute of the Autonomous Province of Trento (Italy), founded in 1976. The institute, through its center for the scientific and technological research, is active in the areas of Information Technology, Microsystems, and Physical Chemistry of Surfaces and Interfaces. Today, FBK is an internationally recognized research institute, collaborating with industries, universities, and public and private laboratories in Italy and abroad. The institute's applied and basic research activities aim at resolving real-world problems, driven by the need for technological innovation in society and industry. The SW Engineering & Formal Methods Research Program at DISI ============================================================ The SW Engineering & Formal Methods R. P. at DISI currently consists on 5 faculties, 4 post-docs and 19 PhD students. The Unit carries out research, tool development and technology transfer in the fields of Goal-Oriented Requirements Engineering, Agent-oriented SW engineering, Security, and Formal Methods. Referring to formal methods, current research directions include: * Satisfiability Modulo Theory, and its application to the verification of hardware, embedded critical software, and hybrid systems. * Advanced Model Checking Techniques for Formal Verification of hardware, embedded critical software, and hybrid systems. * Applications of Propositional Satisfiability (SAT) to various domains. The R.P. is part of the Department of Information Engineering and Computer Science, DISI (http://disi.unitn.it/) of University of Trento. University of Trento in the latest years has always been rated among the top-three small&medium-size universities in Italy. DISI currently consists of 50 faculties, 68 research staff and support people, 21 postdocs and 146 Doctoral students, plus administrative and technical staff. DISI covers all the different areas of information technology (computer science, telecommunications, and electronics) and their applications. These disciplines above are studied individually but also with a strong focus on their integration, Location ======== Trento is a lively town of about 100.000 inhabitants, located 130 km south of the border between Italy and Austria. It is well known for the beauty of its mountains and lakes, and it offers the possibility to practice a wide range of sports. Trento enjoys a rich cultural and historical heritage, and it is the ideal starting point for day trips to famous towns such as Venice or Verona, as well as to enjoy great naturalistic journeys. Detailed information about Trento and its region can be found at http://www.trentino.to/home/index.html?_lang=en. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Grothendieck and SGA
by David Roberts 26 Feb '10

26 Feb '10

Hi all, apparently Grothendieck has requested that work on republishing SGA stop: http://www.math.polytechnique.fr/~laszlo/sga4.html Does anyone know anything about this? David Roberts [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 4

FICS 2010 -- call for papers
by Luigi Santocanale 25 Feb '10

25 Feb '10

/* Apologies for multiple posting */ Call for Papers (Extended Abstracts) 7th Workshop on Fixed Points in Computer Science, FICS 2010 Brno, Czech Republic, August 21-22 2010 a satellite workshop to MFCS & CSL 2010 http://www.lif.univ-mrs.fr/fics2010/ Background Fixed points play a fundamental role in several areas of computer science and logic by justifying induction and recursive definitions. The construction and properties of fixed points have been investigated in many different frameworks such as: design and implementation of programming languages, program logics, databases. The aim of the workshop is to provide a forum for researchers to present their results to those members of the computer science and logic communities who study or apply the theory of fixed points. Previous workshops were held in Brno (1998, MFCS/CSL workshop), Paris (2000, LC workshop), Florence (2001, PLI workshop), Copenhagen (2002, LICS (FLoC) workshop), Warsaw (2003, ETAPS workshop), Coimbra (2009, CSL workshop). Topics include, but are not restricted to: * categorical, metric and ordered fixed point models * fixed points in algebra and coalgebra * fixed points in languages and automata * fixed points in programming language semantics * the mu-calculus and fixed points in modal logic * fixed points in process algebras and process calculi * fixed points in the lambda-calculus, functional programming and type theory * fixed points in relation to dataflow and circuits * fixed points in logic programming and theorem proving * finite model theory, descriptive complexity theory, fixed points in databases Invited speakers * Arnaud Carayol, Laboratoire d'informatique Gaspard-Monge. * tba * tba Contributed talks Selection of contributed talks is based on extended abstracts/short papers of 3...6 pp formatted with easychair.cls. Submission is via EasyChair, by June 13 2010. The authors will be notified of acceptance/rejection by July 10 2010. Camera-ready versions of the accepted contributions will be published for distribution at the workshop as a technical report. Journal publication If the number and quality of submissions and accepted talks warrant this, EDP Sciences will publish a special issue of Theoretical Informatics and Applications. With one exception, the special issues of the previous FICS editions appeared in this journal. The special issue of FICS 2009 will also appear there. FICS Program Committee Thorsten Altenkirch (University of Nottingham) Giovanna d'Agostino (University of Udine) Peter Dybjer (Chalmers University of Technology) Zoltán Ésik (University of Szeged) Anna Ingólfsdóttir (Reykjavík University) Gerhard Jäger (University of Bern) Ralph Matthes (IRIT, Toulouse) Andrzej Murawski (University of Oxford) Damian Niwinski (Warsaw University) Luigi Santocanale (LIF, Marseille) Alex Simpson (University of Edinburgh) Jean-Marc Talbot (LIF, Marseille) Tarmo Uustalu (Institute of Cybernetics, Tallinn) Yde Venema (University of Amsterdam) Igor Walukiewicz (LaBRI, Bordeaux) Sponsors Laboratoire d'Informatique Fondamentale de Marseille Université de Provence -- Luigi Santocanale LIF/CMI Marseille Tél: 04 91 11 35 74 http://www.cmi.univ-mrs.fr/~lsantoca/ Fax: 04 91 11 36 02 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

ICFP 2010: Second call for papers
by Wouter Swierstra 25 Feb '10

25 Feb '10

===================================================================== Second Call for Papers ICFP 2010: International Conference on Functional Programming Baltimore, Maryland, 27 -- 29 September 2010 http://www.icfpconference.org/icfp2010 ===================================================================== Important Dates (at 14:00 UTC) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Submission: 2 April 2010 Author response: 24 -- 25 May 2010 Notification: 7 June 2010 Final papers due: 12 July 2010 Scope ~~~~~ ICFP 2010 seeks original papers on the art and science of functional programming. Submissions are invited on all topics from principles to practice, from foundations to features, from abstraction to application. The scope includes all languages that encourage functional programming, including both purely applicative and imperative languages, as well as languages with objects or concurrency. Particular topics of interest include * Language Design: type systems; concurrency and distribution; modules; components and composition; metaprogramming; relations to object-oriented or logic programming; interoperability * Implementation: abstract machines; compilation; compile-time and run-time optimization; memory management; multi-threading; exploiting parallel hardware; interfaces to foreign functions, services, components or low-level machine resources * Software-Development Techniques: algorithms and data structures; design patterns; specification; verification; validation; proof assistants; debugging; testing; tracing; profiling * Foundations: formal semantics; lambda calculus; rewriting; type theory; monads; continuations; control; state; effects * Transformation and Analysis: abstract interpretation; partial evaluation; program transformation; program calculation; program proof * Applications and Domain-Specific Languages: symbolic computing; formal-methods tools; artificial intelligence; systems programming; distributed-systems and web programming; hardware design; databases; XML processing; scientific and numerical computing; graphical user interfaces; multimedia programming; scripting; system administration; security; education * Functional Pearls: elegant, instructive, and fun essays on functional programming The conference also solicits Experience Reports, which are short papers that provide evidence that functional programming really works or describe obstacles that have kept it from working in a particular application. Abbreviated instructions for authors ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ By 2 April 2010, 14:00 UTC, submit an abstract of at most 300 words and a full paper of at most 12 pages (6 pages for an Experience Report), including bibliography and figures. The deadline will be strictly enforced and papers exceeding the page limits will be summarily rejected. Authors have the option to attach supplementary material to a submission, on the understanding that reviewers may choose not to look at it. A submission will be evaluated according to its relevance, correctness, significance, originality, and clarity. It should explain its contributions in both general and technical terms, clearly identifying what has been accomplished, explaining why it is significant, and comparing it with previous work. The technical content should be accessible to a broad audience. Functional Pearls and Experience Reports are separate categories of papers that need not report original research results and must be marked as such at the time of submission. Detailed guidelines on both categories are on the conference web site. Each submission must adhere to SIGPLAN's republication policy, as explained on the web at http://www.acm.org/sigplan/republicationpolicy.htm. Proceedings will be published by ACM Press. Authors of accepted submissions are expected to transfer the copyright to the ACM. Presentations will be videotaped and released online if the presenter consents by signing an additional permission form at the time of the presentation. Formatting: Submissions must be in PDF format printable in black and white on US Letter sized paper and interpretable by Ghostscript. If this requirement is a hardship, make contact with the program chair at least one week before the deadline. Papers must adhere to the standard ACM conference format: two columns, nine-point font on a ten-point baseline, with columns 20pc (3.33in) wide and 54pc (9in) tall, with a column gutter of 2pc (0.33in). A suitable document template for LATEX is available from SIGPLAN at http://www.acm.org/sigs/sigplan/authorInformation.htm. Submission: Submissions will be accepted electronically at a URL to be named later. Improved versions of a paper may be submitted at any point before the submission deadline using the same web interface. Author response: Authors will have a 48-hour period, starting at 14:00 UTC on 24 May 2010, to read and respond to reviews. Special Journal Issue: There will be a special issue of the Journal of Functional Programming with papers from ICFP 2010. The program committee will invite the authors of select accepted papers to submit a journal version to this issue. Organization ~~~~~~~~~~~~ Conference Chair Paul Hudak, Yale University Program Chair Stephanie Weirich, University of Pennsylvania Program Committee: Umut Acar, Max Planck Institute for Software Systems Zena Ariola, University of Oregon James Cheney, University of Edinburgh Peter Dybjer, Chalmers University of Technology Robert Bruce Findler, Northwestern University Andy Gill, Kansas University Fritz Henglein, University of Copenhagen Michael Hicks, University of Maryland, College Park Patricia Johann, University of Strathclyde Andres Löh, Utrecht University Simon L. Peyton Jones, Microsoft Research Didier Rémy, INRIA Paris-Rocquencourt John Reppy, University of Chicago Manuel Serrano, INRIA Sophia-Antipolis Matthieu Sozeau, Harvard University [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0