Research
I am a postdoctoral researcher at
the IMDEA Software Institute.
My research interests are in concurrent and distributed systems and
the foundations of programming languages. I've worked on algorithms for
consensus, process algebras, rule formats for structural operational
semantics, semantics of programming languages, lambda calculus, nominal
techniques, type theory, abstract machines and program transformation.
See
my Curriculum
Vitae and in
FECYT cvn
format.
Publications
[ORCID 
Scopus 
dblp 
Google
Scholar 
ACM 
Mendeley 
ResearchGate]
Journal articles

[AFGI17]

Luca Aceto, Ignacio Fábregas, Álvaro
GarcíaPé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,
In Press. March 2017. Springer.
[doi]

[GN16]

Álvaro GarcíaPérez and Pablo Nogueira.
No solvable lambdavalue term left behind.
Logical Methods in Computer Science,
12(2:12):1–43(2016). May 2016.
[arxiv
 code
 slides]


[GN14]

Álvaro GarcíaPérez and Pablo Nogueira.
On the syntactic and functional correspondence between hybrid (or
layered) normalisers and abstract machines.
Science of Computer programming,
95:176–199(2014). December 2014. Springer.
[doi
 code]
Peerreviewed conference
and workshop articles

[GG18]

Álvaro GarcíaPérez and Alexey Gotsman.
Federated Byzantine quorum systems.
In Proceedings of the 22nd International Conference on Principles of
Distributed Systems (OPODIS 2018),
April 2018.
[doi
 slides]

[GGMS18]

Álvaro GarcíaPé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
 slides]

[AFGIM17]

Luca Aceto, Ignacio Fábregas, Álvaro GarcíaPérez,
Anna Ingólfsdótir and Yolanda OrtegaMallén.
Rule formats for nominal process calculi.
In Proceedings of the 28th International Conference on Concurrency Theory
(CONCUR 2017), pages 10:1–1016, Berlin, Germany, September 2017.
[doi
 slides]

[GNS14]

Álvaro GarcíaPérez, Pablo Nogueira and Ilya
Sergey.
Deriving interpretations of the graduallytyped lambda calculus.
In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation
and Program Manipulation (PEPM 2014), pages 157–168, San Diego,
CA, US, January 2014. ACM.
[doi
 code
 slides]

[GNM13]

Álvaro GarcíaPérez, Pablo Nogueira and Juan
José MorenoNavarro.
Deriving the fullreducing Krivine machine from the smallstep
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
 slides]


[GN13]

Álvaro GarcíaPérez and Pablo Nogueira.
A syntactic and functional correspondence between reduction semantics
and reductionfree full normalisers.
In Proceedings of the ACM SIGPLAN 2013 Workshop on Partial
Evaluation and Program Manipulation (PEPM 2013), pages
107–116, Rome, Italy, January 2013. ACM.
[doi
 code
 slides]

Book chapters

[AGI16]

Luca Aceto, Álvaro GarcíaPérez and Anna
Ingólfsdóttir.
Rule formats for bounded nondeterminism in structural operational
semantics.
In Semantics, Logics, and Calculi – Essays Dedicated to
Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th
Birthdays, volume 9560 of LNCS, pages 313–343. January
2016. Springer.
[doi
 slides]

PhD Dissertation

[Gar14]

Álvaro GarcíaPé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.
[pdf]
Contributions at international
workshops

[GGMS17]

Álvaro GarcíaPérez, Alexey Gotsman, Yuri Meshman and Ilya
Sergey.
Towards modular verification of consensus protocols
The Aarhus Concurrency Workshop (ACW
2017). Aarhus, Denmark, May 2017.
[slides]

[AFGI15]

Luca Aceto, Ignacio Fábregas, Álvaro
GarcíaPérez and Anna Ingólfsdóttir.
Rule formats for bounded nondeterminism in nominal structural
operational semantics.
Nordic Workshop on
Programming Theory (NWPT 2015). Reykjavik, Iceland, October
2015.
[slides]

[GN14a]

Álvaro GarcíaPérez and Pablo Nogueira.
A standard theory for the pure lambdavalue calculus.
International Workshop on Domain Theory and Applications (Domains
XI), Paris, France, September 2014.
[slides]


[GNG10]

Álvaro GarcíaPérez, Pablo Nogueira and Emilio
Jesús Gallego Arias.
The beta cube. International
Workshop on Reduction Strategies in Rewriting, Proving, and
Programming (IWS 2010), Edinburgh, UK, July 2010.
[pdf]


[GM07]

Álvaro GarcíaPérez and Nelson Medinilla
Martínez.
The ambiguity criterion in software design.
International Workshop on
Living with Uncertainty (IWLU 2007), Atlanta, GA, US,
November 2007.
Other publications

[GG09]

Amaya GarcíaPérez and Álvaro
GarcíaPérez.
La afinación de la flauta tradicional salmantina de tres
agujeros.
Revista de Musicología, 22(2):343–361(2009). June
2009. Sociedad Española de Musicología. Madrid, Spain.

[GG08]

Amaya GarcíaPérez and Álvaro
GarcíaPérez.
La afinación de la flauta tradicional salmantina de tres
agujeros.
In Actas del VII Congreso de Musicología de la Sociedad
Española de Musicología, Cáceres, Spain,
November 2008.
Presentations and talks
Presentations at international
conferences and workshops

[Dec. 2018]

Federated Byzantine quorum systems.
22nd International Conference on Principles of Distributed Systems (OPODIS 2018),
Hong Kong.
[slides]

[Apr. 2018]

Paxos consensus, deconstructed and abstracted.
27th European Symposium on Programming (ESOP 2018), Thessaloniki, Greece.
[slides]

[Sep. 2017]

Rule formats for nominal process calculi.
28th International Conference on Concurrency Theory, (CONCUR 2017), Berlin, Germany.
[slides]

[Jan. 2016]

Rule formats for bounded nondeterminism in structural operational
semantics.
Semantics, Logics, and Calculi – Essays Dedicated to Hanne Riis
Nielson and Flemming Nielson on the Occasion of Their 60th
Birthdays, Copenhagen, Denmark.
[slides]

[Oct. 2015]

Rule formats for bounded nondeterminism in nominal structural
operational semantics.
Nordic Workshop on Programming Theory (NWPT 2015), Reykjavik, Iceland.
[slides]

[Sep. 2014]

A standard theory for the pure lambdavalue calculus.
International Workshop on Domain Theory and Applications (Domains XI),
Paris, France.
[slides]

[Jan. 2014]

Deriving interpretations of the graduallytyped lambda
calculus.
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
(PEPM 2014), San Diego, California, US.
[slides]

[Sep. 2013]

Deriving the fullreducing Krivine machine from the smallstep
operational semantics of normal order.
International Symposium on Principles and Practice of Declarative
Programming (PPDP 2013), Madrid, Spain.
[slides]

[Jan. 2013]

A syntactic and functional correspondence between reduction
semantics and reductionfree full normalisers.
ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
(PEPM 2013), Rome, Italy.
[slides]

[Jul. 2010]

The beta cube.
International Workshop on Strategies in Rewriting, Proving, and
Programming (IWS 2010), Edinburgh, UK.

[Nov. 2007]

The ambiguity criterion in software design.
International Workshop on Living with Uncertainty (IWLU 2007),
Atlanta, Georgia, US.
Selected seminar presentations and talks

[May. 2016]

No solvable lambdavalue term left behind.
ICETCS Theory Week, Reykjavik University, Iceland.
[slides]

[Apr. 2016]

On hopefully intelligible contributions to seminar series and
related events (aka. this talk on Kurt Gödel is not a Pearl of
Computation).
ICETCS Pearls of Computation, Reykjavik University, Iceland.
[slides]

[Apr. 2015]

The essence of Reynolds (title borrowed from POPL14's session
in honour of John C. Reynolds by Stephen Brookes, Peter O'Hearn and
Uday Reddy).
ICETCS Pearls of Computation, Reykjavik University, Iceland.
[slides]

[Oct. 2014]

Operational aspects of full reduction in lambda calculi.
ICETCS Seminar, Reykjavik University, Iceland.

[Apr. 2014]

Reasoning about structural operational semantics in a calculus of
closures.
ICETCS Seminar, Reykjavik University, Iceland.

[Jul. 2013]

Deriving interpretations of the gradually typed lambda
calculus.
Student Talks Session, Oregon Programming Languages Summer School,
Eugene, Oregon, USA.

[Jul. 2013]

Deriving interpretations of the gradually typed lambda
calculus.
PL Group, Aarhus University, Denmark.

[Feb. 2013]

A syntactic and functional correspondence between reduction
semantics and reductionfree full normalisers
.
PL Group, Aarhus University, Denmark.

[Mar. 2011]

The beta cube.
Programming, Logic and Semantics Group, IT University, Copenhaguen,
Denmark.