About Me
I have been a postdoc at the IMDEA Software Institute, where I worked in Alexey Gotsman's group. My research interests include distributed ledgers, software verification and formal methods. Before that, I was a postdoc at ICE-TCS, Reykjavik University, under the supervision of Luca Aceto.
I obtained my PhD degree from the IMDEA Software Institute and the Universidad Politécnica de Madrid, where I was a member of the Babel Group. My PhD advisors are Juan José Moreno Navarro and Pablo Nogueira.
See my Résumé,
my Curriculum
Vitae, and in 
FECYT CVN format.
Papers
For all my publications, use your preferred from the profiles below.
[
Google Scholar |
Microsoft Academic |
dblp
|
ORCID |
Scopus |
ACM]
Seelected Journal Papers
- Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir and Yolanda Ortega-Mallén. Rule Formats for Nominal Process Calculi. Logical Methods in Computer Science, 15(4):2:1–2:46(2019). August 2019. [doi]
- Álvaro García-Pérez and Pablo Nogueira. The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus. Journal of Functional Programming, 29(E7)(2019). April 2019. Cambridge University Press. [doi]
- Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez and Anna Ingólfsdóttir. A unified rule format for bounded nondeterminism in SOS with terms as labels. Logical and Algebraic Methods in Programming, 92:64–87(2017). March 2017. Springer. [doi]
- Álvaro García-Pérez and Pablo Nogueira. No solvable lambda-value term left behind. Logical Methods in Computer Science, 12(2:12):1–43(2016). May 2016. [doi | code]
Selected Conference Papers
- Álvaro García-Pérez and Maria A. Schett. Deconstructing Stellar Consensus. In Proceedings of the 23rd International Conference on Principles of Distributed Systems (OPODIS 2019), December 2019. [doi]
- Álvaro García-Pérez and Alexey Gotsman. Federated Byzantine Quorum Systems. In Proceedings of the 22nd International Conference on Principles of Distributed Systems (OPODIS 2018), December 2018. [doi]
- Álvaro García-Pérez, Alexey Gotsman, Yuri Mesman and Ilya Sergey. Paxos consensus, deconstructed and abstracted. In Proceedings of the European Symposium on Programming (ESOP 2018), April 2018. [doi]
- Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir and Yolanda Ortega-Mallén. Rule formats for nominal process calculi. In Proceedings of the 28th International Conference on Concurrency Theory (CONCUR 2017), pages 10:1–10-16, Berlin, Germany, September 2017. [doi]
- Álvaro García-Pérez, Pablo Nogueira and Juan José Moreno-Navarro. Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming (PPDP 2013), pages 85–96, Madrid, Spain, September 2013. ACM. [doi | code]
PhD Dissertation
- Álvaro García Pérez. Operational aspects of full reduction in lambda calculi. Departamento de Lenguages, Sistemas Informáticos e Ingeniería de Software. Escuela Técnica Superior de Ingenieros Informáticos. Universidad Politécnica de Madrid, Spain. [pdf]
Other Publications
- Amaya García Pérez and Álvaro García Pérez. La afinación de la flauta tradicional salmantina de tres agujeros. Revista de Musicología, 32(2):343–361(2009). July 2009. Sociedad Española de Musicología, Madrid, Spain. [doi]
Talks
Selected Conference Presentations
- Deconstructing Stellar Consensus. 23rd International Conference on Principles of Distributed System (OPODIS 2019), Neuchâtel, Switzerland, December 2019. [slides]
- Federated Byzantine quorum systems. 22nd International Conference on Principles of Distributed Systems (OPODIS 2018), Hong Kong, December 2018. [slides]
- Paxos consensus, deconstructed and abstracted. 27th European Symposium on Programming (ESOP 2018), Thessaloniki, Greece, April 2018. [slides]
- Rule formats for nominal process calculi. 28th International Conference on Concurrency Theory, (CONCUR 2017), Berlin, Germany, September 2017. [slides]
- Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. International Symposium on Principles and Practice of Declarative Programming (PPDP 2013), Madrid, Spain, September 2013. [slides]
Selected Seminar Presentations
- Federated Byzantine quorum systems. BART Blockchain Seminar, Telecom Paristech, Paris, France, February 2019. [slides]
- No solvable lambda-value term left behind. ICE-TCS Theory Week, Reykjavik University, Iceland, May 2016. [slides]
- On hopefully intelligible contributions to seminar series and related events (aka. this talk on Kurt Gödel is not a Pearl of Computation). ICE-TCS Pearls of Computation, Reykjavik University, Iceland, April 2016. [slides]
- The essence of Reynolds (title and some content borrowed from POPL14's session in honour of John C. Reynolds by Stephen Brookes, Peter O'Hearn and Uday Reddy). ICE-TCS Pearls of Computation, Reykjavik University, Iceland, April 2015. [slides]
Software
Interderivation of Semantic Artifacts
- Interderiving interpreters for the normal order strategy. [code]
- A Racket implementation of normal order's context-based reduction semantics. [code]
- Interderiving interpreters for the normal order strategy with 2-layer CPS. [code]
- Interderiving interpreters for the hybrid applicative order strategy. [code]
- Interderiving the full-reducing Krivine machine. [code]
- Deriving interpretations of gradually-typed lambda calculus. [code]
Solvability in the Lambda-Value Calculus
- Semi-decision procedure for solvable terms in the lambda-value calculus. [code]
Miscellanea
I am an avid filmgoer and consider myself a "non-encyclopedic" cinephile. Roughly, there are around twenty movies that I have seen more than twenty times. My favourite meta-cinematic experience is watching Sophie Fiennes's "The Pervert's Guide to Cinema".
I am a music aficionado and enthusiastic amateur musician, with a particular interest in early music. I play string struments and practice choir singing regularly. Currently I am a member of the Coro Ars Nova.
