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
-
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]