41 citations · 58 across the 7 of their papers we have counts for
7 papers
Extending Equational Monadic Reasoning with Monad Transformers
Reynald Affeldt, David Nowak
There is a recent interest for the verification of monadic programs using proof assistants. This line of research raises the question of the integration of monad transformers, a st…
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
Reynald Affeldt, Jacques Garrigue, David Nowak +1
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formaliz…
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
Vlad Rusu, David Nowak
Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems…
A Formalization of Polytime Functions
Sylvain Heraud, David Nowak
We present a deep embedding of Bellantoni and Cook's syntactic characterization of polytime functions. We prove formally that it is correct and complete with respect to the origina…
On formal verification of arithmetic-based cryptographic primitives
David Nowak
Cryptographic primitives are fundamental for information security: they are used as basic components for cryptographic protocols or public-key cryptosystems. In many cases, their s…
On the freeze quantifier in Constraint LTL: decidability and complexity
Stéphane Demri, Ranko Lazic, David Nowak
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze q…