Strong embeddings into categories of algebras over a monad. II.
Strong functors and interleaving fixpoints in game semantics
We describe a sequent calculus μLJ with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of Gödel’s system T. We introduce the notion of a μ-closed category, relying on a uniform interpretation of open μLJ formulas as strong functors. We show that any μ-closed category is a sound model for μLJ. We then turn to the construction of a concrete μ-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients:...
Structures algébriques : thème et variations
Structures defined by finite limits in the enriched context, I
Structures pseudo-algébriques (1ère partie)
Subspaces in abstract Stone duality.
Sur la caractérisation sémantique des catégories de structures
Sur les produits tensoriels extérieurs de structures algébriques
Sur quelques problèmes de plongement en algèbre
Sur quelques problèmes de plongements en algèbre
Sur quelques structures de base pour définir les structures
Symmetric monoidal categories model all connective spectra.
Symmetric monoidal closed categories generated by commutative adjoint monads
Symmetry and Cauchy completion of quantaloid-enriched categories.
Syntactical theory of functors