pQLL calculi assign real-valued strength to proofs, generalize hypersequent and deep inference systems, prove cut elimination, and achieve completeness for soft residuated lattices, recovering MALL as p goes to infinity.
Coupling proofs are probabilistic product programs
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
roles
background 1polarities
background 1representative citing papers
Develops an affine calculus and higher-order quantitative logic with novel guarded recursion and induction principles over probability measures and naturals, illustrated on Markov processes and learning algorithms.
Coq framework with discrete lenses for typed, compositional definition and verification of quantum circuits.
Typed extended decision diagrams enable scalable deductive verification of probabilistic programs by compactly representing weakest pre-expectations.
Parameterized concurrent program safety over topologies reduces to complete local compositional proofs via universally quantified inductive invariants.
Ultimate TreeAutomizer is a CHC solver based on trace abstraction, tree automata and tree interpolation, presented as a tool description for the CHC-COMP 2019 competition.
citing papers explorer
-
Quantitative Linear Logic
pQLL calculi assign real-valued strength to proofs, generalize hypersequent and deep inference systems, prove cut elimination, and achieve completeness for soft residuated lattices, recovering MALL as p goes to infinity.
-
Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
Develops an affine calculus and higher-order quantitative logic with novel guarded recursion and induction principles over probability measures and naturals, illustrated on Markov processes and learning algorithms.
-
Typed compositional quantum computation with lenses
Coq framework with discrete lenses for typed, compositional definition and verification of quantum circuits.
-
Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
Typed extended decision diagrams enable scalable deductive verification of probabilistic programs by compactly representing weakest pre-expectations.
-
Complete Local Reasoning About Parameterized Programs Over Topologies
Parameterized concurrent program safety over topologies reduces to complete local compositional proofs via universally quantified inductive invariants.
-
Ultimate TreeAutomizer (CHC-COMP Tool Description)
Ultimate TreeAutomizer is a CHC solver based on trace abstraction, tree automata and tree interpolation, presented as a tool description for the CHC-COMP 2019 competition.