Directed Homotopy in Non-Positively Curved Spaces

Eric Goubault; Samuel Mimram

REVIEW 3 major objections 4 minor 57 references

Directed Homotopy in Non-Positively Curved Spaces

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read For mutex-only programs, homotopy and directed homotopy coincide.

desk verdict This is the real bridge between directed algebraic topology and CAT(0) geometry; the main theorem is well-motivated and likely correct, but the rewriting proof has a genuine gap that should be fixed or formalized. read the letter →

arxiv 1908.06684 v4 pith:SROSH2HS submitted 2019-08-19 cs.LO cs.DCmath.AT

Eric Goubault , Samuel Mimram This is my paper · ORCID

classification cs.LOcs.DCmath.AT MSC 68Q8518D0555U10

keywords precubicalsetsdirectedhomotopydihomotopynon-positivecurvatureCAT(0)spacesconcurrentprogramsmutexsynchronizationcubeproperty

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper studies the spaces of possible executions of concurrent programs that synchronize only with mutexes, the lock primitive that at most one thread can hold at a time. It introduces a combinatorial notion of non-positive curvature for precubical sets, the shapes used to model these execution spaces, and proves that the semantics of every mutex-only program satisfies it. The central result is that in such a space two directed paths are homotopic in the ordinary, undirected sense exactly when they are dihomotopic, meaning one can be deformed into the other while keeping time directed. This says that the fundamental groupoid of an execution space already carries all the information in its fundamental category, so standard algebraic topology can be used to analyse execution traces of mutex-only programs. The same curvature condition is then shown to match the classical CAT(0) condition after geometric realization, connecting program semantics to non-positive curvature geometry.

What carries the argument

The load-bearing mechanism is the cube property, the requirement that whenever a precubical set contains one half of the boundary of a 3-cube it also contains the other half; together with geometricity and unique filling of higher cube boundaries, it defines non-positive curvature for precubical sets. To compare homotopy with dihomotopy, the paper constructs the fundamental 2-category $\vec{\Pi}_2(C)$ and fundamental 2-groupoid $\Pi_2(C)$ of a precubical set, whose 2-cells are formal homotopies generated by square swaps $\gamma_{a,b}^{b',a'}$, by units $\eta_a$ (inserting $a\cdot\bar a$), and by counits $\varepsilon_a$ (cancelling $\bar a\cdot a$). A rewriting system over these 2-cells, with the exchange law and the cube property ensuring that every rewrite stays well-defined, brings every formal 2-cell between two dipaths to a canonical form built only from square swaps; that canonical form is exactly a dihomotopy. In the geometric part, the link of each vertex, with its flagness condition, is the discrete counterpart of the classical link condition characterizing non-positive curvature.

What would settle it

Run an exhaustive computer search over small non-positively curved precubical sets for a pair of homotopic directed paths whose homotopy, written as a formal 2-cell, cannot be rewritten to square-swap form; finding such a pair would refute Theorem 2.29, while checking all finite index cases of the deferred rewriting lemmas would confirm the missing subcases.

Watch

Extended reading notes

Core claim

Let $C$ be a non-positively curved precubical set: geometric, satisfying the cube property, and filling $n$-cube boundaries uniquely for $n\ge 3$. Theorem 2.29 of the paper asserts that two dipaths in $C$ are homotopic if and only if they are dihomotopic, and Theorem 2.30 restates this as the fullness and faithfulness of the quotient functor from the fundamental category $\vec{\Pi}_1(C)$ to the fundamental groupoid $\Pi_1(C)$. Since Proposition 1.29 shows that the precubical semantics of a mutex-only program is such a set, directed paths in the execution space are classified by ordinary homotopy: the orientation of time is immaterial at the level of homotopy classes. The paper also establishes that this discrete notion of non-positive curvature is the algebraic shadow of the standard geometric one: the geometric realization of an npc precubical set is a CAT(0) cubical complex.

Load-bearing premise

The main proof relies on the normalization claim that every formal homotopy written in the fundamental 2-groupoid can be rewritten into a canonical form, and the written proof defers several subcases to 'similar case analysis' or to figures; if any of those deferred cases fails, the reduction of homotopy to dihomotopy is unsupported.

Editorial extensions

If this is right

For any mutex-only program, the fundamental category of its execution space embeds fully faithfully into the fundamental groupoid, so homotopy classes of directed paths are faithfully reflected by ordinary homotopy classes.
Ordinary topological invariants, such as components, fundamental group, and homology, can be used to study the execution traces of these programs without building separate directed invariants.
After directed geometric realization, dipaths between realizations of vertices in an npc precubical set are homotopic exactly when they are dihomotopic, transferring the theorem from combinatorics to metric spaces.
Geometric realizations of mutex-only program semantics are CAT(0) cubical complexes, hence locally uniquely geodesic with contractible universal covers.
The cube property is equivalent to a local flagness condition on links, so the curvature of an execution space can be checked vertex by vertex.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

One natural next step the paper does not take is to prove the same collapse one dimension higher, so that the fundamental 2-category embeds into the fundamental 2-groupoid; the canonical-form rewriting suggests this could hold, but that is an inference, not a theorem proved here.
Since curvature is local, deciding whether two dipaths are dihomotopic in these program spaces could be reduced to an ordinary homotopy problem on the 2-skeleton, a more tractable algorithmic formulation than searching the full path space.
The generalized-metric realization encodes duration as well as direction, so if the curvature argument carries over, timed concurrent models might inherit the same collapse of directed to ordinary homotopy, an extension the paper leaves open.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Two things you should know. First, the main result — for mutex-only programs, directed and ordinary homotopy coincide on execution dipaths — is genuinely new and, if correct, it changes how we think about concurrency semantics: it says the execution space is non-positively curved in a precise algebraic sense, so classical invariants apply. Second, the proof of that result relies on a normalization argument that is not fully written out. Proposition 2.24 ends with "similar case analysis" and Lemma 2.25(4)-(5) says the commutations "can easily be guessed from the figures." Those are exactly the steps that push H and E generators to the right place so Lemma 2.28 can eliminate them. If any of those cases fails for some context, the reduction of homotopy to dihomotopy is unsupported. I don't think it fails — the geometry, the cube property, and the compact-closed-category sanity check all point the same way — but a serious reader cannot verify the central claim from the printed proof alone.

What is actually new: the paper introduces npc precubical sets, proves that mutex semantics are npc, and proves that geometric realization turns npc precubical sets into CAT(0) cubical complexes. That gives a clean triangle: programs, combinatorics, metric geometry. The paper is unusually honest about its debts — it cites Winskel, Chepoi, Gromov, and others carefully, and uses them as benchmarks rather than fitting definitions to force the conclusion. The 2-categorical rewriting setup is elegant.

The soft spots are contained and real. Theorem 1.42 (link characterization) is proved in full. The gap is localized to the normalization and exchange lemmas. Proposition 2.24 explicitly defers many cases; Lemma 2.25(4)-(5) has no derivation at all. This is load-bearing, so "conditional" is the right verdict. It is a proof gap, not a statement gap.

Who should read this: anyone working on directed algebraic topology, concurrency semantics, or CAT(0) cube complexes. It deserves serious referee time. I would ask the authors for an expanded proof, ideally a machine-checked version of the rewriting lemmas, before I rely on the theorem. The paper is significant and the gap looks fixable.

Referee Report

3 major / 4 minor

Summary. The paper introduces non-positively curved (npc) precubical sets as an algebraic analogue of CAT(0) cubical complexes, proves that the precubical semantics of mutex-only concurrent programs is npc (Prop 1.29), gives a link-condition characterization (Thm 1.42), and establishes the main result (Thm 2.29/2.30): for npc precubical sets, two dipaths are homotopic if and only if they are dihomotopic, so the fundamental category and fundamental groupoid determine each other for directed paths. The proof strategy is a 2-categorical rewriting system on formal 2-cells, with a canonical form (Prop 2.24) and commutation rules (Lemma 2.25) used to eliminate the η and ε generators. The paper then develops generalized metric spaces and geometric realization, showing that the npc axioms correspond to Gromov's flag condition (Thm 3.79), so that realizations are CAT(0) cubical complexes.

Significance. If the main theorem is established, it is an important bridge: ordinary (undirected) homotopy theory becomes applicable to the directed execution spaces of mutex programs, and the connection to CAT(0) geometry links concurrency semantics to a mature body of geometric group theory. The paper's architectural strengths are its external benchmarks: the npc condition is checked against Gromov's CAT(0) link condition (Thm 3.79), the 2-categorical axioms are related to compact closed categories (Prop 2.33), and the mutex semantics independently yields the cube property (Prop 1.29). The treatment of generalized metric spaces and the identification of directed realizations as CAT(0) cubical complexes is also valuable. However, the proof of the central normalization theorem is not complete as written: two load-bearing steps are deferred to 'similar case analysis' or to figures.

major comments (3)

[§2.2.2, Proposition 2.24] Proposition 2.24 is the normalization lemma on which the proof of Theorem 2.29 rests, but its proof is incomplete. The induction treats only four subcases for α = ε with ψ = G...; it defers 'The cases where ψ = H... and ψ = E... can be handled similarly by case analysis' and 'The case where α = γ can be handled similarly by case analysis.' Since the canonical form can be an arbitrary nested expression in the operators G, H, E, and the slice α can be η, ε, or γ in arbitrary context, these omitted combinations are exactly the ones that require the delicate commutations of Lemma 2.25. Without a complete case analysis, the assertion that every formal 2-cell rewrites to a canonical form is not established.
[§2.2.2, Lemma 2.25] Items (4) and (5) of Lemma 2.25 are asserted with 'can easily be guessed from the figures' and no derivation is supplied. These are the only stated rules for commuting G past H in the nested cases involving two G/H contexts, and Lemma 2.28 uses them to bring an H to the left and to place an E in front of an H-free expression. A missing index or context case would break the elimination of η and ε. The proof should either give complete equational derivations for (4) and (5), or formulate a general commutation lemma with all indices specified.
[§2.2.2, Lemma 2.28] The argument in Lemma 2.28 that a canonical form containing H or E can be rearranged 'up to more rewriting' needs to ensure that each application of Lemma 2.25 preserves the property of being a canonical form and does not reintroduce an operator already eliminated. The text asserts this without proof, and the properties in Lemma 2.27 are stated for canonical forms, not for arbitrary rewrites. A precise induction on the structure of the canonical form is needed.

minor comments (4)

[Definition 1.37] The flag condition for presimplicial sets is stated for 'every integer n > 3', but the proof of Theorem 1.42 applies it with n = 2 in the cube-property direction and with arbitrary n afterwards; the condition should presumably read n > 2 (or n ≥ 3). Please correct the statement and check that it agrees with the standard usage in Definition 3.78.
[Section 2.3] The section begins 'We omit proofs, they should be detailed in subsequent works'; this explicitly leaves Proposition 2.33 and the convergence conjectures unproved. Since they are not used in the proof of Theorem 2.29 this is acceptable for an extensions section, but the paper should mark them clearly as conjectures or unproved claims rather than presenting them as established results.
[Remark 1.26] There is a typo: 'there are height in total' should read 'there are eight in total.'
[§2.2.1, equations (2.13)–(2.15)] Some displayed equations, in particular (2.14) and the surrounding lines, have malformed or missing indices on the γ generators; please proofread and restore the full indices.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main theorem is proved by explicit rewriting from npc lifting conditions, and the proof gaps are correctness risks, not circular inputs.

full rationale

The main derivation is self-contained against external benchmarks. Proposition 1.29 establishes that mutex semantics is non-positively curved by an explicit induction and resource-potential case analysis, not by assuming the desired homotopy/dihomotopy coincidence. Theorem 2.29 is then obtained by a 2-categorical rewriting argument: Lemma 2.20 decomposes formal 2-cells into slices, Proposition 2.24 rewrites them to canonical forms, Lemma 2.28 eliminates the η and ε generators using the direction analysis of Lemma 2.27, and the conclusion follows from the canonical functor of Remark 2.17. None of these steps is an equation that defines the conclusion into the hypotheses; the npc conditions are geometric lifting properties, independent of path equivalence. The paper also checks its categorical axioms against an external benchmark in Proposition 2.33, identifying the one-loop example with the free compact closed category on a unidimensional object via Kelly–Laplaza and Preller–Lambek, and Section 3 verifies the algebraic npc notion against Gromov's CAT(0)/link condition in Theorem 3.79, with the classical equivalences attributed to [26] and [6]. Self-citations such as [22], [41], [42], and [15] provide background and proof techniques, but the load-bearing claims are proved in the paper itself. There are genuine proof gaps: Proposition 2.24 defers cases with 'can be handled similarly by case analysis,' and Lemma 2.25 items (4) and (5) are asserted with 'can easily be guessed from the figures'; these are correctness risks that could affect Lemma 2.28, but they are not circularity because they do not reduce the theorem to its own statement or to fitted inputs.

Assumptions & free parameters 0 free parameters · 7 assumptions · 2 invented entities

No free parameters are fitted. The central claim rests on standard categorical and geometric background, on the domain modeling assumptions for mutex programs, and on two new definitions (npc precubical sets and the fundamental 2-groupoid) that the paper itself introduces. The npc notion is independently anchored by Theorem 3.79 to CAT(0) geometry.

assumptions (7)

standard math The category of precubical sets is a presheaf category and is cocomplete; this underlies colimit-based definitions and the geometric realization as a left Kan extension.
Used throughout Sections 1 and 3 for presheaf categories, Yoneda embedding, colimits, and Kan extensions (e.g., Def 1.1, Def 3.53).
standard math Gromov's link condition: a finite-dimensional cubical complex is non-positively curved (locally CAT(0)) iff the link of every vertex is a flag complex, and CAT(0) iff simply connected with flag links.
Invoked in the Proof of Theorem 3.79, Section 3.3.2, citing [26] and Bridson-Haefliger [6].
standard math Standard results on length spaces, geodesic spaces, and CAT(0) spaces from Bridson-Haefliger, including that length spaces are closed under colimits and finite-dimensional cubical complexes are geodesic.
Used in Sections 3.1.5 and 3.2.3 (Lemmas 3.52, 3.57, Prop 3.71).
domain assumption The operational semantics of mutex programs is correctly abstracted by the grammar and resource potential model: conservative programs, forbidden vertices, and removal of cubes containing them yield the true execution space.
Section 1.2, Definitions 1.10-1.16; this modeling is imported from the authors' book [15] and is not re-validated here.
domain assumption Programs without occurrences of the empty program 1 suffice for the semantics; this restriction ensures geometricity (Lemma 1.22).
Section 1.3.1, "We will implicitly assume that this is the case in the rest of the paper."
ad hoc to paper The new definition of npc precubical sets (geometric + cube property + unique n-cube property) is a sound algebraic analogue of non-positive curvature; this is what the geometric realization theorem (3.79) must justify.
Definition 1.28/1.46 introduces a new notion; the paper's own Theorem 3.79 provides the external justification via CAT(0) geometry.
ad hoc to paper The fundamental 2-groupoid Pi2(C) with the eleven relations (2.5)-(2.15) correctly represents path homotopy, and the cube property makes all left-hand sides of rewriting rules well-defined.
Definitions 2.10-2.13, Lemmas 2.14 and 2.19; this is a new axiomatization whose naturalness is argued via Prop 2.33.

invented entities (2)

Non-positively curved (npc) precubical set independent evidence
purpose: Algebraic condition on precubical sets under which directed and undirected homotopy coincide, and which mutex program semantics satisfy.
Introduced in Def 1.28/1.46. Independent evidence is Theorem 3.79, which identifies it with the established notion of CAT(0)/NPC cubical complexes via Gromov's link condition.
Fundamental 2-category and 2-groupoid of a precubical set (Pi2, Pi2) independent evidence
purpose: 2-categorical framework to rewrite homotopies into dihomotopies and to formalize higher tracks.
New in Section 2.2. Independent evidence is Prop 2.33 showing the one-edge example yields the free compact closed category on a unidimensional object, a known structure; the geometric realization conjecture is also stated as a falsifiable check.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Directed Homotopy in Non-Positively Curved Spaces." pith.science (2026). https://pith.science/paper/SROSH2HS

@misc{pith2026190806684,
  author       = {Pith},
  title        = {Pith review of: Directed Homotopy in Non-Positively Curved Spaces},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SROSH2HS}},
  note         = {Machine review of arXiv:1908.06684}
}

read the original 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-positive curvature, a notion that we introduce and study here for precubical sets, and can be thought of as an algebraic analogue of the well-known one for metric spaces. Using this it, as well as categorical rewriting techniques, we are then able to show that directed and non-directed homotopy coincide for directed paths in these precubical sets. Finally, we study the geometric realization of precubical sets in metric spaces, to show that our conditions on precubical sets actually coincide with those for metric spaces. Since the category of metric spaces is not cocomplete, we are lead to work with generalized metric spaces and study some of their properties.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

57 extracted references · 56 canonical work pages

[1]

G. E. Albert. A note on quasi-metric spaces.Bulletin of the American Mathematical Society, 47(6):479– 482, 1941

work page 1941
[2]

Ardila, M

F. Ardila, M. Owen, and S. Sullivant. Geodesics in CAT(0) cubical complexes.Advances in Applied Mathematics, 48(1):142–163, 2012

work page 2012
[3]

Barthélemy and J

J.-P. Barthélemy and J. Constantin. Median graphs, parallelism and posets.Discrete mathematics, 111(1):49–63, 1993

work page 1993
[4]

Betti, A

R. Betti, A. Carboni, R. Street, and R. Walters. Variation through enrichment.Journal of Pure and Applied Algebra, 29(2):109–127, 1983

work page 1983
[5]

Bezem, J

M. Bezem, J. Klop, R. de Vrijer, and Terese.Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003

work page 2003
[6]

M. R. Bridson and A. Haeﬂiger.Metric spaces of non-positive curvature, volume 319. Springer, 2009

work page 2009
[7]

V. Chepoi. Graphs of some CAT(0) complexes.Advances in Applied Mathematics, 24(2):125–179, 2000

work page 2000
[8]

V. Chepoi. Nice labeling problem for event structures: a counterexample.SIAM Journal on Computing, 41(4):715–727, 2012

work page 2012

Show all 57 references

[9]

Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015

F.ClercandS.Mimram.Presentingacategorymoduloarewritingsystem.In LIPIcs-Leibniz International Proceedings in Informatics, volume 36. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015

2015
[10]

Dehornoy

P. Dehornoy. On completeness of word reversing.Discrete Mathematics, 225(1):93–119, 2000

2000
[11]

Dehornoy, F

P. Dehornoy, F. Digne, E. Godelle, D. Krammer, and J. Michel. Foundations of garside theory.arXiv preprint arXiv:1309.0796, 2013

2013 arXiv
[12]

M. Droste. A kleene theorem for recognizable languages over concurrency monoids. InAutomata, Languages and Programming, pages 388–399. Springer, 1994

1994
[13]

Fahrenberg

U. Fahrenberg. Directed homology.Electr. Notes Theor. Comput. Sci., 100:111–125, 2004

2004
[14]

Fajstrup

L. Fajstrup. Dipaths and dihomotopies in a cubical complex.Advances in Applied Mathematics, 35(2):188– 206, 2005

2005
[15]

Fajstrup, É

L. Fajstrup, É. Goubault, E. Haucourt, S. Mimram, and M. Raussen.Directed Algebraic Topology and Concurrency. SpringerBriefs in Mathematical Methods. Springer International Publishing, 2016. Book to appear

2016
[16]

Ghrist and S

R. Ghrist and S. M. LaValle. Nonpositive curvature and pareto-optimal coordination of robots.SIAM Journal of Control and Optimization, 45(5):1697–1713, 2006

2006
[17]

Ghrist and V

R. Ghrist and V. Peterson. A Geometric Approach to Dipath Classiﬁcation on Process Graphs. Unpub- lished
[18]

Ghrist and V

R. Ghrist and V. Peterson. The geometry and topology of reconﬁguration.Advances in Applied Mathe- matics, 38(3):302 – 323, 2007

2007
[19]

É. Ghys, P. de La Harpe, et al.Sur les groupes hyperboliques d’apres Mikhael Gromov, volume 83. Birkhäuser Basel, 1990

1990
[20]

Gonthier, J.-J

G. Gonthier, J.-J. Lévy, and P.-A. Melliès. An abstract standardisation theorem. InLogic in Computer Science, 1992. LICS’92., Proceedings of the Seventh Annual IEEE Symposium on, pages 72–81. IEEE, 1992

1992
[21]

Goubault

E. Goubault. Geometry and concurrency: a user’s guide.Mathematical structures in computer science, 10(04):411–425, 2000

2000
[22]

Goubault and S

E. Goubault and S. Mimram. Formal relationships between geometrical and classical models for concur- rency.Electronic Notes in Theoretical Computer Science, 283:77–109, 2012

2012
[23]

Goubault-Larrecq.Non-Hausdorﬀ Topology and Domain Theory: Selected Topics in Point-Set Topology, volume 22

J. Goubault-Larrecq.Non-Hausdorﬀ Topology and Domain Theory: Selected Topics in Point-Set Topology, volume 22. Cambridge University Press, 2013

2013
[24]

M. Grandis. Directed algebraic topology: Models of non-reversible worlds.AMC, 10:12, 2009

2009
[25]

Grandis et al

M. Grandis et al. The fundamental weighted category of a weighted space: From directed to weighted algebraic topology.Homology, Homotopy and Applications, 9(1):221–256, 2007

2007
[26]

Gromov.Hyperbolic groups

M. Gromov.Hyperbolic groups. Springer, 1987

1987
[27]

Y. Guiraud. Termination orders for three-dimensional rewriting.Journal of Pure and Applied Algebra, 207(2):341–371, 2006

2006
[28]

Hardie, K

K. Hardie, K. Kamps, and R. Kieboom. A homotopy 2-groupoid of a hausdorﬀ space.Applied Categorical Structures, 8(1-2):209–234, 2000

2000
[29]

Hardie, K

K. Hardie, K. Kamps, and R. Kieboom. A homotopy bigroupoid of a topological space.Applied Categorical Structures, 9(3):311–327, 2001. Vol. 16:3 DIRECTED HOMOTOPY IN NON-POSITIVELY CUR VED SPACES 4:55

2001
[30]

Hopf and W

H. Hopf and W. Rinow. Über den begriﬀ der vollständigen diﬀerentialgeometrischen ﬂäche.Commentarii Mathematici Helvetici, 3(1):209–225, 1931

1931
[31]

P. T. Johnstone. On embedding categories in groupoids. InMathematical Proceedings of the Cambridge Philosophical Society, volume 145, pages 273–294. Cambridge University Press, 2008

2008
[32]

G. M. Kelly and M. L. Laplaza. Coherence for compact closed categories.Journal of Pure and Applied Algebra, 19:193–213, 1980

1980
[33]

J. Kelly. Bitopological spaces.Proceedings of the London Mathematical Society, 3(1):71–89, 1963

1963
[34]

Krishnan

S. Krishnan. Criteria for homotopic maps to be so along monotone homotopies.Electron. Notes Theor. Comput. Sci., 230:141–148, Mar. 2009

2009
[35]

D. Kuske. Nondeterministic automata with concurrency relations and domains. InTrees in Algebra and Programming—CAAP’94, pages 202–217. Springer, 1994

1994
[36]

Y. Lafont. Towards an algebraic theory of boolean circuits.Journal of Pure and Applied Algebra, 184(2):257–310, 2003

2003
[37]

F. W. Lawvere. Metric spaces, generalized logic, and closed categories. Rendiconti del seminario matématico e ﬁsico di Milano, 43(1):135–166, 1973

1973
[38]

Lévy.Réductions correctes et optimales dans le lambda-calcul

J.-J. Lévy.Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université Paris 7, 1978

1978
[39]

Mac Lane.Categories for the working mathematician, volume 5

S. Mac Lane.Categories for the working mathematician, volume 5. springer, 1998

1998
[40]

P.-A. Melliès. Axiomatic rewriting theory VI: Residual theory revisited. InRewriting techniques and applications, pages 24–50. Springer, 2002

2002
[41]

Mimram.Sémantique des jeux asynchrones et réécriture 2-dimensionnelle

S. Mimram.Sémantique des jeux asynchrones et réécriture 2-dimensionnelle. PhD thesis, PPS, CNRS – Université Paris Diderot, 2008

2008
[42]

Mathematical Structures in Computer Science, 21(01):65– 110, 2011

S.Mimram.Thestructureofﬁrst-ordercausality. Mathematical Structures in Computer Science, 21(01):65– 110, 2011

2011
[43]

S. Mimram. Towards 3-Dimensional Rewriting Theory.Logical Methods in Computer Science, 10(1):1–47, 2014

2014
[44]

Nielsen, G

M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part I.Theoretical Computer Science, 13(1):85–108, 1981

1981
[45]

Nielsen, V

M. Nielsen, V. Sassone, and G. Winskel.Relationships between models of concurrency. Springer, 1994

1994
[46]

Panangaden, V

P. Panangaden, V. Shanbhogue, and E. W. Stark.Stability and sequentiality in dataﬂow networks. Springer, 1990

1990
[47]

Preller and J

A. Preller and J. Lambek. Free compact 2-categories.Mathematical Structures in Computer Science, 17(02):309–340, 2007

2007
[48]

M. Roller. Poc sets, median algebras and group actions. An extended study of Dunwoody’s construction and Sageev’s theorem.Southampton Preprint Archive, 1998

1998
[49]

Rudin.Principles of mathematical analysis, volume 3

W. Rudin.Principles of mathematical analysis, volume 3. McGraw-Hill New York, 1964

1964
[50]

Sassone, M

V. Sassone, M. Nielsen, and G. Winskel. Deterministic behavioural models for concurrency. InMathe- matical Foundations of Computer Science 1993, pages 682–692. Springer, 1993

1993
[51]

Sassone, M

V. Sassone, M. Nielsen, and G. Winskel. Models for concurrency: Towards a classiﬁcation.Theoretical Computer Science, 170(1):297–348, 1996

1996
[52]

Sorgenfrey

R. Sorgenfrey. On the topological product of paracompact spaces.Bulletin of the American Mathematical Society, 53(6):631–632, 1947

1947
[53]

E. W. Stark. Concurrent transition systems.Theoretical Computer Science, 64(3):221–269, 1989

1989
[54]

R. Steiner. Omega-categories and chain complexes.Homology, Homotopy and Applications, 6(1):175–200, 2004

2004
[55]

W. Wilson. On quasi-metric spaces.American Journal of Mathematics, 53(3):675–684, 1931

1931
[56]

Winskel.Events in computation.PhD thesis, University of Edinburgh, 1980

G. Winskel.Events in computation.PhD thesis, University of Edinburgh, 1980

1980
[57]

Winskel and M

G. Winskel and M. Nielsen. Models for concurrency.DAIMI Report Series, 22(463), 1993. This work is licensed under the Creative Commons Attribution License. T o view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons,...

1993

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

G. E. Albert. A note on quasi-metric spaces.Bulletin of the American Mathematical Society, 47(6):479– 482, 1941

work page 1941

[2] [2]

Ardila, M

F. Ardila, M. Owen, and S. Sullivant. Geodesics in CAT(0) cubical complexes.Advances in Applied Mathematics, 48(1):142–163, 2012

work page 2012

[3] [3]

Barthélemy and J

J.-P. Barthélemy and J. Constantin. Median graphs, parallelism and posets.Discrete mathematics, 111(1):49–63, 1993

work page 1993

[4] [4]

Betti, A

R. Betti, A. Carboni, R. Street, and R. Walters. Variation through enrichment.Journal of Pure and Applied Algebra, 29(2):109–127, 1983

work page 1983

[5] [5]

Bezem, J

M. Bezem, J. Klop, R. de Vrijer, and Terese.Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003

work page 2003

[6] [6]

M. R. Bridson and A. Haeﬂiger.Metric spaces of non-positive curvature, volume 319. Springer, 2009

work page 2009

[7] [7]

V. Chepoi. Graphs of some CAT(0) complexes.Advances in Applied Mathematics, 24(2):125–179, 2000

work page 2000

[8] [8]

V. Chepoi. Nice labeling problem for event structures: a counterexample.SIAM Journal on Computing, 41(4):715–727, 2012

work page 2012