2015/06/22 by Ugo Dal Lago, Lago, Ugo Dal, Alessandro Rioli +1
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1506.06661
openalex publication_date 2015/06/22 · openalex created_date 2022/10/01 · openalex updated_date 2026/08/01
Applicative bisimulation is a coinductive technique to check program equivalence in higher-order functional languages. It is known to be sound, and sometimes complete, with respect to context equivalence. In this paper we show that applicative bisimulation also works when the underlying language of programs takes the form of a linear λ-calculus extended with features such as probabilistic binary choice, but also quantum data, the latter being a setting in which linearity plays a role. The main results are proofs of soundness for the obtained notions of bisimilarity.