Strong functors and interleaving fixpoints in game semantics

DOI10.1051/ITA/2012028MaRDI QIDQ2842239zbMATH OpenOpenAlexFDO

Authors Pierre Clairambault

Publication date 13 August 2013

Published in RAIRO. Theoretical Informatics and Applications (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/6baa7eb05615299aed1b9ac844d18fbc954c47ad

zbMATH Keywords

coinductive typesgame semanticsinductive typesinitial algebrasstrong functorsterminal coalgebras

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Theories (e.g., algebraic theories), structure, and semantics (18C10)

Review text

The paper develops a sequent calculus for inductive and coinductive types and endows it with reduction rules for allowing a sound translation of Gödel's system \(T\). The authors introduce a categorical model for the calculus and build a concrete instance based on Hyland-Ong game semantics. A weak completeness result is proved for this model, that yields a normalisation proof for the calculus.

Recommendations

• Least and Greatest Fixpoints in Game Semantics
• μ-Bicomplete Categories and Parity Games
• Games and full abstraction for FPC.
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes
• A Theory for Game Theories

Cited in

(7)

• Fixed-Point Elimination in the Intuitionistic Propositional Calculus
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes
• Least and Greatest Fixpoints in Game Semantics
• μ-Bicomplete Categories and Parity Games
• scientific article; zbMATH DE number 1424046 (Why is no real title available?)
• Computational expressivity of (circular) proofs with fixed points
• Totality for mixed inductive and coinductive types

This page was built for publication: Strong functors and interleaving fixpoints in game semantics

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