50 citations · 180 across the 26 of their papers we have counts for
27 papers
Proof Identity and Categorical Models of BV
Matteo Acclavio, Lutz Straßburger, Vladimir Zamdzhiev
BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-…
On the Centre of Strong Graded Monads
Flavien Breuvart, Quan Long, Vladimir Zamdzhiev
We introduce the notion of 'centre' for pomonoid-graded strong monads which generalizes some previous work that describes the centre of (not graded) strong monads. We show that, wh…
Quantum Coherence Spaces Revisited: A von Neumann (Co)Algebraic Approach
Thea Li, Vladimir Zamdzhiev
We describe a categorical model of MALL (Multiplicative Additive Linear Logic) inspired by the Heisenberg-Schrödinger duality of finite-dimensional quantum theory. Proofs of formul…
A programming language combining quantum and classical control
Kinnari Dave, Louis Lemonnier, Romain Péchoux +1
The two main notions of control in quantum programming languages are often referred to as "quantum control" and "classical control". With the latter, the control flow is based on c…
IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation
Kinnari Dave, Alejandro Díaz-Caro, Vladimir Zamdzhiev
We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language s…
Operator Spaces, Linear Logic and the Heisenberg-Schrödinger Duality of Quantum Theory
Bert Lindenhovius, Vladimir Zamdzhiev
We show that the category OS of operator spaces, with complete contractions as morphisms, is locally countably presentable and a model of Intuitionistic Linear Logic in the sense o…
The Category of Operator Spaces and Complete Contractions
Bert Lindenhovius, Vladimir Zamdzhiev
We show that the category OS of operator spaces, with complete contractions as morphisms, is locally countably presentable. This result, together with its symmetric monoidal closed…
Proceedings of the 21st International Conference on Quantum Physics and Logic
Alejandro Díaz-Caro, Vladimir Zamdzhiev
This volume contains the proceedings of the 21st International Conference on Quantum Physics and Logic (QPL 2024), which was held from July 15th to 19th, 2024, in Buenos Aires, Arg…
Proceedings of the Twentieth International Conference on Quantum Physics and Logic
Shane Mansfield, Benoît Valiron, Vladimir Zamdzhiev
This volume contains the proceedings of the 20th International Conference on Quantum Physics and Logic (QPL 2023). The aim of the QPL conference series is to bring together academi…
Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
TItouan Carette, Louis Lemonnier, Vladimir Zamdzhiev
Monads in category theory are algebraic structures that can be used to model computational effects in programming languages. We show how the notion of "centre", and more generally…
Quantum Expectation Transformers for Cost Analysis
Martin Avanzini, Georg Moser, Romain Péchoux +2
We introduce a new kind of expectation transformer for a mixed classical-quantum programming language. Our semantic approach relies on a new notion of a cost structure, which we in…
The Central Valuations Monad
Xiaodong Jia, Michael Mislove, Vladimir Zamdzhiev
We give a commutative valuations monad Z on the category DCPO of dcpo's and Scott-continuous functions. Compared to the commutative valuations monads given in [Jia et al., 2021], o…
Qimaera: Type-safe (Variational) Quantum Programming in Idris
Liliane-Joy Dandy, Emmanuel Jeandel, Vladimir Zamdzhiev
Variational Quantum Algorithms are hybrid classical-quantum algorithms where classical and quantum computation work in tandem to solve computational problems. These algorithms crea…
Semantics for Variational Quantum Programming
Xiaodong Jia, Andre Kornell, Bert Lindenhovius +2
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is…
Commutative Monads for Probabilistic Programming Languages
Xiaodong Jia, Bert Lindenhovius, Michael Mislove +1
A long-standing open problem in the semantics of programming languages supporting probabilistic choice is to find a commutative monad for probability on the category DCPO. In this…
Computational Adequacy for Substructural Lambda Calculi
Vladimir Zamdzhiev
Substructural type systems, such as affine (and linear) type systems, are type systems which impose restrictions on copying (and discarding) of variables, and they have found many…
Semantics for first-order affine inductive data types via slice categories
Vladimir Zamdzhiev
Affine type systems are substructural type systems where copying of information is restricted, but discarding of information is permissible at all types. Such type systems are well…
Quantum Programming with Inductive Datatypes: Causality and Affine Type Theory
Romain Péchoux, Simon Perdrix, Mathys Rennela +1
Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive dat…
Reflecting Algebraically Compact Functors
Vladimir Zamdzhiev
A compact T-algebra is an initial T-algebra whose inverse is a final T-coalgebra. Functors with this property are said to be algebraically compact. This is a very strong property u…
LNL-FPC: The Linear/Non-linear Fixpoint Calculus
Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev
We describe a type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus). The type system supports linear typing, which e…
A Framework for Rewriting Families of String Diagrams
Vladimir Zamdzhiev
We describe a mathematical framework for equational reasoning about infinite families of string diagrams which is amenable to computer automation. The framework is based on context…
Enriching a Linear/Non-linear Lambda Calculus: A Programming Language for String Diagrams
Bert Lindenhovius, Michael Mislove, Vladimir Zamdzhiev
Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a c…
Rewriting Context-free Families of String Diagrams
Vladimir Nikolaev Zamdzhiev
String diagrams provide a convenient graphical framework which may be used for equational reasoning about morphisms of monoidal categories. However, unlike term rewriting, rewritin…
Equational reasoning with context-free families of string diagrams
Aleks Kissinger, Vladimir Zamdzhiev
String diagrams provide an intuitive language for expressing networks of interacting processes graphically. A discrete representation of string diagrams, called string graphs, allo…