A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers. - Álvaro García-Pérez; Pablo Nogueira (PEPM, 2013)

Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. - Álvaro García-Pérez; Pablo Nogueira; Juan José Moreno-Navarro (PPDP, 2013)

Deriving interpretations of the gradually-typed lambda calculus. - Álvaro García-Pérez; Pablo Nogueira; Ilya Sergey (PEPM, 2014)

On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines. - Álvaro García-Pérez; Pablo Nogueira (Sci. Comput. Program., 2014)

Operational Aspects of Full Reduction in Lambda Calculi. - Álvaro García-Pérez (2014)

Rule Formats for Bounded Nondeterminism in Structural Operational Semantics. - Luca Aceto; Álvaro García-Pérez; Anna Ingólfsdóttir (Semantics, Logics, and Calculi, 2016)

No solvable lambda-value term left behind. - Álvaro García-Pérez; Pablo Nogueira (Log. Methods Comput. Sci., 2016)

A unified rule format for bounded nondeterminism in SOS with terms as labels. - Luca Aceto; Ignacio Fábregas; Álvaro García-Pérez; Anna Ingólfsdóttir (J. Log. Algebraic Methods Program., 2017)

Paxos Consensus, Deconstructed and Abstracted. - Álvaro García-Pérez; Alexey Gotsman; Yuri Meshman; Ilya Sergey (ESOP, 2018)

Federated Byzantine Quorum Systems. - Álvaro García-Pérez; Alexey Gotsman (OPODIS, 2018)

Paxos Consensus, Deconstructed and Abstracted (Extended Version). - Álvaro García-Pérez; Alexey Gotsman; Yuri Meshman; Ilya Sergey (CoRR, 2018)

Federated Byzantine Quorum Systems (Extended Version). - Álvaro García-Pérez; Alexey Gotsman (CoRR, 2018)

Deconstructing Stellar Consensus. - Álvaro García-Pérez; Maria Anna Schett (OPODIS, 2019)

Deconstructing Stellar Consensus (Extended Version). - Álvaro García-Pérez; Maria Anna Schett (CoRR, 2019)

The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus. - Álvaro García-Pérez; Pablo Nogueira (J. Funct. Program., 2019)

Rule Formats for Nominal Process Calculi. - Luca Aceto; Ignacio Fábregas; Álvaro García-Pérez; Anna Ingólfsdóttir; Yolanda Ortega-Mallén (Log. Methods Comput. Sci., 2019)

SoK: Achieving State Machine Replication in Blockchains based on Repeated Consensus. - Silvia Bonomi; Antonella Del Pozzo; Álvaro García-Pérez; Sara Tucci Piergiovanni (CoRR, 2021)

Equivalence of eval-readback and eval-apply big-step evaluators by regimentation of the lambda-calculus's strategy space. - Pablo Nogueira; Álvaro García-Pérez (CoRR, 2022)

Notara: Efficient Blockchain Asset Notarization Service. - Guillermo Toyos-Marfurt; Rouwaida Abdallah; Álvaro García-Pérez (BRAINS, 2024)

Fantastyc: Blockchain-Based Federated Learning Made Secure and Practical. - William Boitier; Antonella Del Pozzo; Álvaro García-Pérez; Stéphane Gazut; Pierre Jobic; Alexis Lemaire; Erwan Mahe; Aurélien Mayoue; Maxence Perion; Tuanir Franca Rezende; Deepika Singh; Sara Tucci Piergiovanni (SRDS, 2024)

Pure Subtype Systems Are Type-Safe. - Valentin Pasquale; Álvaro García-Pérez (CoRR, 2024)

Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space. - Pablo Nogueira; Álvaro García-Pérez (Log. Methods Comput. Sci., 2024)