Skip to main content

Showing 1–21 of 21 results for author: Mimram, S

Searching in archive math. Search in all archives.
.
  1. arXiv:2506.19402  [pdf, ps, other

    math.AT cs.LO

    Hypercubical manifolds in homotopy type theory

    Authors: Samuel Mimram, Émile Oleon

    Abstract: Homotopy type theory is a logical setting in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces up to homotopy, and proofs as homotopy invariant constructions. In this context, we introduce a type which corresponds to the hypercubical manifold, a space first introduced by Poincaré in 1895. Its importance stems from the fact that… ▽ More

    Submitted 24 June, 2025; originally announced June 2025.

  2. Polynomials in homotopy type theory as a Kleisli category

    Authors: Elies Harington, Samuel Mimram

    Abstract: Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of… ▽ More

    Submitted 7 December, 2024; v1 submitted 15 November, 2024; originally announced November 2024.

    Journal ref: Electronic Notes in Theoretical Informatics and Computer Science, Volume 4 - Proceedings of MFPS XL (December 11, 2024) entics:14786

  3. arXiv:2405.10149  [pdf, other

    cs.LO math.AT

    Delooping cyclic groups with lens spaces in homotopy type theory

    Authors: Samuel Mimram, Émile Oleon

    Abstract: In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precis… ▽ More

    Submitted 16 May, 2024; originally announced May 2024.

  4. arXiv:2405.03264  [pdf, ps, other

    cs.LO math.CT

    Delooping presented groups in homotopy type theory

    Authors: Camil Champin, Samuel Mimram, Emile Oleon

    Abstract: Homotopy type theory is a logical setting based on Martin-Löf type theory in which one can perform geometric constructions and proofs in a synthetic way. Namely, types can be interpreted as spaces up to homotopy and proofs as homotopy invariant constructions. In this context, loop spaces of pointed connected groupoids provide a natural representation of groups, and any group can be obtained as the… ▽ More

    Submitted 1 July, 2025; v1 submitted 6 May, 2024; originally announced May 2024.

  5. arXiv:2402.18170  [pdf, ps, other

    math.CT

    Rewriting techniques for relative coherence

    Authors: Samuel Mimram

    Abstract: A series of works has established rewriting as an essential tool in order to prove coherence properties of algebraic structures, such as MacLane's coherence theorem for monoidal categories, based on the observation that, under reasonable assumptions, confluence diagrams for critical pairs provide the required coherence axioms. We are interested here in extending this approach simultaneously in two… ▽ More

    Submitted 18 June, 2025; v1 submitted 28 February, 2024; originally announced February 2024.

    MSC Class: 18N20 ACM Class: F.4.2

  6. arXiv:2312.00429  [pdf, other

    math.CT cs.LO

    Polygraphs: From Rewriting to Higher Categories

    Authors: Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, Samuel Mimram

    Abstract: Polygraphs are a higher-dimensional generalization of the notion of directed graph. Based on those as unifying concept, this monograph on polygraphs revisits the theory of rewriting in the context of strict higher categories, adopting the abstract point of view offered by homotopical algebra. The first half explores the theory of polygraphs in low dimensions and its applications to the computation… ▽ More

    Submitted 1 December, 2023; originally announced December 2023.

    MSC Class: 18N30 (Primary) 18-00; 18C10; 18N40; 68Q42 (Secondary) ACM Class: F.4.2; A.1

  7. arXiv:2211.16099  [pdf, ps, other

    math.CT

    Free precategories as presheaf categories

    Authors: Simon Forest, Samuel Mimram

    Abstract: Precategories generalize both the notions of strict $n$-category and sesquicategory: their definition is essentially the same as the one of strict $n$-categories, excepting that we do not require the various interchange laws to hold. Those have been proposed as a framework in which one can express semi-strict definitions of weak higher categories: in dimension 3, Gray categories are an instance of… ▽ More

    Submitted 29 November, 2022; originally announced November 2022.

    Comments: 34 pages

    MSC Class: 18N99

  8. arXiv:2109.05369  [pdf, ps, other

    math.CT

    Rewriting in Gray categories with applications to coherence

    Authors: Simon Forest, Samuel Mimram

    Abstract: Over the recent years, the theory of rewriting has been used and extended in order to provide systematic techniques to show coherence results for strict higher categories. Here, we investigate a further generalization to Gray categories, which are known to be equivalent to tricategories. This requires us to develop the theory of rewriting in the setting of precategories, which include Gray categor… ▽ More

    Submitted 29 November, 2022; v1 submitted 11 September, 2021; originally announced September 2021.

  9. arXiv:2106.04475  [pdf, ps, other

    cs.LO math.CT

    Globular weak $ω$-categories as models of a type theory

    Authors: Thibaut Benjamin, Eric Finster, Samuel Mimram

    Abstract: We study the dependent type theory CaTT, introduced by Finster and Mimram, which presents the theory of weak $ω$-categories, following the idea that type theories can be considered as presentations of generalized algebraic theories. Our main contribution is a formal proof that the models of this type theory correspond precisely to weak $ω$-categories, as defined by Maltsiniotis, by generalizing a… ▽ More

    Submitted 2 February, 2024; v1 submitted 8 June, 2021; originally announced June 2021.

  10. arXiv:2101.03591  [pdf, ps, other

    cs.LO math.AT

    Tietze Equivalences as Weak Equivalences

    Authors: Simon Henry, Samuel Mimram

    Abstract: A given monoid usually admits many presentations by generators and relations and the notion of Tietze equivalence characterizes when two presentations describe the same monoid: it is the case when one can transform one presentation into the other using the two families of so-called Tietze transformations. The goal of this article is to provide an abstract and geometrical understanding of this well… ▽ More

    Submitted 14 October, 2021; v1 submitted 10 January, 2021; originally announced January 2021.

  11. arXiv:1908.06684  [pdf, other

    cs.LO cs.DC math.AT

    Directed Homotopy in Non-Positively Curved Spaces

    Authors: Eric Goubault, Samuel Mimram

    Abstract: A semantics of concurrent programs can be given using precubical sets, in order to study (higher) commutations between the actions, thus encoding the "geometry" of the space of possible executions of the program. Here, we study the particular case of programs using only mutexes, which are the most widely used synchronization primitive. We show that in this case, the resulting programs have non-pos… ▽ More

    Submitted 10 July, 2020; v1 submitted 19 August, 2019; originally announced August 2019.

    MSC Class: 55M99; 68Q10 ACM Class: G.0; F.3.2

    Journal ref: Logical Methods in Computer Science, Volume 16, Issue 3 (July 13, 2020) lmcs:5731

  12. arXiv:1903.05848  [pdf

    math.CT

    Syntactic approaches to opetopes

    Authors: Pierre-Louis Curien, Cédric Ho Thanh, Samuel Mimram

    Abstract: Opetopes are algebraic descriptions of shapes corresponding to compositions in higher dimensions. As such, they offer an approach to higher-dimensional algebraic structures, and in particular, to the definition of weak $ω$-categories, which was the original motivation for their introduction by Baez and Dolan. They are classically defined inductively (as free operads in Leinster's approach, or as z… ▽ More

    Submitted 14 March, 2019; originally announced March 2019.

    Comments: 76 pages

    MSC Class: Primary 18D50; Secondary 03B15

  13. arXiv:1706.02866  [pdf, ps, other

    cs.LO math.CT

    A Type-Theoretical Definition of Weak ω-Categories

    Authors: Eric Finster, Samuel Mimram

    Abstract: We introduce a dependent type theory whose models are weak ω-categories, generalizing Brunerie's definition of ω-groupoids. Our type theory is based on the definition of ω-categories given by Maltsiniotis, himself inspired by Grothendieck's approach to the definition of ω-groupoids. In this setup, ω-categories are defined as presheaves preserving globular colimits over a certain category, called a… ▽ More

    Submitted 9 June, 2017; originally announced June 2017.

    ACM Class: F.4.1

  14. Coherent Presentations of Monoidal Categories

    Authors: Pierre-Louis Curien, Samuel Mimram

    Abstract: Presentations of categories are a well-known algebraic tool to provide descriptions of categories by means of generators, for objects and morphisms, and relations on morphisms. We generalize here this notion, in order to consider situations where the objects are considered modulo an equivalence relation, which is described by equational generators. When those form a convergent (abstract) rewriting… ▽ More

    Submitted 25 September, 2017; v1 submitted 9 May, 2017; originally announced May 2017.

    MSC Class: 68Q42 ACM Class: F.4.2

    Journal ref: Logical Methods in Computer Science, Volume 13, Issue 3 (September 26, 2017) lmcs:3955

  15. A Categorical Theory of Patches

    Authors: Samuel Mimram, Cinzia Di Giusto

    Abstract: When working with distant collaborators on the same documents, one often uses a version control system, which is a program tracking the history of files and helping importing modifications brought by others as patches. The implementation of such a system requires to handle lots of situations depending on the operations performed by users on files, and it is thus difficult to ensure that all the co… ▽ More

    Submitted 13 November, 2013; originally announced November 2013.

    Journal ref: MFPS - Mathematical Foundations of Programming Semantics 298 (2013) 283-307

  16. arXiv:1306.2305  [pdf, other

    math.OC eess.SY math.NA

    Computing Flowpipe of Nonlinear Hybrid Systems with Numerical Methods

    Authors: Olivier Bouissou, Alexandre Chapoutot, Samuel Mimram

    Abstract: Modern control-command systems often include controllers that perform nonlinear computations to control a physical system, which can typically be described by an hybrid automaton containing high-dimensional systems of nonlinear differential equations. To prove safety of such systems, one must compute all the reachable sets from a given initial position, which might be uncertain (its value is not p… ▽ More

    Submitted 10 June, 2013; originally announced June 2013.

  17. A Non-Standard Semantics for Kahn Networks in Continuous Time

    Authors: Romain Beauxis, Samuel Mimram

    Abstract: In a seminal article, Kahn has introduced the notion of process network and given a semantics for those using Scott domains whose elements are (possibly infinite) sequences of values. This model has since then become a standard tool for studying distributed asynchronous computations. From the beginning, process networks have been drawn as particular graphs, but this syntax is never formalized. We… ▽ More

    Submitted 25 August, 2011; originally announced August 2011.

    Comments: 2010

    Journal ref: Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL 12 (2011) 35-50

  18. arXiv:1101.4813  [pdf, ps, other

    cs.LO cs.GT math.CT

    The Structure of First-Order Causality (extended version)

    Authors: Samuel Mimram

    Abstract: Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that i… ▽ More

    Submitted 25 January, 2011; originally announced January 2011.

    Journal ref: Mathematical Structures in Computer Science 21, 01 (2011) 65-110

  19. arXiv:1004.3135  [pdf, ps, other

    cs.FL math.CT

    Computing Critical Pairs in 2-Dimensional Rewriting Systems

    Authors: Samuel Mimram

    Abstract: Rewriting systems on words are very useful in the study of monoids. In good cases, they give finite presentations of the monoids, allowing their manipulation by a computer. Even better, when the presentation is confluent and terminating, they provide one with a notion of canonical representative for the elements of the presented monoid. Polygraphs are a higher-dimensional generalization of this no… ▽ More

    Submitted 19 April, 2010; originally announced April 2010.

  20. arXiv:0908.3994  [pdf, ps, other

    cs.LO math.CT math.LO

    The Structure of First-Order Causality

    Authors: Samuel Mimram

    Abstract: Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that… ▽ More

    Submitted 27 August, 2009; originally announced August 2009.

    Journal ref: Logic in Computer Science, Los Angeles : United States (2009)

  21. arXiv:0805.0845  [pdf, ps, other

    cs.LO math.CT math.LO

    Presentation of a Game Semantics for First-Order Propositional Logic

    Authors: Samuel Mimram

    Abstract: Game semantics aim at describing the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. In this article, we introduce a game semantics for a fragment of first order propositional logic. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strate… ▽ More

    Submitted 7 May, 2008; originally announced May 2008.