output
20002026
most citedQuantum attacks on Bitcoin, and how to protect against them

225 citations

researchers with a paper here
collaborating institutions
Showing cs.LOShow all

83 papers · 1 filter

cs.LO2026

A uniform characterisation of the (a)synchronous must-preorder

Giovanni Bernardi, Hugo Férée, Gaëtan Lopez

In the setting of message passing software, De Nicola and Hennessy must-preorder defines when a program improves on another one. Since this preorder does not come equipped with a v…

cs.LO2026

Quantum Bayesian Networks: Compositionality and Typing via Linear Logic

Rémi Di Guardia, Thomas Ehrhard, Claudia Faggian

Quantum Bayesian networks provide a mathematical formalism to describe causal relations, to analyse correlations, and to predict the probabilities of measurement outcomes, in syste…

cs.LO2026

Synthetic Differential Geometry in Lean

Riccardo Brasca, Gabriella Clemente

This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formaliz…

cs.LO2026

Bidirectional Interpolation for the Lambda-Calculus: Revisiting and Formalising Craig-Čubrić Interpolation

Meven Lennon Bertrand, Alexis Saurin

Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follo…

cs.LO2026

The very dependent recursive structure of iterated parametricity in indexed form

Hugo Herbelin, Ramkumar Ramachandra

Reynolds' parametricity originally equips types with proof-irrelevant binary propositional relations over the types. But such relations can also be taken proof-relevant or unary, a…

cs.LO2025

Reversible computations are computations

Clément Aubert, Jean Krivine

Causality serves as an abstract notion of time for concurrent systems. A computation is causal, or simply valid, if each observation of a computation event is preceded by the obser…