8 citations · 22 across the 7 of their papers we have counts for
7 papers
Effect Algebras as Omega-categories
Lorenzo Perticone, Robin Adams
We show how an effect algebra can be regarded as a category, where the morphisms are the elements such that . This gives an emb…
Constructing Independently Verifiable Privacy-Compliant Type Systems for Message Passing between Black-Box Components
Robin Adams, Sibylle Schupp
Privacy by design (PbD) is the principle that privacy should be considered at every stage of the software engineering process. It is increasingly both viewed as best practice and r…
A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic
Robin Adams, Marc Bezem, Thierry Coquand
The univalence axiom expresses the principle of extensionality for dependent type theory. However, if we simply add the univalence axiom to type theory, then we lose the property o…
A Type Theory for Probabilistic and Bayesian Reasoning
Robin Adams, Bart Jacobs
This paper introduces a novel type theory and logic for probabilistic reasoning. Its logic is quantitative, with fuzzy predicates. It includes normalisation and conditioning of sta…
QPEL: Quantum Program and Effect Language
Robin Adams
We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - ef…
Classical Predicative Logic-Enriched Type Theories
Robin Adams, Zhaohui Luo
A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTTO and LTTO*, which we…