DOI10.1017/S096012950100336XzbMath1051.03045OpenAlexW2145617779MaRDI QIDQ2732138
Jean-Yves Girard
Publication date: 23 July 2001
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s096012950100336x
Models of Linear Logic based on the Schwartz $\varepsilon$-product,
Formal ontologies and coherent spaces,
On dialogue games and graph games,
Structure of proofs and the complexity of cut elimination,
Polarized games,
From Focalization of Logic to the Logic of Focalization,
Game Semantics and the Manifestation Thesis,
Non-linearity as the Metric Completion of Linearity,
Theorems as Constructive Visions,
Intuitionistic games: determinacy, completeness, and normalization,
Differential interaction nets,
A categorical semantics for polarized MALL,
Jump from parallel to sequential proofs: exponentials,
Imperative programs as proofs via game semantics,
Structural Focalization,
Figures of dialogue: a view from ludics,
An approach to innocent strategies as graphs,
A correspondence between maximal abelian sub-algebras and linear logic fragments,
Aristotle on Universal Quantification: A Study from the Point of View of Game Semantics,
Constructive semantics for instantaneous reactions,
Between syntax and semantics of resource oriented logic for IDS behavior description,
Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus,
Proof and refutation in MALL as a game,
A System F with Call-by-Name Exceptions,
The relational model is injective for multiplicative exponential linear logic (without weakenings),
Unnamed Item,
An Indexed System for Multiplicative Additive Polarized Linear Logic,
A logical characterization of forward and backward chaining in the inverse method,
Parametric \(\lambda \)-theories,
Verificationism and Classical Realizability,
Proof nets for classical logic,
Uniformity and the Taylor expansion of ordinary lambda-terms,
Classical realizability in the CPS target language,
Dialogues in Ludics,
Cut as Consequence,
Extended Lambek Calculi and First-Order Linear Logic,
Preface to the special volume,
Geometry of interaction. V: Logic in the hyperfinite factor,
Computational ludics,
On the unity of duality,
Rewriting systems for the surface classification theorem,
Substitution in non-wellfounded syntax with variable binding,
An exact correspondence between a typed pi-calculus and polarised proof-nets,
Softness of hypercoherences and MALL full completeness,
Interaction graphs: multiplicatives,
2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02,
Call-By-Push-Value from a Linear Logic Point of View,
Contraction-free Proofs and Finitary Games for Linear Logic,
Least and Greatest Fixed Points in Linear Logic,
On geometry of interaction for polarized linear logic,
Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic,
On the Meaning of Focalization,
Non-uniform (hyper/multi)coherence spaces,
On the Meaning of Logical Completeness,
Partial Orders, Event Structures and Linear Strategies,
A Polymorphic Type System for the Lambda-Calculus with Constructors,
Focalisation and Classical Realisability,
The λ-calculus with constructors: Syntax, confluence and separation,
From Hilbert's program to a logic tool box,
Game of grounds,
Syntax vs. semantics: A polarized approach,
Towards Ludics Programming: Interactive Proof Search,
An interpretation of CCS into ludics,
Proofs, Reasoning and the Metamorphosis of Logic,
A Graph Abstract Machine Describing Event Structure Composition,
Observational Equivalence for the Interaction Combinators and Internal Separation,
Gradual type theory,
Realizability models for a linear dependent PCF,
Unnamed Item,
Infinitary affine proofs,
Interactive observability in Ludics: the geometry of tests,
A calculus of coroutines