A relational logic for higher-order programs A Aguirre, G Barthe, M Gaboardi, D Garg, PY Strub Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 68 | 2017 |
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, bayesian inference, and optimization T Sato, A Aguirre, G Barthe, M Gaboardi, D Garg, J Hsu Proceedings of the ACM on Programming Languages 3 (POPL), 1-30, 2019 | 38 | 2019 |
A pre-expectation calculus for probabilistic sensitivity A Aguirre, G Barthe, J Hsu, BL Kaminski, JP Katoen, C Matheja Proceedings of the ACM on Programming Languages 5 (POPL), 1-28, 2021 | 23 | 2021 |
Weakest preconditions in fibrations A Aguirre, S Katsumata Electronic Notes in Theoretical Computer Science 352, 5-27, 2020 | 18 | 2020 |
Relational reasoning for markov chains in a probabilistic guarded lambda calculus A Aguirre, G Barthe, L Birkedal, A Bizjak, M Gaboardi, D Garg Programming Languages and Systems: 27th European Symposium on Programming …, 2018 | 16 | 2018 |
Higher-order probabilistic adversarial computations: categorical semantics and program logics A Aguirre, G Barthe, M Gaboardi, D Garg, S Katsumata, T Sato Proceedings of the ACM on Programming Languages 5 (ICFP), 1-30, 2021 | 14 | 2021 |
Towards a provably correct encoding from F* to SMT A Aguirre Master's thesis, Université Paris 7, 2016 | 8 | 2016 |
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic SO Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, L Birkedal Proceedings of the ACM on Programming Languages 8 (POPL), 753-784, 2024 | 6 | 2024 |
Step-indexed logical relations for countable nondeterminism and probabilistic choice A Aguirre, L Birkedal Proceedings of the ACM on Programming Languages 7 (POPL), 33-60, 2023 | 4 | 2023 |
Weakest preconditions in fibrations A Aguirre, S Katsumata, S Kura Mathematical Structures in Computer Science 32 (4), 472-510, 2022 | 3 | 2022 |
Kantorovich continuity of probabilistic programs A Aguirre, G Barthe, J Hsu, BL Kaminski, JP Katoen, C Matheja arXiv preprint arXiv:1901.06540, 2019 | 3 | 2019 |
From F* to SMT A Aguirre, C Hritcu, C Keller, N Swamy Talk at 1st International Workshop on Hammers for Type Theories (HaTT), 2016 | 3 | 2016 |
Almost Sure Productivity A Aguirre, G Barthe, J Hsu, A Silva arXiv preprint arXiv:1802.06283, 2018 | 2 | 2018 |
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs A Aguirre, PG Haselwarter, M de Medeiros, KH Li, SO Gregersen, ... arXiv preprint arXiv:2404.14223, 2024 | 1 | 2024 |
Tachis: Higher-Order Separation Logic with Credits for Expected Costs PG Haselwarter, KH Li, M de Medeiros, SO Gregersen, A Aguirre, ... arXiv preprint arXiv:2405.20083, 2024 | | 2024 |
Almost-Sure Termination by Guarded Refinement SO Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, L Birkedal arXiv preprint arXiv:2404.08494, 2024 | | 2024 |
Almost-Sure Termination by Guarded Refinement S Oddershede Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, ... arXiv e-prints, arXiv: 2404.08494, 2024 | | 2024 |
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic S Oddershede Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, ... arXiv e-prints, arXiv: 2301.10061, 2023 | | 2023 |
Symbolic Synthesis of Indifferentiability Attacks I Rakotonirina, M Ambrona, A Aguirre, G Barthe Proceedings of the 2022 ACM on Asia Conference on Computer and …, 2022 | | 2022 |
A Relational Logic for Higher-Order Programs (Additional material) A AGUIRRE, G BARTHE, M GABOARDI, D GARG, PY STRUB | | 2017 |