| Dijkstra monads for free D Ahman, C Hriţcu, K Maillard, G Martínez, G Plotkin, J Protzenko, ... Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017 | 82 | 2017 |
| Dijkstra monads for all K Maillard, D Ahman, R Atkey, G Martínez, C Hriţcu, E Rivas, É Tanter Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019 | 71 | 2019 |
| Meta-f: Proof automation with smt, tactics, and metaprograms G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ... European Symposium on Programming, 30-59, 2019 | 59 | 2019 |
| SteelCore: an extensible concurrent separation logic for effectful dependently typed programs N Swamy, A Rastogi, A Fromherz, D Merigoux, D Ahman, G Martínez Proceedings of the ACM on Programming Languages 4 (ICFP), 1-30, 2020 | 46 | 2020 |
| Steel: proof-oriented programming in a dependently typed concurrent separation logic A Fromherz, A Rastogi, N Swamy, S Gibson, G Martínez, D Merigoux, ... Proceedings of the ACM on Programming Languages 5 (ICFP), 1-30, 2021 | 33 | 2021 |
| Confluence in probabilistic rewriting A Díaz-Caro, G Martinez Electronic Notes in Theoretical Computer Science 338, 115-131, 2018 | 15 | 2018 |
| Securing Verified IO Programs Against Unverified Code in F CC Andrici, Ș Ciobâcă, C Hriţcu, G Martínez, E Rivas, É Tanter, ... Proceedings of the ACM on Programming Languages 8 (POPL), 2226-2259, 2024 | 4 | 2024 |
| Partial dijkstra monads for all T Winterhalter, CC Andrici, C Hriţcu, K Maillard, G Martínez, E Rivas Proceedings of the International Conference on Types for Proofs and Programs …, 2022 | 4 | 2022 |
| Proof-Oriented Programming in F* N Swamy, G Martinez, A Rastogi | 3 | 2023 |
| Programming and Proving with Indexed Effects A Rastogi, G Martínez, A Fromherz, T Ramananandro, N Swamy Microsoft Research, 2020 | 3 | 2020 |
| SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F CC Andrici, D Ahman, C Hritcu, R Icleanu, G Martínez, E Rivas, ... arXiv preprint arXiv:2503.00404, 2025 | | 2025 |
| Securely Compiling Verified F* Programs With IO. CC Andrici, C Hritcu, G Martínez, E Rivas, T Winterhalter CoRR, 2023 | | 2023 |
| Dijkstra Monads for All D AHMAN, R ATKEY, G MARTÍNEZ, H CĂTĂLIN, R EXEQUIEL, ... | | 2019 |
| Improving typeclass relations by being open G Martínez, M Jaskelioff, G De Luca ACM SIGPLAN Notices 53 (7), 68-80, 2018 | | 2018 |
| Layered Indexed Effects A RASTOGI, G MARTÍNEZ, A FROMHERZ, T RAMANANANDRO, ... | | |
| ML as a Tactic Language, Again G MARTÍNEZ, D AHMAN, V DUMITRESCU, N GIANNARAKIS, ... | | |
