| 2024 | ITP | Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics. | Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani |
| 2020 | PPDP | Understanding Lua's Garbage Collection: Towards a Formalized Static Analyzer. | Mallku Soldevila, Beta Ziliani, Daniel Fridlender |
| 2019 | TAP | Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. | Raul Fervari, Francisco Trucco, Beta Ziliani |
| 2017 | DLS | Decoding Lua: formal semantics for the developer and the semanticist. | Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, Fabio Mascarenhas |
| 2015 | ICFP | A unification algorithm for Coq featuring universe polymorphism and overloading. | Beta Ziliani, Matthieu Sozeau |
| 2013 | ICFP | Mtac: a monad for typed tactic programming in Coq. | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | ITP | Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. | Guillaume Claret, Lourdes Del Carmen Gonzlez-Huesca, Yann Rgis-Gianas, Beta Ziliani |
| 2011 | ICFP | How to make ad hoc proof automation less ad hoc. | Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer |