Bialgebraic reasoning on higher-order program equivalence
From MaRDI portal
Cites work
- A categorical approach to secure compilation
- A fibrational tale of operational logical relations
- A Kripke logical relation between ML and assembly
- A theory of type polymorphism in programming
- Bialgebraic reasoning on higher-order program equivalence
- Biorthogonality, step-indexing and compiler correctness
- Bisimilarity as a theory of functional programming
- Cerise: program verification on a capability machine in the presence of untrusted code
- Differential logical relations. I: The simply-typed case
- Differential logical relations. II: Increments and derivatives
- Fully Abstract and Robust Compilation
- Fully abstract compilation via universal embedding
- Fully-abstract compilation by approximate back-translation
- scientific article; zbMATH DE number 431771 (Why is no real title available?)
- scientific article; zbMATH DE number 4180818 (Why is no real title available?)
- scientific article; zbMATH DE number 5318491 (Why is no real title available?)
- scientific article; zbMATH DE number 1241702 (Why is no real title available?)
- scientific article; zbMATH DE number 555217 (Why is no real title available?)
- scientific article; zbMATH DE number 195102 (Why is no real title available?)
- scientific article; zbMATH DE number 822489 (Why is no real title available?)
- scientific article; zbMATH DE number 7774231 (Why is no real title available?)
- Intensional interpretations of functionals of finite type I
- Introduction to coalgebra. Towards mathematics of states and observation
- Introduction to extensive and distributive categories
- Kripke logical relations and PCF
- Lax bialgebras and up-to techniques for weak bisimulations
- Logical predicates in higher-order mathematical operational semantics
- Logical relations and parametricity -- a Reynolds programme for category theory and programming languages
- Logical relations and the typed λ-calculus
- Logical relations for monadic types
- Modelling environments in call-by-value programming languages.
- Normalisation by evaluation for dependent types
- On cool congruence formats for weak bisimulations
- Operational equivalences for untyped and polymorphic object calculi
- Operational reasoning for functions with local state
- Parametric polymorphism and operational equivalence
- Parametricity in an impredicative sort
- Programming Languages and Systems
- Proofs for free. Parametricity for dependent types
- Proving congruence of bisimulation in functional programming languages
- Relational properties of domains
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- State-dependent representation independence
- Step-indexed logical relations for probability
- Structural induction and coinduction in a fibrational setting
- Structural operational semantics for weak bisimulations
- The category-theoretic solution of recursive metric-space equations
- The impact of higher-order state and control effects on local relational reasoning
- The marriage of bisimulations and Kripke logical relations
- Universal coalgebra: A theory of systems
- Verifying an Open Compiler Using Multi-language Semantics
- Weak similarity in higher-order mathematical operational semantics
- Well-behaved translations between structural operational semantics
This page was built for publication: Bialgebraic reasoning on higher-order program equivalence
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6970238)