most recent 30 from http://mathoverflow.net 2013-06-19T09:34:21Z http://mathoverflow.net/feeds/question/89307 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/89307/higher-categories-in-logic Giorgio Mossa 2012-02-23T17:46:13Z 2012-02-24T11:47:07Z

<p>I've read somewhere (probably in the nlab) that higher category theory has application in logic. By the way since now the only applications of higher category theory I've seen are in homotopy theory and mathematical physics, so I was wondering if anyone could give me some example of applications of higher categorical methods in logic (any reference would be appreciated).</p>

http://mathoverflow.net/questions/89307/higher-categories-in-logic/89312#89312 Ed Dean 2012-02-23T18:18:58Z 2012-02-23T18:18:58Z

<p>You would probably enjoy checking out <a href="http://homotopytypetheory.org/" rel="nofollow">homotopy type theory</a> and Vladimir Voevodsky's corresponding program of <em>univalent foundations</em> for mathematics. Steve Awodey's survey article (linked to from that site) is a good starting point, and includes a spelling-out of a homotopical interpretation of Martin-Lof type theory.</p>

http://mathoverflow.net/questions/89307/higher-categories-in-logic/89338#89338 Peter Arndt 2012-02-23T22:05:25Z 2012-02-23T22:05:25Z

<p>Another group of related applications are those in rewriting theory, concurrency theory, directed homotopy theory etc. For this check out the pages of <a href="http://iml.univ-mrs.fr/~lafont/recherche.html" rel="nofollow">Yves Lafont</a> and his collaborators.</p>

http://mathoverflow.net/questions/89307/higher-categories-in-logic/89341#89341 Miroslav Korbelar 2012-02-23T22:32:54Z 2012-02-23T22:32:54Z

<p>There should be a lot of stuff concerning this in papers and books of Michael Makkai.</p>

http://mathoverflow.net/questions/89307/higher-categories-in-logic/89384#89384 Vladimir Dotsenko 2012-02-24T11:47:07Z 2012-02-24T11:47:07Z

<p>To elaborate on Peter Arndt's answer a bit: indeed, considering terms as 1-cells and rewriting rules as 2-cells, you can indeed obtain a rather productive higher categorical view on various constructions of rewriting theory. Morally, this would mean that cofibrant replacements in various model categories (of modules, or associative algebras) can be described in a rather pleasant geometric way, - computing syzygies becomes building higher-dimensional cells of a cell complex from the low-dimensional ones. There are several good references to master this kind of viewpoint, best processed when viewed together. Those are the paper of Craig Squier "Word problems and a homological finiteness condition for monoids" from which all sort of started, when it comes to theoretical computer science, at least (this paper re-discovered in a somewhat different context results from a paper of David Anick "On the homology of associative algebras"), the paper of Jean-Louis Loday "Homotopical syzygies", and indeed, recent papers of the French computer science school, such as Yves Lafont, Francois Metayer, Yves Guiraud, Philippe Malbos and many others.</p>