| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Thu, 11 Dec 2025 19:28:38 GMT
access-control-allow-origin: *
etag: W/"693b1b66-170a"
expires: Sun, 28 Dec 2025 03:17:04 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 1432:3946E9:7205CE:7FBEBA:69509ED7
accept-ranges: bytes
age: 0
date: Sun, 28 Dec 2025 03:07:04 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210054-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1766891225.666294,VS0,VE205
vary: Accept-Encoding
x-fastly-request-id: e149c79da37c7bc89d150209ac46561dc143c0f2
content-length: 1919
Guido Martínez
Research Engineer at Microsoft Research
I mostly work on the F* programming language / proof assistant.
Guido Martínez
Research Engineer at Microsoft Research
Email address: replace '.github.io' in this URL with '@gmail.com'.
I mostly work on the F* programming language / proof assistant.
Publications and Talks
-
SecRef*: Securely Sharing Mutable References Between Verified and Unverified Code in F*
Cezar-Constantin Andrici, Danel Ahman, Cătălin Hrițcu, Ruxandra Icleanu, Guido Martínez, Exequiel Rivas, Théo Winterhalter,
ICFP 2025 [ACM DL] [arXiv] -
Secure Parsing and Serializing with Separation Logic Applied to CBOR,
CDDL and COSE
Tahina Ramananandro, Gabriel Ebner, Guido Martínez, Nikhil Swamy
CCS 2025 [arXiv] -
Kuiper: verified and efficient GPU programming
Guido Martínez, Jonáš Fiala, Abhinav Jangda, Angélica Moreira, Nikhil Swamy, Tyler Sorensen
ARRAY 2025 [pdf] -
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, Nikhil Swamy
PLDI 2025 [pdf] [doi] -
Securing Verified IO Programs Against Unverified Code in F*
Cezar-Constantin Andrici, Stefan Ciobaca, Cătălin Hrițcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter,
POPL 2024 [pdf] [doi] -
Steel: Proof-Oriented Programming in a Dependently Typed
Concurrent Separation Logic
Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sidney Gibson, Guido Martínez, Denis Merigoux, Tahina Ramananandro
ICFP 2021 [pdf] [doi] [page] -
SteelCore: An Extensible Concurrent Separation Logic for
Effectful Dependently Typed Programs
Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Guido Martínez
ICFP 2020 [pdf] [doi] [page] -
Dijkstra Monads for All
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hrițcu, Exequiel Rivas, Éric Tanter
ICFP 2019 [pdf] [doi] [arXiv] -
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu, Nick Giannarakis, Chris Hawblitzel, Cătălin Hrițcu, Monal Narasimhamurthy, Zoe Paraskevopoulou, Clément Pit-Claudel, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy
ESOP 2019 [pdf] [doi] [arXiv] [page] -
Improving Typeclass Relations by Being Open
Guido Martínez, Mauro Jaskelioff, Guido De Luca
Haskell 2018 [pdf] [doi] -
Confluence in Probabilistic Rewriting
Alejandro Díaz-Caro, Guido Martínez
LSFA 2017 [pdf] [doi] [arXiv] -
Dijkstra Monads for Free
Danel Ahman, Cătălin Hrițcu, Kenji Maillard, Guido Martínez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy
POPL 2017 [pdf] [doi] [arXiv] [page]