Journals

• From Specification to Testing: Semantics Engineering for Lua 5.2.
  M. Soldevila, B. Silvestre, B. Ziliani.
  In Journal of Automated Reasoning (2022) (doi) (pdf).
• Verification of Dynamic Bisimulation Theorems in Coq
  R. Fervari, F. Trucco, B. Ziliani.
  In Journal of Logical and Algebraic Methods in Programming (JLAMP, 2021) (pdf).
• Mtac2: Typed Tactics for Backward Reasoning in Coq
  J.-O. Kaiser, B. Ziliani, R. Krebbers, Y. Régis-Gianas and D. Dreyer.
  Presented in International Conference for Functional Programming (ICFP 2018) and published in PACMPL, Volume 2, Issue ICFP, September 2018 (doi) (video).
• A Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading.
  B. Ziliani, M. Sozeau.
  In Journal of functional Programming (JFP), Volume 27, February 2017 (pdf) (doi) (code).
• Mtac: A Monad for Typed Tactic Programming in Coq.
  B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, V. Vafeiadis.
  In Journal of Functional Programming (JFP), Volume 25, August 2015 (web page).
  Special issue devoted to selected papers from ICFP 2013.
• How to Make Ad Hoc Proof Automation Less Ad Hoc.
  G. Gonthier, B. Ziliani, A. Nanevski, D. Dreyer.
  In Journal of Functional Programming (JFP), Volume 23, July 2013 (web page).
  Special issue devoted to selected papers from ICFP 2011.

Proceedings (peer-reviewed long papers)

• Understanding Lua's Garbage Collection. Towards a Formalized Static Analyzer.
  M. Soldevila, B. Ziliani, D. Fridlender.
  In Symposium on Principles and Practice of Declarative Programming (PPDP 2020) (pdf).
• Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq
  R. Fervari, F. Trucco, B. Ziliani.
  In 2nd DaLí Workshop (DaLí 19) (pdf).
• Decoding Lua: Formal Semantics for the Developer and the Semanticist.
  M. Soldevila, B. Ziliani, B. Silvestre, D. Fridlender, F. Mascarenhas.
  In Dynamic Languages Symposium (DLS 2017) (pdf).
• A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading.
  B. Ziliani, M. Sozeau.
  In International Conference of Functional Programming (ICFP 2015) (pdf) (code).
• Mtac: A Monad for Typed Tactic Programming in Coq.
  B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, V. Vafeiadis.
  In International Conference of Functional Programming (ICFP 2013) (web page).
• Lightweight proof by reflection using a posteriori simulation of effectful computation.
  G. Clauret, L. del C. González Huesca, Y. Régis-Gianas, B. Ziliani.
  In Conference on Interactive Theorem Proving (ITP 2013) (pdf).
• How to Make Ad Hoc Proof Automation Less Ad Hoc.
  G. Gonthier, B. Ziliani, A. Nanevski, D. Dreyer.
  In International Conference of Functional Programming (ICFP 2011) (web page).
• Swapping: a natural bridge between named and indexed explicit substitution calculi.
  A. Mendelzon, A. Ríos, B. Ziliani.
  In International Workshop on Higher-Order Rewriting (HOR 2010) (pdf).

Abstracts

• Extended Abstract: Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2.
  I. Tiraboschi, J.-O. Kaiser, B. Ziliani.
  In ACM Workshop on Type-Driven Development, TyDe 2020, 2020. (link).
• A “destruct” tactic for Mtac2.
  J.-O. Kaiser and B. Ziliani
  In the 4th International Workshop on Coq for Programming Languages, CoqPL ’18, 2018 (link).
• Introducing MetaCoq: A Safe Tactic Language for Coq.
  B. Ziliani.
  In Type Theory Based Tools (TTT 2017) (pdf).
• Towards a better-behaved unification algorithm for Coq.
  B. Ziliani, M. Sozeau.
  In International Workshop on Unification (UNIF 2014) (pdf).
• Towards a better-behaved unification algorithm for Coq.
  B. Ziliani, M. Sozeau.
  In Coq-6: The Coq Workshop (2014) (pdf).

Theses

• Interactive Typed Tactic Programming for the Coq Proof Assistant.
  B. Ziliani.
  PhD Thesis, 2015 (manuscript and code).
• λgc: A Calculus based on λ-calculus with Garbage Collection.
  B. Ziliani.
  Master's Thesis, 2009 (pdf), Universidad de Buenos Aires (Spanish).