Swapping: a natural bridge between named and indexed explicit substitution calculi - Ariel Mendelzon; Alejandro Ríos 001; Beta Ziliani (HOR, 2010)

Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. - Guillaume Claret; Lourdes Del Carmen González-Huesca; Yann Régis-Gianas; Beta Ziliani (ITP, 2013)

How to make ad hoc proof automation less ad hoc. - Georges Gonthier; Beta Ziliani; Aleksandar Nanevski; Derek Dreyer (J. Funct. Program., 2013)

Towards a better-behaved unification algorithm for Coq. - Beta Ziliani; Matthieu Sozeau (UNIF, 2014)

A unification algorithm for Coq featuring universe polymorphism and overloading. - Beta Ziliani; Matthieu Sozeau (ICFP, 2015)

Mtac: A monad for typed tactic programming in Coq. - Beta Ziliani; Derek Dreyer; Neelakantan R. Krishnaswami; Aleksandar Nanevski; Viktor Vafeiadis (J. Funct. Program., 2015)

Interactive typed tactic programming in the Coq proof assistant. - Beta Ziliani (2015)

Decoding Lua: formal semantics for the developer and the semanticist. - Mallku Soldevila; Beta Ziliani; Bruno Silvestre; Daniel Fridlender; Fabio Mascarenhas (DLS, 2017)

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. - Beta Ziliani; Matthieu Sozeau (J. Funct. Program., 2017)

Mtac2: typed tactics for backward reasoning in Coq. - Jan-Oliver Kaiser; Beta Ziliani; Robbert Krebbers; Yann Régis-Gianas; Derek Dreyer (Proc. ACM Program. Lang., 2018)

Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. - Raul Fervari; Francisco Trucco; Beta Ziliani (DaLí, 2019)

Understanding Lua's Garbage Collection: Towards a Formalized Static Analyzer. - Mallku Soldevila; Beta Ziliani; Daniel Fridlender (PPDP, 2020)

Verification of dynamic bisimulation theorems in Coq. - Raul Fervari; Francisco Trucco; Beta Ziliani (J. Log. Algebraic Methods Program., 2021)

From Specification to Testing: Semantics Engineering for Lua 5.2. - Mallku Soldevila; Beta Ziliani; Bruno Silvestre (J. Autom. Reason., 2022)

Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics. - Mallku Soldevila; Rodrigo Geraldo Ribeiro; Beta Ziliani (ITP, 2024)

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics. - Mallku Soldevila; Rodrigo Geraldo Ribeiro; Beta Ziliani (CoRR, 2024)

redex2coq. - Mallku Soldevila; Rodrigo Geraldo Ribeiro; Beta Ziliani (DROPS Artifacts, 2024)