From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7211 Path: news.gmane.org!not-for-mail From: Steve Awodey Newsgroups: gmane.science.mathematics.categories Subject: Call for papers: special issue of MSCS Date: Tue, 21 Feb 2012 10:23:12 -0500 Message-ID: Reply-To: Steve Awodey NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1329918605 21691 80.91.229.3 (22 Feb 2012 13:50:05 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 22 Feb 2012 13:50:05 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Wed Feb 22 14:50:01 2012 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.4]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1S0CZy-00049V-Ie for gsmc-categories@m.gmane.org; Wed, 22 Feb 2012 14:49:58 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:42697) by smtpx.mta.ca with esmtp (Exim 4.77) (envelope-from ) id 1S0CYd-0001bH-8e; Wed, 22 Feb 2012 09:48:35 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1S0CYc-0003Sy-Hq for categories-list@mlist.mta.ca; Wed, 22 Feb 2012 09:48:34 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7211 Archived-At: *********************** Call for papers = *************************************** * Mathematical Structures in Computer Science - Special issue * "=46rom Type Theory and Homotopy Theory to Univalent Foundations" * Deadline for submissions: December 31st, 2012 BACKGROUND Over the last few years, there has been significant progress in relating type theory with homotopy theory and higher-dimensional category theory. These advances have stimulated a new wave of research in type theory, in which ideas of mathematical logic and theoretical computer science are often combined with geometric intuition in an original way. In particular, the Univalent Foundations programme formulated by = Vladimir Voevodsky seeks to develop a new approach to the foundations of mathematics on the basis of type theories that combine the good computational properties of Martin-L=F6f type theories and the Calculus = of Inductive Constructions with new axioms inspired by homotopy theory, = such as the Univalence Axiom. AIMS AND SCOPE The aim of the special issue is to provide a comprehensive and timely account of the state of the art in this new area of research, thus providing a basis for future developments. We welcome submissions from participants in the several conferences and workshops on these topics that are occurring this year or have occurred = in the past few years. Topics of interest include, but are not limited, to: - homotopical semantics of type theories - semantics of type theories in higher categories - syntactic and semantic aspects of identity types - syntactic and semantic aspects of the Univalence Axiom - development of Univalent Foundations - related issues and challenges in computer-assisted proof-checking - representation of homotopical and higher categorical structures in = type theory - related applications of polynomial/container functors. SUBMISSION The deadline for submissions is December 31st, 2012. Papers should be submitted as pdf attachments with an email to one of = the editors. EDITORS The special issue will be edited by Steve Awodey (Carnegie Mellon University) Nicola Gambino (University of Palermo) Erik Palmgren (University of Stockholm) With best wishes, Steve= [For admin and other information see: http://www.mta.ca/~cat-dist/ ]