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 | 37 | 2021 |
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 | 16 | 2018 |
A general definition of dependent type theories A Bauer, PG Haselwarter, PLF Lumsdaine arXiv preprint arXiv:2009.05539, 2020 | 15 | 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 | 11 | 2023 |
Finitary Type Theories With and Without Contexts PG Haselwarter, A Bauer Journal of Automated Reasoning 67 (4), 1-87, 2023 | 9 | 2023 |
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic SO Gregersen, A Aguirre, PG Haselwarter, J Tassarotti, L Birkedal arXiv preprint arXiv:2301.10061, 2023 | 7 | 2023 |
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 |
The ‘Andromeda’ prover A Bauer, G Gilbert, PG Haselwarter, M Pretnar, C Stone | 5 | 2016 |
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography PG Haselwarter, BS Hvass, LL Hansen, T Winterhalter, C Hritcu, ... Cryptology ePrint Archive, 2023 | 4 | 2023 |
Effective Metatheory for Type Theory PG Haselwarter University of Ljubljana, Faculty of Mathematics and Physics, 2022 | 3 | 2022 |
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 |