-
Reynald Affeldt,
Jacques Garrigue,
David Nowak,
and Takafumi Saikawa.
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism.
arXiv:2003.09993 [cs],
March 2020.
Keyword(s): probability.
Abstract: |
REYNALD AFFELDT, National Institute of Advanced Industrial Science and Technology, Japan JACQUES GARRIGUE, Nagoya University, Japan DAVID NOWAK, CNRS \& Lille University, France TAKAFUMI SAIKAWA, Nagoya University, Japan 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 formalization (the first one to the best of our knowledge) in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories. |
@article{affeldtTrustfulMonadAxiomatic2020,
title = {A {{Trustful Monad}} for {{Axiomatic Reasoning}} with {{Probability}} and {{Nondeterminism}}},
author = {Affeldt, Reynald and Garrigue, Jacques and Nowak, David and Saikawa, Takafumi},
year = {2020},
month = mar,
abstract = {REYNALD AFFELDT, National Institute of Advanced Industrial Science and Technology, Japan JACQUES GARRIGUE, Nagoya University, Japan DAVID NOWAK, CNRS \& Lille University, France TAKAFUMI SAIKAWA, Nagoya University, Japan 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 formalization (the first one to the best of our knowledge) in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4339-Affeldt et al (2020) - A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism.pdf},
journal = {arXiv:2003.09993 [cs]},
keywords = {probability},
}
-
Reynald Affeldt,
Jacques Garrigue,
and Takafumi Saikawa.
A Library for Formalization of Linear Error-Correcting Codes.
Journal of Automated Reasoning,
January 2020.
ISSN: 1573-0670.
Keyword(s): Coq,
probability.
Abstract: |
Error-correcting codes add redundancy to transmitted data to ensure reliable communication over noisy channels. Since they form the foundations of digital communication, their correctness is a matter of concern. To enable trustful verification of linear error-correcting codes, we have been carrying out a systematic formalization in the Coq proof-assistant. This formalization includes the material that one can expect of a university class on the topic: the formalization of well-known codes (Hamming, Reed- Solomon, Bose- Chaudhuri- Hocquenghem) and also a glimpse at modern coding theory. We demonstrate the usefulness of our formalization by extracting a verified decoder for low-density parity-check codes based on the sum-product algorithm. To achieve this formalization, we needed to develop a number of libraries on top of Coq's Mathematical Components. Special care was taken to make them as reusable as possible so as to help implementers and researchers dealing with error-correcting codes in the future. |
@article{affeldtLibraryFormalizationLinear2020,
title = {A {{Library}} for {{Formalization}} of {{Linear Error}}-{{Correcting Codes}}},
author = {Affeldt, Reynald and Garrigue, Jacques and Saikawa, Takafumi},
year = {2020},
month = jan,
issn = {1573-0670},
doi = {10.1007/s10817-019-09538-8},
abstract = {Error-correcting codes add redundancy to transmitted data to ensure reliable communication over noisy channels. Since they form the foundations of digital communication, their correctness is a matter of concern. To enable trustful verification of linear error-correcting codes, we have been carrying out a systematic formalization in the Coq proof-assistant. This formalization includes the material that one can expect of a university class on the topic: the formalization of well-known codes (Hamming, Reed- Solomon, Bose- Chaudhuri- Hocquenghem) and also a glimpse at modern coding theory. We demonstrate the usefulness of our formalization by extracting a verified decoder for low-density parity-check codes based on the sum-product algorithm. To achieve this formalization, we needed to develop a number of libraries on top of Coq's Mathematical Components. Special care was taken to make them as reusable as possible so as to help implementers and researchers dealing with error-correcting codes in the future.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4335-Affeldt et al (2020) - A Library for Formalization of Linear Error-Correcting Codes.pdf},
journal = {Journal of Automated Reasoning},
keywords = {Coq,probability},
}
-
Davide Ancona,
Pietro Barbieri,
Francesco Dagnino,
and Elena Zucca.
Sound Regular Corecursion in coFJ.
arXiv:2005.14085 [cs],
May 2020.
Keyword(s): Java,
streams.
Abstract: |
The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one. |
@article{anconaSoundRegularCorecursion2020,
title = {Sound {{Regular Corecursion}} in {{coFJ}}},
author = {Ancona, Davide and Barbieri, Pietro and Dagnino, Francesco and Zucca, Elena},
year = {2020},
month = may,
abstract = {The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4547 - Ancona et al (2020) - Sound Regular Corecursion in coFJ.pdf},
journal = {arXiv:2005.14085 [cs]},
keywords = {Java,streams},
}
-
Ryan Beckett,
Aarti Gupta,
Ratul Mahajan,
and David Walker.
Abstract Interpretation of Distributed Network Control Planes.
Proceedings of the ACM on Programming Languages,
4(POPL):1-27,
January 2020.
ISSN: 2475-1421, 2475-1421.
Keyword(s): abstract interpretation.
@article{beckettAbstractInterpretationDistributed2020,
title = {Abstract Interpretation of Distributed Network Control Planes},
author = {Beckett, Ryan and Gupta, Aarti and Mahajan, Ratul and Walker, David},
year = {2020},
month = jan,
volume = {4},
pages = {1--27},
issn = {2475-1421, 2475-1421},
doi = {10.1145/3371110},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4621-Beckett et al (2020) - Abstract interpretation of distributed network control planes.pdf},
journal = {Proceedings of the ACM on Programming Languages},
keywords = {abstract interpretation},
number = {POPL}
}
-
Gianluca Curzi and Luca Roversi.
Probabilistic Soft Type Assignment.
arXiv:2007.01733 [cs],
July 2020.
Keyword(s): calculus,
probability.
Abstract: |
We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; they allow for duplications harmlessly affecting the computational cost of normalization. PSTA is sound and complete w.r.t. probabilistic polynomial time functions and characterizes the probabilistic complexity classes PP and BPP, the latter slightly less implicitly than PP. |
@article{curziProbabilisticSoftType2020,
title = {Probabilistic {{Soft Type Assignment}}},
author = {Curzi, Gianluca and Roversi, Luca},
year = {2020},
month = jul,
abstract = {We model randomized complexity classes in the style of Implicit Computational Complexity. We introduce PSTA, a probabilistic version of STA, the type-theoretical counterpart of Soft Linear Logic. PSTA is a type assignment for an extension of Simpson's Linear Lambda Calculus and its surface reduction, where Linear additives express random choice. Linear additives are weaker than the usual ones; they allow for duplications harmlessly affecting the computational cost of normalization. PSTA is sound and complete w.r.t. probabilistic polynomial time functions and characterizes the probabilistic complexity classes PP and BPP, the latter slightly less implicitly than PP.},
archivePrefix = {arXiv},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4532 - Curzi and Roversi - 2020 - Probabilistic Soft Type Assignment.pdf},
journal = {arXiv:2007.01733 [cs]},
keywords = {calculus,probability},
}