Towards a typed geometry of interaction

DOI10.1017/S096012951000006XMaRDI QIDQ3564345zbMATH OpenFDO

Authors Esfandiar Haghverdi, Philip Scott

Publication date 2 June 2010

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S096012951000006X

zbMATH Keywords

cut eleminationgeometry of interactiontraced monoidal categories

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical logic, topoi (03G30)

Recommendations

• Computer Science Logic
• Proofs as Polynomials
• Typed GoI for Exponentials
• Automata, Languages and Programming
• A categorical model for the geometry of interaction

Cites work

• W^ *-categories
• A categorical framework for finite state machines
• A categorical model for the geometry of interaction
• A new duality theory for compact groups
• Feedback for linearly distributive categories: Traces and fixpoints
• Geometry of Interaction and linear combinatory algebras
• Glueing and orthogonality for models of linear logic
• Linear logic
• New foundations for the geometry of interaction
• Nuclear and trace ideals in tensored \(^*\)-categories
• On traced monoidal closed categories
• Towards a quantum programming language
• Traced monoidal categories
• Unique decomposition categories, Geometry of Interaction and combinatory logic

Cited in

(23)

• Partial traces on additive categories
• scientific article; zbMATH DE number 1722659 (Why is no real title available?)
• From geometry of interaction to denotational semantics
• A modified GoI interpretation for a linear functional programming language and its adequacy
• Geometry of interaction and the dynamics of proof reduction: a tutorial
• A Representation Theorem for Unique Decomposition Categories
• Strict geometry of interaction graph models
• Interaction graphs: graphings
• Typed GoI for Exponentials
• Geometry of interaction for MALL via Hughes-Van Glabbeek proof-nets
• Geometry of Interaction and linear combinatory algebras
• On geometry of interaction for polarized linear logic
• A \(\mathsf{MALL}\) geometry of interaction based on indexed linear logic
• Aspects of categorical recursion theory
• The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter
• Geometry of interaction. V: Logic in the hyperfinite factor
• Computer Science Logic
• Geometry of synthesis III
• Automata, Languages and Programming
• Types for Proofs and Programs
• On traces in categories of contractions
• A categorical model for the geometry of interaction
• Type interaction models and the rule of six

This page was built for publication: Towards a typed geometry of interaction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3564345)