Zobrazeno 1 - 10
of 298
pro vyhledávání: '"BIRKEDAL, LARS"'
Autor:
Stassen, Philipp Jan Andries, Møgelberg, Rasmus Ejlers, Zwart, Maaike, Aguirre, Alejandro, Birkedal, Lars
Constructive type theory combines logic and programming in one language. This is useful both for reasoning about programs written in type theory, as well as for reasoning about other programming languages inside type theory. It is well-known that it
Externí odkaz:
http://arxiv.org/abs/2408.04455
Autor:
Haselwarter, Philipp G., Li, Kwing Hei, Aguirre, Alejandro, Gregersen, Simon Oddershede, Tassarotti, Joseph, Birkedal, Lars
Publikováno v:
Proc. ACM Program. Lang. 9, POPL, Article 41 (January 2025)
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational program logics have been developed to reason about such approximate equ
Externí odkaz:
http://arxiv.org/abs/2407.14107
Autor:
Haselwarter, Philipp G., Li, Kwing Hei, de Medeiros, Markus, Gregersen, Simon Oddershede, Aguirre, Alejandro, Tassarotti, Joseph, Birkedal, Lars
Publikováno v:
Proc. ACM Program. Lang. 8, OOPSLA2, Article 313 (October 2024), 30 pages
We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probab
Externí odkaz:
http://arxiv.org/abs/2405.20083
Autor:
Aguirre, Alejandro, Haselwarter, Philipp G., de Medeiros, Markus, Li, Kwing Hei, Gregersen, Simon Oddershede, Tassarotti, Joseph, Birkedal, Lars
Probabilistic programs often trade accuracy for efficiency, and thus may, with a small probability, return an incorrect result. It is important to obtain precise bounds for the probability of these errors, but existing verification approaches have li
Externí odkaz:
http://arxiv.org/abs/2404.14223
Autor:
Gregersen, Simon Oddershede, Aguirre, Alejandro, Haselwarter, Philipp G., Tassarotti, Joseph, Birkedal, Lars
Almost-sure termination is an important correctness property for probabilistic programs, and a number of program logics have been developed for establishing it. However, these logics have mostly been developed for first-order programs written in lang
Externí odkaz:
http://arxiv.org/abs/2404.08494
Publikováno v:
Electronic Notes in Theoretical Informatics and Computer Science, Volume 3 - Proceedings of MFPS XXXIX (November 23, 2023) entics:12232
Separation logic is used to reason locally about stateful programs. State of the art program logics for higher-order store are usually built on top of untyped operational semantics, in part because traditional denotational methods have struggled to s
Externí odkaz:
http://arxiv.org/abs/2308.02906
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky's univalent foundations. We observe for the first time the prof
Externí odkaz:
http://arxiv.org/abs/2307.16608
We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present a
Externí odkaz:
http://arxiv.org/abs/2307.08514
Autor:
Gregersen, Simon Oddershede, Aguirre, Alejandro, Haselwarter, Philipp G., Tassarotti, Joseph, Birkedal, Lars
Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., s
Externí odkaz:
http://arxiv.org/abs/2301.10061
Publikováno v:
Journal of the ACM; Dec2024, Vol. 71 Issue 6, p1-75, 75p
