Abstract: In two previous papers, we exposed a combinatorial approach to the program of Geometry of Interaction, a program initiated by Jean-Yves Girard. The strength of our approach lies in the fact that we interpret proofs by simpler structures - graphs - than Girard's constructions, while generalizing the latter since they can be recovered as special cases of our setting. This third paper extends this approach by considering a generalization of graphs named graphings, which is in some way a geometric realization of a graph. This very general framework leads to a number of new models of multiplicative-additive linear logic which generalize Girard's geometry of interaction models and opens several new lines of research. As an example, we exhibit a family of such models which account for second-order quantification without suffering the same limitations as Girard's models.
Recommendations
Cites work
- scientific article; zbMATH DE number 5851813 (Why is no real title available?)
- scientific article; zbMATH DE number 4179372 (Why is no real title available?)
- scientific article; zbMATH DE number 4091500 (Why is no real title available?)
- scientific article; zbMATH DE number 4099289 (Why is no real title available?)
- scientific article; zbMATH DE number 3462249 (Why is no real title available?)
- scientific article; zbMATH DE number 4123722 (Why is no real title available?)
- scientific article; zbMATH DE number 786500 (Why is no real title available?)
- scientific article; zbMATH DE number 5038458 (Why is no real title available?)
- A correspondence between maximal abelian sub-algebras and linear logic fragments
- CONCUR 2005 – Concurrency Theory
- Characterizingco-NLby a group action
- Cost of equivalence relations and groups
- Determinant theory in finite factors
- Elementary complexity and geometry of interaction
- Geometry of interaction. V: Logic in the hyperfinite factor
- Interaction graphs: additives
- Interaction graphs: graphings
- Interaction graphs: multiplicatives
- Linear logic
- Logarithmic space and permutations
- On the cost of generating an equivalence relation
- The geometry of linear higher-order recursion
- Three lightings of logic (Invited Talk)
- Transcendental syntax I: deterministic case
- Trees and amenable equivalence relations
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
- Unary resolution: characterizing \textsc{Ptime}
Cited in
(11)- Verificationism and Classical Realizability
- Interaction graphs: graphings
- Interaction graphs: multiplicatives
- Interaction graphs: full linear logic
- Unifying lower bounds for algebraic machines, semantically
- scientific article; zbMATH DE number 1974143 (Why is no real title available?)
- Interaction graphs: additives
- Zeta functions and the (linear) logic of Markov processes
- Interaction graphs: exponentials
- Coherent interaction graphs
- scientific article; zbMATH DE number 6917940 (Why is no real title available?)
This page was built for publication: Interaction graphs: graphings
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q345705)
