39 citations · 127 across the 31 of their papers we have counts for
6 papers · 1 filter
Practical Datatype Specializations with Phantom Types and Recursion Schemes
Matthew Fluet, Riccardo Pucella
Datatype specialization is a form of subtyping that captures program invariants on data structures that are expressed using the convenient and intuitive datatype notation. Of parti…
Evidence with Uncertain Likelihoods
Joseph Y. Halpern, Riccardo Pucella
An agent often has a number of hypotheses, and must choose among them based on observations, or outcomes of experiments. Each of these observations can be viewed as providing evide…
Logic Column 12: Logical Verification and Equational Verification
Riccardo Pucella
This article examines two approaches to verification, one based on using a logic for expressing properties of a system, and one based on showing the system equivalent to a simpler…
Probabilistic Algorithmic Knowledge
Joseph Y. Halpern, Riccardo Pucella
The framework of algorithmic knowledge assumes that agents use deterministic knowledge algorithms to compute the facts they explicitly know. We extend the framework to allow for ra…
Logic Column 11: The Finite and the Infinite in Temporal Logic
Riccardo Pucella
This article examines the interpretation of the LTL temporal operators over finite and infinite sequences. This is used as the basis for deriving a sound and complete axiomatizatio…
On Partially Additive Kleene Algebras
Riccardo Pucella
We define the notion of a partially additive Kleene algebra, which is a Kleene algebra where the + operation need only be partially defined. These structures formalize a number of…