| SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq C Abate, PG Haselwarter, E Rivas, A Van Muylder, T Winterhalter, ... 2021 IEEE 34th Computer Security Foundations Symposium (CSF), 1-15, 2021 | 45 | 2021 |
| 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), 2024 | 18 | 2024 |
| Design and Implementation of the Andromeda Proof Assistant A Bauer, G Gilbert, PG Haselwarter, M Pretnar, CA Stone 22nd International Conference on Types for Proofs and Programs (TYPES 2016) 97, 2018 | 18* | 2018 |
| A general definition of dependent type theories A Bauer, PG Haselwarter, PLF Lumsdaine arXiv preprint arXiv:2009.05539, 2020 | 17* | 2020 |
| SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq PG Haselwarter, E Rivas, A Van Muylder, T Winterhalter, C Abate, ... ACM Transactions on Programming Languages and Systems 45 (3), 1-61, 2023 | 15 | 2023 |
| Finitary Type Theories With and Without Contexts PG Haselwarter, A Bauer Journal of Automated Reasoning 67 (4), 1-87, 2023 | 8 | 2023 |
| The ‘Andromeda’ prover A Bauer, G Gilbert, PG Haselwarter, M Pretnar, C Stone | 8* | 2016 |
| Equality Checking for General Type Theories in Andromeda 2 A Bauer, PG Haselwarter, A Petković International Congress on Mathematical Software, 253-259, 2020 | 7 | 2020 |
| Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs A Aguirre, PG Haselwarter, M de Medeiros, KH Li, SO Gregersen, ... Proceedings of the ACM on Programming Languages 8 (ICFP), 284-316, 2024 | 6 | 2024 |
| The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography PG Haselwarter, BS Hvass, LL Hansen, T Winterhalter, C Hriţcu, ... Proceedings of the 13th ACM SIGPLAN International Conference on Certified …, 2024 | 6 | 2024 |
| Tachis: Higher-Order Separation Logic with Credits for Expected Costs PG Haselwarter, KH Li, M de Medeiros, SO Gregersen, A Aguirre, ... Proceedings of the ACM on Programming Languages 8 (OOPSLA2), 1189-1218, 2024 | 3 | 2024 |
| Approximate Relational Reasoning for Higher-Order Probabilistic Programs PG Haselwarter, KH Li, A Aguirre, SO Gregersen, J Tassarotti, L Birkedal Proceedings of the ACM on Programming Languages 9 (POPL), 1196-1226, 2025 | 2 | 2025 |
| Almost-Sure Termination by Guarded Refinement SO Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, L Birkedal Proceedings of the ACM on Programming Languages 8 (ICFP), 203-233, 2024 | 2 | 2024 |
| Effective Metatheory for Type Theory PG Haselwarter University of Ljubljana, Faculty of Mathematics and Physics, 2022 | 2 | 2022 |
| Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs KH Li, A Aguirre, SO Gregersen, PG Haselwarter, J Tassarotti, L Birkedal arXiv preprint arXiv:2503.04512, 2025 | | 2025 |
| On equality checking for general type theories: Implementation in Andromeda 2 A Bauer, PG Haselwarter, A Petković 26th International Conference on Types for Proofs and Programs, EUTYPES …, 2020 | | 2020 |
| Towards a Proof-Irrelevant Calculus of Inductive Constructions P Haselwarter Université Paris 7, 2014 | | 2014 |
| Passive Inference of Register Automata P Haselwarter | | 2013 |
Lars BirkedalDept. of Computer Science, Aarhus UniversityVerified email at cs.au.dk
