Related papers: A Trustful Monad for Axiomatic Reasoning with Prob…
We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads,…
One can perform equational reasoning about computational effects with a purely functional programming language thanks to monads. Even though equational reasoning for effectful programs is desirable, it is not yet mainstream. This is partly…
The monad of convex sets of probability distributions is a well-known tool for modelling the combination of nondeterministic and probabilistic computational effects. In this work we lift this monad from the category of sets to the category…
Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…
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 standard technique to combine monads. In this paper, we extend…
As part of the author's studies on equational reasoning for monadic programs, this report focus on non-determinism monad. We discuss what properties this monad should satisfy, what additional operators and notations can be introduced to…
We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define…
We discuss some aspects of our work on the mechanization of syntax and semantics in the UniMath library, based on the proof assistant Coq. We focus on experiences where Coq (as a type-theoretic proof assistant with decidable typechecking)…
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics…
Context-free language theory is a well-established area of mathematics, relevant to computer science foundations and technology. This paper presents the preliminary results of an ongoing formalization project using context-free grammars and…
Describing systems in terms of choices and their resulting costs and rewards offers the promise of freeing algorithm designers and programmers from specifying how those choices should be made; in implementations, the choices can be realized…
Probabilistic puzzles can be confusing, partly because they are formulated in natural languages - full of unclarities and ambiguities - and partly because there is no widely accepted and intuitive formal language to express them. We propose…
Constructive-deductive method for plane Euclidean geometry is proposed and formalized within Coq Proof Assistant. This method includes both postulates that describe elementary constructions by idealized geometric tools (pencil, straightedge…
Imprecise probability is concerned with uncertainty about which probability distributions to use. It has applications in robust statistics and machine learning. We look at programming language models for imprecise probability. Our…
Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different tools are being increasingly used in…
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets in vector spaces, we formalize in Coq an intrinsic…
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a specification monad. We prove that any monad morphism…
This paper describes a formal proof library, developed using the Coq proof assistant, designed to assist users in writing correct diagrammatic proofs, for 1-categories. This library proposes a deep-embedded, domain-specific formal language,…
The paper presents algebraic and logical developments. From the algebraic viewpoint, we introduce Monadic Equational Systems as an abstract enriched notion of equational presentation. From the logical viewpoint, we provide Equational…
We explore language semantics for automata combining probabilistic and nondeterministic behavior. We first show that there are precisely two natural semantics for probabilistic automata with nondeterminism. For both choices, we show that…