January 2016 - Categories - categories.org.au

Funded Doctoral Positions in Computer Science in Austria (LogiCS)
by list-announcer＠dbai.tuwien.ac.at 29 Jan '16

29 Jan '16

(* Apologies if you got multiple copies of this email *) Funded Doctoral Positions in Computer Science [http://logic-cs.at/phd/] TU Wien, TU Graz, and JKU Linz are seeking exceptionally talented and motivated students for their joint doctoral program LogiCS. The LogiCS doctoral college focuses on interdisciplinary research topics covering (i) computational logic, and applications of logic to (ii) databases and artificial intelligence as well as to (iii) computer-aided verification. THE PROGRAM LogiCS is a doctoral college focusing on logic and its applications in computer science. Successful applicants will work with and be supervised by leading researchers in the fields of computational logic, databases and knowledge representation, and computer-aided verification. FACULTY MEMBERS M. Baaz A. Biere R. Bloem A. Ciabattoni U. Egly T. Eiter C. Fermueller R. Grosu A. Leitsch M. Ortiz R. Pichler S. Szeider H. Tompits H. Veith G. Weissenbacher The LogiCS faculty comprises 15 renowned researchers with strong records in research, teaching and advising, complemented by 12 associated members who further strengthen the research and teaching activities of the college. Details are provided on http://logic-cs.at/faculty/ POSITIONS AND FUNDING We are looking for 1 doctoral students per faculty member, where 30% of the positions are reserved for highly qualified female candidates. The doctoral positions are funded for a period of 3 years according to the funding scheme of the Austrian Science Fund (details: http://www.fwf.ac.at/de/forschungsfoerderung/personalkostensaetze/) The funding can be extended for one additional year contingent on a placement at one of our international partner institutions. CURRENT RESEACH AREAS At the moment we are particularly looking for people in the following areas: * Automated reasoning and symbolic computation * Formal Verification of hybrid systems * Model Checking HOW TO APPLY Detailed information about the application process is available on the LogiCS web-page http://logic-cs.at/phd/ The applicants are expected to have completed an excellent diploma or master's degree in computer science, mathematics, or a related field. Candidates with comparable achievements will be considered on a case-by-case basis. Applications by the candidates need to be submitted electronically. Next application Deadline: March 1, 2016. LOGIC IN AUSTRIA Austria has a highly active and successful logic in computer science community. Recent activities include: vsl2014.at Vienna Summer of Logic, the Largest Conference in the History of Logic www.arise.or.at Austrian Research Network in Rigorous Systems Engineering vcla.at Vienna Center for Logic and Algorithms kgs.logic.at International Kurt Goedel Society HIGHEST QUALITY OF LIFE The Austrian cities Vienna, Graz, and Linz, located close to the Alps and surrounded by beautiful nature, provide an exceptionally high quality of life, with a vibrant cultural scene, numerous cultural events, world-famous historical sites, a large international community, a varied cuisine and famous coffee houses. For further information please contact: info(a)logic-cs.at [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Natural Language and Computer Science 2016
by larry moss 26 Jan '16

26 Jan '16

*CALL FOR PAPERS* Fourth Workshop on Natural Language and Computer Science NLCS '16 July 10, 2016 New York, NY http://www.indiana.edu/~iulg/nlcs.html A workshop affiliated with the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016) Paper submission deadline: May 10, 2016. AIMS AND SCOPE Formal tools coming from logic and category theory are important in both natural language semantics and in computational semantics. Moreover, work on these tools borrows heavily from all areas of theoretical computer science. In the other direction, applications having to do with natural language has inspired developments on the formal side. The workshop invites papers on both topics. Specific topics include, but are not limited to: ??? logic for semantics of lexical items, sentences, discourse and dialog ??? continuations in natural language semantics ??? formal tools in textual inference, such as logics for natural language inference ??? applications of category theory in semantics ??? linear logic in semantics ??? formal approaches to unifying data-driven and declarative approaches to semantics INVITED SPEAKERS Lucas Champollion, New York University Uli Sattler, University of Manchester PROGRAM COMMITTEE Chris Barker, New York University Cleo Condoravdi, Stanford University Philippe de Groote, Inria Gerard de Melo, Tsinghua University Valeria de Paiva, Nuance Communications Makoto Kanazawa, National Institute of Informatics Larry Moss, Indiana University Christian Retor??, Universit?? de Montpellier PAPER SUBMISSIONS May be made through Easychair: https://easychair.org/conferences/?conf=nlcs16 ORGANIZERS Chris Barker New York University Email: chris barker at nyu . edu Valeria de Paiva Nuance.com Email: Valeria.dePaiva at nuance .com Larry Moss Indiana University Email: lsm at cs.indiana . edu IMPORTANT DATES Paper submission: May 10, 2016 Notification: May 20, 2016 Electronic versions due: June 14, 2016 Workshop: July 10, 2016??? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

AARMS Summer School Announcement
by Dorette Pronk 24 Jan '16

24 Jan '16

ANNOUNCEMENT: AARMS Summer School at Dalhousie University July 11 - August 5, 2016 The AARMS Summer School 2016 will offer courses in category theory and number theory and combinatorics. Directors: Dr. Dorette Pronk, Dalhousie University and Dr. Geoffrey Cruttwell, Mount Allison University The AARMS summer school is intended for graduate students and promising undergraduate students from all parts of the world. Each participant is required to register for two of the four courses in order to receive support from AARMS. Each course consists of five ninety-minute lecture sessions each week. These are graduate courses approved by Dalhousie and we will facilitate transfer credit to the extent possible. The courses of interest to people on this list are the following. Higher Category Theory and Categorical Logic Instructors: Dr. Michael Shulman, University of San Diego, and Dr. Peter Lumsdaine, Stockholm University Description: This course will introduce students to the relationship between category theory and logic, and its emerging generalization to higher category theory. On the one hand, category theory provides a flexible and powerful semantics for logic, uniting for instance forcing models of set theory with domain semantics for programming languages. On the other hand, logic provides an "internal language" for categories, that can greatly simplify the proofs of general theorems. We will discuss the classical version of this correspondence that applies to ordinary categories, including elementary toposes. Then we will introduce some basic concepts of higher category theory, and end with a brief introduction to homotopy type theory, a logic that corresponds to certain higher categories. Categories, Quantum Computation and Topology Instructor: Dr. Jamie Vicary, University of Oxford Description: This course will introduce the theory of monoidal categories, an approach to mathematics which combines algebra and geometry into a single subject, and investigates its applications in quantum computation and topology. An emphasis will be on graphical calculi, which allow us to prove theorems using pictures, rather than traditional mathematical syntax. The course will also have a practical component, using the proof assistant Globular to formalize and investigate the results we encounter. Topics studied will include coherence, linear structures, duality, monoids and comonoids, Frobenius and Hopf algebras, quantum groups, quantum protocols, higher categories, and topological quantum field theory. There will also be a week with preparatory lectures on basic category theory by Geoff Cruttwell, from July 4 till July 8. For more information and the application form, visit the summer school website, https://aarms.math.ca/the-2016-aarms-summer-school/ Don't wait too long with applying as we can only support 20 students in category theory. Since CT2016 will be held in Halifax right after this summer school, interested students may want to get a dorm room at Dalhousie that they can keep for the whole time. There is one residence house (with kitchen facilities) that we would like to use for this, but we can only reserve it if there is enough interest. So if you are interested in this option contact us as soon as possible to show your interest and indicate the dates for your time in Halifax. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Call for Nominations: The 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation
by Gordon Plotkin 23 Jan '16

23 Jan '16

The 2016 Alonzo Church Award for Outstanding Contributions to Logic and Computation Call for Nominations Introduction An annual award, called the Alonzo Church Award for Outstanding Contributions to Logic and Computation, was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or by a small group of papers published within the past 25 years. This time span allows the lasting impact and depth of the contribution to have been established. The award can be given to an individual, or to a group of individuals who have collaborated on the research. For the rules governing this award, see http://siglog.hosting.acm.org/the-alonzo-church-award-for-outstanding-contr… Eligibility and Nominations The contribution must have appeared in a paper or papers published within the past 25 years. Thus, for the 2016 award, the cut-off date is January 1, 1991. When a paper has appeared in a conference and then in a journal, the date of the journal publication will determine the cut-off date. In addition, the contribution must not yet have received recognition via a major award, such as the Turing Award, the Kanellakis Award, or the Gödel Prize. (The nominee(s) may have received such awards for other contributions.) While the contribution can consist of conference or journal papers, journal papers will be given a preference. Nominations for the 2016 award are now being solicited. The nominating letter must summarize the contribution and make the case that it is fundamental and outstanding. The nominating letter can have multiple co-signers. Self-nominations are excluded. Nominations must include: a proposed citation (up to 25 words); a succinct (100-250 words) description of the contribution; and a detailed statement (not exceeding four pages) to justify the nomination. Nominations may also be accompanied by supporting letters and other evidence of worthiness. Nominations are due by March 1, 2016, and should be submitted to vardi(a)cs.rice.edu Presentation of the Award The 2016 award will be presented at LICS, the flagship conference of SIGLOG. The award will be accompanied by an invited lecture by the award winner, or by one of the award winners. The awardee(s) will receive a certificate and a cash prize of USD 2,000. If there are multiple awardees, this amount will be shared. Award Committee The 2016 Alonzo Church Award Committee consists of the following four members: Catuscia Palamidessi, Gordon Plotkin, Wolfgang Thomas, and Moshe Vardi (chair). [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Call for papers: CSL 2016
by European Association of Computer Science Logic 23 Jan '16

23 Jan '16

CALL FOR PAPERS CSL 2016 25th EACSL Annual Conference on Computer Science Logic August 29 -- September 1st, 2016, Marseille, France http://csl16.lif.univ-mrs.fr/ ------------------------------------------------------------------------ Abstract submission: April 8, 2016 Paper submission: April 15, 2016 Notification: June 11, 2016 ------------------------------------------------------------------------ Computer Science Logic (CSL) is the annual conference of the European Association for Computer Science Logic (EACSL). The conference is intended for computer scientists whose research activities involve logic, as well as for logicians working on issues significant for computer science. CSL 2016 is the 25th EACSL annual conference, and will be organized by Aix-Marseille Universit?? in Marseille, France. Scope ----- Suggested topics of interest include (but are not limited to): * automated deduction and interactive theorem proving, * constructive mathematics and type theory, * equational logic and term rewriting, * automata and games, game semantics, * modal and temporal logic, * model checking, * decision procedures, * logical aspects of computational complexity, * finite model theory, * computational proof theory, * bounded arithmetic and propositional proof complexity, * logic programming and constraints, * lambda calculus and combinatory logic, * domain theory, * categorical logic and topological semantics, * database theory, * specification, extraction and transformation of programs, * logical aspects of quantum computing, * logical foundations of programming paradigms, * verification and program analysis, * linear logic, * higher-order logic, * nonmonotonic reasoning. Invited Speakers ---------------- Alexandra Silva - University College, London, UK Anca Muscholl - University of Bordeaux, France Agata Ciabattoni - University of Vienna, Austria Libor Barto - University of Prague, Czech Republic Satellite events ---------------- Three affiliated workshops will be held as co-located events in the days following the conference: LCC'16: Logic and Computational Complexity 2016 (September 2) PLRR: Parametricity, Logical Relations and Realizability (September 2) QSLC: Quantitative Semantics of Logic and Computation (September 2-3) Submission guidelines --------------------- We expect that the CSL 2016 conference proceedings will be published in Leibniz International Proceedings in Informatics (LIPIcs). Authors are invited to submit papers of no more than 15 pages in LIPIcs style (including references) presenting work not previously published, fitting the scope of the conference. The submission is in two stages: * abstracts are due on April 8, 2016 (AoE); * final papers are due on April 15, 2016 (AoE). Both stages must be done via the EasyChair page for the conference: https://easychair.org/conferences/?conf=csl2016 Submitted papers must be written in English and must provide sufficient detail to allow the Programme Committee to assess the merits of the paper. Full proofs may appear in a technical appendix which will be read at the reviewers??? discretion. Authors are strongly encouraged to include a well written introduction which is directed at all members of the PC. Papers must not be submitted concurrently to another conference with refereed proceedings. The PC chairs should be informed of closely related work submitted to a conference or a journal. Papers authored or co-authored by members of the PC are not allowed. Programme Committee ------------------- Christel Baier ??? Technische Universit??t Dresden, Germany Mickael Benedikt ??? University of Oxford, UK Manuel Bodirsky ??? Technische Universit??t Dresden, Germany Sam Buss ??? University of California, USA Luis Caires ??? Universidade Nova de Lisboa, Portugal Giovanna D???Agostino ??? University of Udine, Italy Thomas Ehrhard ??? CNRS Universit?? Paris Diderot, France Emmanuel Filiot ??? Universit?? Libre de Bruxelles, Belgium Silvio Ghilardi ??? Universit?? degli Studi di Milano, Italy Valentin Goranko ??? Stockholm University, Sweden Anna Ing??lfsd??ttir ??? Reykjavik University, Iceland Laura Kov??cs ??? Chalmers University of Technology, Sweden Marta Kwiatkowska ??? University of Oxford, UK Christof L??ding ??? RWTH Aachen University, Germany Assia Mahboubi ??? INRIA Saclay Ile-de-France, France Guy McCusker ??? University of Bath, UK Magdalena Ortiz ??? TU Wien, Austria Sophie Pinchinat ??? Universit?? de Rennes 1, France Laurent Regnier ??? Aix-Marseille Universit??, France (co-chair) Sylvain Salvati ??? Universit?? de Bordeaux, France Ulrike Sattler ??? University of Manchester, UK Peter Selinger ??? Dalhousie University, Canada Thomas Streicher ??? Technische Universit??t Darmstadt, Germany Jean-Marc Talbot ??? Aix-Marseille Universit??, France (co-chair) Pawe?? Urzyczyn ??? Uniwersytet Warszawski, Poland Luca Vigan?? ??? King???s College London, UK Organising Committee -------------------- * Emmanuel Beffara * Benjamin Monmege * Luigi Santocanale * Laurent Regnier (co-chair) * Pierre-Alain Reynier * Jean-Marc Talbot (co-chair) * Lionel Vaux (all from Aix-Marseille Universit??, Marseille, France) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

type theory postdoc at Dalhousie University
by Peter Selinger 22 Jan '16

22 Jan '16

Dear colleagues, I invite applications for one postdoctoral position, starting between now and January 1, at Dalhousie University under my supervision. The successful applicant will work on a project entitled "Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language". Specifically, the project will involve the design of a type system for a type-safe functional programming language for quantum computing, loosely modelled on the Quipper language (http://www.mathstat.dal.ca/~selinger/quipper/) It will also involve developing the meta-theory (including categorical semantics) of the language, and eventually the formalization of some of this meta-theory in a proof assistant. Familiarity with type theory (especially dependent type theory), programming language design, and/or semantics will be a prerequisite for this postdoc. Familiarity with quantum computing will be helpful, but is neither necessary nor sufficient for this position - the main emphasis is on programming languages and type systems. Although the position will be held at Dalhousie University in Canada, it will be an asset if the candidate is able to travel, because I will be spending one semester in Germany and one semester in the U.S. next year, and ideally I would like the postdoc to be able to accompany me. Funding for the project comes from the U.S. Air Force Office of Scientific Research, and the research project will be part of a team effort also involving collaborators from Tulane, Stanford, Oxford, the University of Iowa, and the University of Pennsylvania. The nominal start date for the project is September 30, 2015 (yes, this is today!), so the start date can be immediately, or some time in the near future. The position is initially for 1 year, and can be extended for an additional year. The salary is CAD $60,000 per year. Interested applicants should contact Peter Selinger at selinger(a)mathstat.dal.ca as soon as possible, and in any case before October 21. I can provide more details about the research project to interested applicants on request. Thanks, -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

FSCD'16 Final Call for Papers
by hassei＠kurims.kyoto-u.ac.jp 22 Jan '16

22 Jan '16

FINAL CALL FOR PAPERS First International Conference on Formal Structures for Computation and Deduction (FSCD'16) 22 June -- 26 June 2016, Porto, Portugal http://fscd2016.dcc.fc.up.pt/ *** ABSTRACT SUBMISSION DUE 29 JANUARY 2016 *** **** PAPER SUBMISSION DUE 5 FEBRUARY 2016 **** ========================================================================== IMPORTANT DATES Abstract Submission: 29 January 2016 Paper Submission : 5 February 2016 Rebuttal : 21 - 23 March 2016 Notification : 6 April 2016 ========================================================================== FSCD (http://fscdconference.org/) covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing and homotopy type theory. The name of the new conference comes from an unpublished but important book by Gerard Huet that strongly influenced many researchers in the area. Suggested, but not exclusive, list of topics for submission are: 1 Calculi * Lambda calculus * Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.) * Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.) * Proof theory (natural deduction, sequent calculus, proof nets, etc.) * Type theory and logical frameworks * Homotopy type theory 2. Methods in Computation and Deduction * Type systems (polymorphism, dependent, recursive, intersection, session, etc.) * Induction, coinduction * Matching, unification, completion, orderings * Strategies (normalization, completeness, etc.) * Tree automata * Model building and model checking * Proof search (resolution, paramodulation, narrowing, focusing, etc.) * Constraint solving and decision procedures 3. Semantics * Operational semantics and abstract machines * Game Semantics and applications * Domain theory and categorical models * Quantitative models (timing, probabilities, resources, etc.) * Quantum computation and emerging models in computation 4. Algorithmic Analysis and Transformations of Formal Systems * Type Inference and type checking * Abstract Interpretation * Complexity analysis and implicit computational complexity * Checking termination, confluence, derivational complexity and related properties * Symbolic computation 5. Tools and Applications * Programming and proof environments (proof assistants, automated theorem prover, proof checkers, specialized provers, dependently typed languages, etc.) * Verification tools (abstract interpretation, termination, confluence, specialized provers, etc.) * Libraries for proof assistants and interactive theorem provers (support for variable bindings, nominal, polynomial, equality, etc.) * Case studies in proof assistants and interactive theorem provers (formalizations, mechanizations, certifications) * Certifications (theorems, rewriting techniques, etc.) * Applications of formal systems inside and outside of CS (biology, linguistics, physics, education, etc.) INVITED SPEAKERS Amal Ahmed (USA) Ichiro Hasuo (Japan) Gerard Huet (France) Tobias Nipkow (Germany) PROGRAM CHAIRS Delia Kesner (Univ. Paris-Diderot) Brigitte Pientka (McGill University) fscd16(a)easychair.org PROGRAM COMMITTEE Andreas Abel (Gothenburg Univ.) Zena Ariola (Univ. Oregon) Patrick Baillot (CNRS & ENS Lyon) Andrej Bauer (Univ. Ljubljana) Eduardo Bonelli (Univ. Quilmes) Patricia Bouyer (ENS Cachan) Ugo Dal Lago (Univ. Bologna) Nachum Dershowitz (Univ. Tel Aviv) Mariangiola Dezani-Ciancaglini (Univ. Torino) Derek Dreyer (MPI-SWS) Santiago Figueira (Univ. Buenos Aires) Marcelo Fiore (Univ. Cambridge) Juergen Giesl (Univ. Aachen) Nao Hirokawa (JAIST) Martin Hofmann (LMU Munchen) Delia Kesner (Univ. Paris-Diderot) Naoki Kobayashi (Univ. Tokyo) Dan Licata (Wesleyan Univ.) Chris Lynch (Clarkson Univ.) Narciso Marti-Oliet (Univ. Complutense) Aart Middeldorp (Univ. Innsbruck) Dale Miller (INRIA Saclay) Cesar Munoz (NASA) Vivek Nigam (Univ. Paraiba) Brigitte Pientka (McGill Univ.) Jakob Rehof (Univ. Dortmund) Xavier Rival (ENS Paris) Peter Selinger (Dalhousie Univ.) Paula Severi (Univ. Leicester) Jakob Grue Simonsen (Univ. Copenhagen) Matthieu Sozeau (INRIA Rocquencourt) Sophie Tison (Univ. Lille) Femke van Raamsdonk (VU Univ. Amsterdam) Nobuko Yoshida (Imperial College) CONFERENCE CHAIR Sandra Alves (University of Porto) FSCD STEERING COMMITTEE: Thorsten Altenkirch (Univ. Nottingham) Gilles Dowek (INRIA) Santiago Escobar (Univ. Politecnica de Valencia) Maribel Fernandez (King's College London) Masahito Hasegawa (Univ. Kyoto) Hugo Herbelin (INRIA) Nao Hirokawa (JAIST) Luke Ong (Chair, Univ. Oxford) Jens Palsberg (UCLA) Kristoffer Rose (Two Sigma Investments) Rene Thiemann (Univ. Innsbruck) Pawel Urzyczyn (Univ. Warsaw) Femke van Raamsdonk (VU Univ. Amsterdam) PUBLICATION The proceedings will be published as an electronic volume in the Leibniz International Proceedings in Informatics (LIPIcs). All LIPIcs proceedings are open access. SUBMISSION GUIDELINES Submissions can be made in two categories: regular research papers and system descriptions. Submissions of research papers must present original research which is unpublished and not submitted elsewhere. They must not exceed 15 pages (including figures and bibliography). Submissions of research papers will be judged on originality, significance, correctness, and readability. Submission of system descriptions must describe a working system which has not been published or submitted elsewhere. They must not exceed 10 pages and should contain a link to a working system. System descriptions will be judged on originality, significance, usefulness, and readability. Proofs of theoretical results that do not fit within the page limit, executables of systems, code of case studies, benchmarks used to evaluate a given system, should be made available, via a reference to a website or in an appendix of the paper. Reviewers will be encouraged to consider this additional material, but are not obliged to. Submissions must be self-contained within the respective page limit; considering the additional material should not be necessary to assess the merits of a submission. Submissions must be formatted using the LIPIcs style files using the instructions at http://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/ A condition of submission is that, if accepted, one of the authors must attend the conference to give the presentation. Papers should be submitted via easychair. The submission site is at https://easychair.org/conferences/?conf=fscd16 CONFERENCE AWARDS Two awards will be selected: one for the best paper and another one for the best student paper. SPECIAL ISSUE After the conference, authors of selected papers will be invited to submit extended versions of their work to a special issue published in the open-access journal Logical Methods in Computer Science (LMCS). SATELLITE EVENTS The following meetings and workshops are colocated with FSCD 2016: CL&C, DCM, HDRA, HOR, IFIP Working Group 1.6, ITRS, Linearity, LFMTP, LSFA, UNIF, WPTE, WWV. ORGANISING COMMITTEE Sandra Alves (Univ. Porto) Sabine Broda (Univ. Porto) Jose Espirito-Santo (Univ. do Minho) Mario Florido (Univ. Porto) Nelma Moreira (Univ. Porto) Luis Pinto (Univ. do Minho) Rogerio Reis (Univ. Porto) Ana Paula Tomas (Univ. Porto) Pedro Vasconcelos (Univ. Porto) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

PSSL99, aka Jirkafest, 2.1st announcement and correction
by Jürgen Koslowski 20 Jan '16

20 Jan '16

Dear colleagues, Unfortunately, yesterday's 2nd announcement exposed a discrepancy in the original WEB-site: - A conference fee of 20 Euros was mentioned twice in the main text, but the registration form said 25 Euros. The latter value was used in yesterday's announcement, but I've now reverted to 20 Euros everywhere. In case you have already transfered 25 Euros, you will be reimbursed accordingly. Sorry about that! Since we have sufficiently many talks for 3 sessions, and the idea of extending into Sunday afternoon may not be that popular (judging from previous PSSLs, people tend to be tired by noon on Sunday anyway), further proposed talks will need to go on a waiting list, in case there is a cancellation. (If you did not submit a title already, please do so in the near future.) Moreover, yesterday I managed to edit an old version of the html-file rather than the current one on my notebook: - invited speaker Lars Birkedal and the other participants have been re-instated; - the price of 50 Euros for Saturday's dinner INCLUDES drinks. Sincerely yours, -- J??rgen Koslowski -- Juergen Koslowski If I don't see you no more on this world ITI, TU Braunschweig I'll meet you on the next one koslowj(a)iti.cs.tu-bs.de and don't be late! http://www.iti.cs.tu-bs.de/~koslowj Jimi Hendrix (Voodoo Child, SR) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Formalizing topos-theoretic arguments in Lean
by Todd Wilson 19 Jan '16

19 Jan '16

For those interested in formalizing internal topos-theoretic arguments in a proof assistant, I'd like to make a plug for a newer entry on the usual list of provers, namely the Lean Theorem Prover [1]. In Lean, Prop is impredicative and extensional, and so it functions much like a subobject classifier, allowing a direct encoding of topos-theoretic arguments. As an example, you can look at my formalization [2] of the results from my paper J. Todd Wilson, "An Intuitionistic version of Zermelo's proof that every choice set can be well-ordered", J. Symbolic Logic, 66:3 (2001), 1121-1126. Abstract: We give a proof, valid in any elementary topos, of the theorem of Zermelo that any set possessing a choice function for its set of inhabited subsets can be well-ordered. Our proof is considerably simpler than existing proofs in the literature and moreover can be seen as a direct generalization of Zermelo's own 1908 proof of his theorem. This "elementary" proof, besides being a direct generalization of Zermelo's, makes crucial use of both impredicativity and extensionality of the subobject classifier, and so is a good illustration of these features of Lean when it comes to doing such formalizations. (The "existing proofs in the literature" mentioned in the abstract referred to proofs of Freyd and Axel.) Also, if I can be permitted an additional self-plug, this proof does not appear to be well-known, since there is no reference to it in Section D4.5 of Johnstone's Elephant book or, for example, in the article on the well-ordering theorem in the nLab [3]. [1] https://leanprover.github.io/ [2] https://github.com/lambdacalculator/lean-choice [3] https://ncatlab.org/nlab/show/well-ordering+theorem -- Todd Wilson A smile is not an individual Computer Science Department product; it is a co-product. California State University, Fresno -- Thich Nhat Hanh [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

two categories of interest
by Paul B Levy 19 Jan '16

19 Jan '16

Dear all, Have either of the following categories been studied before? 1. A "set with loners" is a set A with a subset U, whose elements are called "loners". A "loner-respecting function" (A,U) --> (B,V) is a function A --> B such that for any x in U, f(x) is in V and its only f-preimage is x. Let SWL be the category of sets with loners and loner-respecting functions, and Inj the category of sets and injections. Both Set and Inj are isomorphic to full subcategories of SWL. 2. For sets A and B, a "sum preorder" from A to B is a preorder on A+B. Example: A is the set of men, B is the set of women, take the preorder "younger than or the same age as". An equivalence relation on A+B is called a "corelation" from A to B. Given sum preorders R : A --> B and S : B --> C, obtain the composite by taking the least preorder on A+B+C that contains R and S, and then restricting to A+C. Let SumPreord be the category of sets and sum preorders, Rel the category of sets and relations, and Corel the category of sets and corelations. Both Rel and Corel are isomorphic to lluf subcategories of SumPreord. Paul -- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1