A fibrational tale of operational logical relations: pure, effectful and differential
From MaRDI portal
Publication:6563048
DOI10.46298/LMCS-20(2:1)2024MaRDI QIDQ6563048
Francesco Dagnino, Francesco Gavazzo
Publication date: 27 June 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Could not fetch data.
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Relation lifting, a survey
- Borel structures for function spaces
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Bicategories of spans and relations
- Structural induction and coinduction in a fibrational setting
- Modelling environments in call-by-value programming languages.
- Weak subobjects and the epi-monic completion of a category.
- Algebraic operations and generic effects
- Relating computational effects by \(\top \top \)-lifting
- Effectful applicative similarity for call-by-name lambda calculi
- On bisimilarity in lambda calculi with continuous probabilistic choice
- Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics
- The formal theory of monads
- A Kripke logical relation for effect-based program transformations
- Differential logical relations. II: Increments and derivatives
- Types and programing languages
- Practical foundations for programming languages
- Functors are type refinement systems
- Factorization systems and fibrations: toward a fibred Birkhoff variety theorem
- Elementary quotient completion
- Syntactic Logical Relations for Polymorphic and Recursive Types
- Generic Fibrational Induction
- Logical relations for fine-grained concurrency
- Step-Indexed Logical Relations for Probability
- A lambda-calculus foundation for universal probabilistic programming
- Commutative Semantics for Probabilistic Programming
- The impact of higher-order state and control effects on local relational reasoning
- Logical relations for monadic types
- Fibrational Induction Rules for Initial Algebras
- Framed bicategories and monoidal fibrations
- Logical relations and the typed λ-calculus
- Parametricity and local variables
- Codensity Lifting of Monads and its Dual
- Introduction to bicategories
- Coinduction up-to in a fibrational setting
- Semantics for probabilistic programming
- A bifibrational reconstruction of Lawvere's presheaf hyperdoctrine
- Up-To Techniques for Behavioural Metrics via Fibrations
- Doctrines, modalities and comonads
- Differential logical relations, Part I: The simply-typed case
- Quantitative Behavioural Reasoning for Higher-order Effectful Programs
- A General Framework for Relational Parametricity
- Distance makes the types grow stronger
- Logical Relations and Nondeterminism
- Computer Science Logic
- Abstract effects and proof-relevant logical relations
- Parametric effect monads and semantics of effect systems
- Intensional interpretations of functionals of finite type I
- Relational algebras
- Programming Languages and Systems
- Effectful normal form bisimulation
- Types, abstraction, and parametric polymorphism, part 2
- A fibrational tale of operational logical relations
This page was built for publication: A fibrational tale of operational logical relations: pure, effectful and differential
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6563048)
