Reference. Fixpoint constructions in focused orthogonality models of linear logic
Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.
Cite
Cites 43 works (4 here)
With notes (4)
Glueing and orthogonality for models of linear logic hyland_glueing_2003
We present the general theory of the method of glueing and associated technique of orthogonality for constructing categorical models of all the structure of linear logic: in particular we treat the exponentials in detail. We indicate simple applications of the methods and show that they cover familiar examples.
Axiomatic Domain Theory in Categories of Partial Maps fiore-1996-axiomatic
Axiomatic categorical domain theory is crucial for understanding the meaning of programs and reasoning about them. This book is the first systematic account of the subject and studies mathematical structures suitable for modelling functional programming languages in an axiomatic (i.e. abstract) setting. In particular, the author develops theories of partiality and recursive types and applies them to the study of the metalanguage FPC; for example, enriched categorical models of the FPC are defined. Furthermore, FPC is considered as a programming language with a call-by-value operational semantics and a denotational semantics defined on top of a categorical model. To conclude, for an axiomatisation of absolute non-trivial domain-theoretic models of FPC, operational and denotational semantics are related by means of computational soundness and adequacy results. To make the book reasonably self-contained, the author includes an introduction to enriched category theory.
Linear logic girard_linear_1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
External (39)
- Double glueing over free exponential: With measure theoretic applications (2026)
- Phase Semantics for Linear Logic with Least and Greatest Fixed Points (2022)
- Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings (2022)
- Categorical models of Linear Logic with fixed points of formulas (2021)
- Transport of finiteness structures and applications (2016)
- Probabilistic coherence spaces are fully abstract for probabilistic PCF (2014)
- Weighted Relational Models of Typed Lambda-Calculi (2013)
- Least and Greatest Fixed Points in Linear Logic (2012)
- Collapsing non-idempotent intersection types (2012)
- Probabilistic coherence spaces as a model of higher-order probabilistic computation (2011)
- The Scott model of linear logic is the extensional collapse of its relational model (2011)
- Second-Order Equational Logic (2010)
- CATEGORICAL SEMANTICS OF LINEAR LOGIC (2009)
- Realizability in classical logic (2009)
- Finiteness spaces (2005)
- What is a categorical model of linear logic? (manuscript) (2004)
- Complete axioms for categorical fixed-point operators (2000)
- Structural Induction and Coinduction in a Fibrational Setting (1998)
- A theory of recursive domains with applications to concurrency (1998)
- Full completeness for models of linear logic (PhD thesis) (1998)
- Game Semantics (1997)
- A constructive proof of Tarski's fixed-point theorem for dcpo's (talk, 65th PSSL) (1997)
- Traced monoidal categories (1996)
- Linear Logic: its syntax and semantics (1995)
- Linear logic, totality and full completeness (1994)
- Quantitative domains and infinitary algebras (1992)
- Fixpoint theorem in linear logic (email to linear@cs.stanford.edu) (1992)
- Algebraically complete categories (1991)
- Categories, Allegories (1990)
- Proofs and Types (1989)
- The system F of variable types, fifteen years later (1986)
- Logical relations and the typed lambda-calculus (1985)
- The category-theoretic solution of recursive domain equations (1982)
- Fixed-point constructions in order-enriched categories (1979)
- Artin glueing (1974)
- Théorie des topos et cohomologie étale des schémas, tome 3 (SGA 4) (1973)
- Lambda-definability and logical relations (1973)
- Continuous lattices (1972)
- Intensional interpretations of functionals of finite type I (1967)